let n be Nat; for p being one-to-one a_partition of n
for e being odd-valued a_partition of n holds
( e = Euler_transformation p iff for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
let p be one-to-one a_partition of n; for e being odd-valued a_partition of n holds
( e = Euler_transformation p iff for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
let e be odd-valued a_partition of n; ( e = Euler_transformation p iff for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
thus
( e = Euler_transformation p implies for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
( ( for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... ) implies e = Euler_transformation p )proof
assume A1:
e = Euler_transformation p
;
for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
let O be
odd-valued FinSequence;
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... let a be
natural-valued FinSequence;
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... let sort be
odd_organization of
O;
( len O = len p & len p = len a & p = O (#) (2 |^ a) implies for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... )
assume A2:
(
len O = len p &
len p = len a &
p = O (#) (2 |^ a) )
;
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
let j be
Nat;
card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
len (2 |^ a) = len a
by CARD_1:def 7;
then A3:
(
dom O = dom p &
dom p = dom a &
dom (2 |^ a) = dom a )
by A2, FINSEQ_3:29;
reconsider S =
sort as
DoubleReorganization of
dom p by A2, FINSEQ_3:29;
A4:
(2 * 1) - 1
= 1
;
A5:
(2 * 2) - 1
= 3
;
(2 * 3) - 1
= 5
;
then A6:
( 1
= O . (S _ (1,1)) & ... & 1
= O . (S _ (1,(len (S . 1)))) & 3
= O . (S _ (2,1)) & ... & 3
= O . (S _ (2,(len (S . 2)))) & 5
= O . (S _ (3,1)) & ... & 5
= O . (S _ (3,(len (S . 3)))) & ( for
i being
Nat holds
(2 * i) - 1
= O . (S _ (i,1)) & ... &
(2 * i) - 1
= O . (S _ (i,(len (S . i)))) ) )
by A4, Def4, A5;
(2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (
j,1)
by FLEXARY1:42;
then card (Coim (e,((j * 2) - 1))) =
((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),(1 + 1)) +...)
by A6, A2, A1, Def5
.=
(
(((2 |^ a) *. S) . j),1)
+...
by FLEXARY1:20, A3
;
hence
card (Coim (e,((j * 2) - 1))) = (
(((2 |^ a) *. sort) . j),1)
+...
;
verum
end;
assume A7:
for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...
; e = Euler_transformation p
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
proof
let j be
Nat;
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )let O be
odd-valued FinSequence;
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )let a be
natural-valued FinSequence;
( len O = len p & len p = len a & p = O (#) (2 |^ a) implies for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) )
assume A8:
(
len O = len p &
len p = len a &
p = O (#) (2 |^ a) )
;
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
let sort be
DoubleReorganization of
dom p;
( 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) implies ( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) )
assume A9:
( 1
= O . (sort _ (1,1)) & ... & 1
= O . (sort _ (1,(len (sort . 1)))) & 3
= O . (sort _ (2,1)) & ... & 3
= O . (sort _ (2,(len (sort . 2)))) & 5
= O . (sort _ (3,1)) & ... & 5
= O . (sort _ (3,(len (sort . 3)))) & ( for
i being
Nat holds
(2 * i) - 1
= O . (sort _ (i,1)) & ... &
(2 * i) - 1
= O . (sort _ (i,(len (sort . i)))) ) )
;
( card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
A10:
for
j being
Nat holds
card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
proof
let j be
Nat;
card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
len (2 |^ a) = len a
by CARD_1:def 7;
then A11:
(
dom O = dom p &
dom p = dom a &
dom (2 |^ a) = dom a )
by A8, FINSEQ_3:29;
reconsider S =
sort as
DoubleReorganization of
dom p ;
A12:
sort is
odd_organization of
O
by A11, A9, Th4;
(2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (
j,1)
by FLEXARY1:42;
then
(
(((2 |^ a) *. S) . j),1)
+... = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),(1 + 1)) +...)
by A11, FLEXARY1:20;
hence
card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
by A12, A7, A8;
verum
end;
(
(1 * 2) - 1
= 1 &
(2 * 2) - 1
= 3 &
(3 * 2) - 1
= 5 )
;
hence
(
card (Coim (e,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) &
card (Coim (e,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) &
card (Coim (e,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) &
card (Coim (e,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
by A10;
verum
end;
hence
e = Euler_transformation p
by Def5; verum