let n be Nat; :: thesis: for fp being FinSequence of NAT st n > 1 & len fp >= 2 & ( for d being Element of NAT st d in dom fp holds
fp . d,n are_coprime ) holds
for fr being FinSequence of NAT st len fr = len fp & ( for d being Element of NAT st d in dom fr holds
fr . d = order ((fp . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) holds
order ((Product fp),n) = Product fr
let fp be FinSequence of NAT ; :: thesis: ( n > 1 & len fp >= 2 & ( for d being Element of NAT st d in dom fp holds
fp . d,n are_coprime ) implies for fr being FinSequence of NAT st len fr = len fp & ( for d being Element of NAT st d in dom fr holds
fr . d = order ((fp . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) holds
order ((Product fp),n) = Product fr )
defpred S1[ FinSequence of NAT ] means for d being Element of NAT st d in dom $1 holds
$1 . d,n are_coprime ;
defpred S2[ FinSequence of NAT ] means for fr being FinSequence of NAT st len fr = len $1 & ( for d being Element of NAT st d in dom fr holds
fr . d = order (($1 . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) holds
order ((Product $1),n) = Product fr;
defpred S3[ FinSequence of NAT ] means ( n > 1 & len $1 >= 2 & S1[$1] implies S2[$1] );
A1: S3[ <*> NAT] ;
A2: for fp being FinSequence of NAT
for c being Element of NAT st S3[fp] holds
S3[fp ^ <*c*>]
proof
let fp be FinSequence of NAT ; :: thesis: for c being Element of NAT st S3[fp] holds
S3[fp ^ <*c*>]
let c be Element of NAT ; :: thesis: ( S3[fp] implies S3[fp ^ <*c*>] )
assume A3: S3[fp] ; :: thesis: S3[fp ^ <*c*>]
set fp1 = fp ^ <*c*>;
S3[fp ^ <*c*>]
proof
assume A4: ( n > 1 & len (fp ^ <*c*>) >= 2 & S1[fp ^ <*c*>] ) ; :: thesis: S2[fp ^ <*c*>]
A5: len (fp ^ <*c*>) = (len fp) + 1 by FINSEQ_2:16;
per cases ( len (fp ^ <*c*>) = 2 or len (fp ^ <*c*>) > 2 ) by A4, XXREAL_0:1;
suppose A6: len (fp ^ <*c*>) = 2 ; :: thesis: S2[fp ^ <*c*>]
then fp ^ <*c*> = <*((fp ^ <*c*>) . 1),((fp ^ <*c*>) . 2)*> by FINSEQ_1:44;
then A7: Product (fp ^ <*c*>) = ((fp ^ <*c*>) . 1) * ((fp ^ <*c*>) . 2) by RVSUM_1:99;
dom (fp ^ <*c*>) = Seg 2 by A6, FINSEQ_1:def 3;
then A8: ( 1 in dom (fp ^ <*c*>) & 2 in dom (fp ^ <*c*>) ) ;
then A9: ( (fp ^ <*c*>) . 1,n are_coprime & (fp ^ <*c*>) . 2,n are_coprime ) by A4;
S2[fp ^ <*c*>]
proof
let fr be FinSequence of NAT ; :: thesis: ( len fr = len (fp ^ <*c*>) & ( for d being Element of NAT st d in dom fr holds
fr . d = order (((fp ^ <*c*>) . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) implies order ((Product (fp ^ <*c*>)),n) = Product fr )
assume A10: ( len fr = len (fp ^ <*c*>) & ( for d being Element of NAT st d in dom fr holds
fr . d = order (((fp ^ <*c*>) . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) ) ; :: thesis: order ((Product (fp ^ <*c*>)),n) = Product fr
then A11: ( 1 in dom fr & 2 in dom fr ) by A8, FINSEQ_3:29;
then fr . 1,fr . 2 are_coprime by A10;
then order (((fp ^ <*c*>) . 1),n),fr . 2 are_coprime by A10, A11;
then A12: order (((fp ^ <*c*>) . 1),n), order (((fp ^ <*c*>) . 2),n) are_coprime by A10, A11;
fr = <*(fr . 1),(fr . 2)*> by A6, A10, FINSEQ_1:44;
then Product fr = (fr . 1) * (fr . 2) by RVSUM_1:99
.= (order (((fp ^ <*c*>) . 1),n)) * (fr . 2) by A10, A11
.= (order (((fp ^ <*c*>) . 1),n)) * (order (((fp ^ <*c*>) . 2),n)) by A10, A11 ;
hence order ((Product (fp ^ <*c*>)),n) = Product fr by A12, A4, A7, A9, Th17; :: thesis: verum
end;
hence S2[fp ^ <*c*>] ; :: thesis: verum
end;
suppose len (fp ^ <*c*>) > 2 ; :: thesis: S2[fp ^ <*c*>]
then (len fp) + 1 > 2 by FINSEQ_2:16;
then A13: ((len fp) + 1) - 1 >= 2 by INT_1:52;
A14: S1[fp]
proof
let d be Element of NAT ; :: thesis: ( d in dom fp implies fp . d,n are_coprime )
assume A15: d in dom fp ; :: thesis: fp . d,n are_coprime
then (fp ^ <*c*>) . d = fp . d by FINSEQ_1:def 7;
hence fp . d,n are_coprime by A4, A15, FINSEQ_2:15; :: thesis: verum
end;
S2[fp ^ <*c*>]
proof
let fr be FinSequence of NAT ; :: thesis: ( len fr = len (fp ^ <*c*>) & ( for d being Element of NAT st d in dom fr holds
fr . d = order (((fp ^ <*c*>) . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) implies order ((Product (fp ^ <*c*>)),n) = Product fr )
assume A16: ( len fr = len (fp ^ <*c*>) & ( for d being Element of NAT st d in dom fr holds
fr . d = order (((fp ^ <*c*>) . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) ) ; :: thesis: order ((Product (fp ^ <*c*>)),n) = Product fr
then consider f being FinSequence of NAT , l being Element of NAT such that
A17: fr = f ^ <*l*> by FINSEQ_2:19;
A18: (len f) + 1 = (len fp) + 1 by A5, A16, A17, FINSEQ_2:16;
A19: for d being Element of NAT st d in dom f holds
f . d = order ((fp . d),n)
proof
let d be Element of NAT ; :: thesis: ( d in dom f implies f . d = order ((fp . d),n) )
assume A20: d in dom f ; :: thesis: f . d = order ((fp . d),n)
then A21: f . d = fr . d by A17, FINSEQ_1:def 7;
A22: d in dom fr by A20, A17, FINSEQ_2:15;
dom f = dom fp by A18, FINSEQ_3:29;
then fp . d = (fp ^ <*c*>) . d by A20, FINSEQ_1:def 7;
hence f . d = order ((fp . d),n) by A22, A16, A21; :: thesis: verum
end;
for d, e being Element of NAT st d in dom f & e in dom f & d <> e holds
f . d,f . e are_coprime
proof
let d, e be Element of NAT ; :: thesis: ( d in dom f & e in dom f & d <> e implies f . d,f . e are_coprime )
assume A23: ( d in dom f & e in dom f & d <> e ) ; :: thesis: f . d,f . e are_coprime
then A24: ( f . d = fr . d & f . e = fr . e ) by A17, FINSEQ_1:def 7;
( d in dom fr & e in dom fr ) by A23, A17, FINSEQ_2:15;
hence f . d,f . e are_coprime by A23, A16, A24; :: thesis: verum
end;
then A25: order ((Product fp),n) = Product f by A18, A19, A14, A3, A4, A13;
A26: for d being Nat st d in dom fp holds
(fp . d) gcd n = 1 by A14, INT_2:def 3;
(Product fp) gcd n = 1 by A26, WSIERP_1:36;
then A27: Product fp,n are_coprime by INT_2:def 3;
reconsider z = 0 , j = 1 as Element of NAT ;
(len fp) + j >= z + j by XREAL_1:7;
then (len fp) + 1 in dom (fp ^ <*c*>) by A5, FINSEQ_3:25;
then (fp ^ <*c*>) . ((len fp) + 1),n are_coprime by A4;
then A28: c,n are_coprime by FINSEQ_1:42;
(len f) + j >= z + j by XREAL_1:7;
then len fr >= j by A17, FINSEQ_2:16;
then A29: len fr in dom fr by FINSEQ_3:25;
then fr . (len fr) = order (((fp ^ <*c*>) . (len fr)),n) by A16
.= order (((fp ^ <*c*>) . ((len fp) + 1)),n) by A16, FINSEQ_2:16
.= order (c,n) by FINSEQ_1:42 ;
then A30: fr . ((len f) + 1) = order (c,n) by A17, FINSEQ_2:16;
A31: ( Product (fp ^ <*c*>) = (Product fp) * c & Product fr = (Product f) * l ) by A17, RVSUM_1:96;
for d being Nat st d in dom f holds
(f . d) gcd (fr . ((len f) + 1)) = 1
proof
let d be Nat; :: thesis: ( d in dom f implies (f . d) gcd (fr . ((len f) + 1)) = 1 )
assume A32: d in dom f ; :: thesis: (f . d) gcd (fr . ((len f) + 1)) = 1
then A33: d in dom fr by A17, FINSEQ_2:15;
d <= len f by A32, FINSEQ_3:25;
then A34: d < (len f) + 1 by XREAL_1:145;
(len f) + 1 in dom fr by A17, A29, FINSEQ_2:16;
then fr . d,fr . ((len f) + 1) are_coprime by A16, A33, A34;
then f . d,fr . ((len f) + 1) are_coprime by A17, A32, FINSEQ_1:def 7;
hence (f . d) gcd (fr . ((len f) + 1)) = 1 by INT_2:def 3; :: thesis: verum
end;
then (Product f) gcd (fr . ((len f) + 1)) = 1 by WSIERP_1:36;
then Product f, order (c,n) are_coprime by A30, INT_2:def 3;
then order (((Product fp) * c),n) = (order ((Product fp),n)) * (order (c,n)) by A4, A28, A27, A25, Th17;
hence order ((Product (fp ^ <*c*>)),n) = Product fr by A31, A30, A17, A25, FINSEQ_1:42; :: thesis: verum
end;
hence S2[fp ^ <*c*>] ; :: thesis: verum
end;
end;
end;
hence S3[fp ^ <*c*>] ; :: thesis: verum
end;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A1, A2);
 hence ( n > 1 & len fp >= 2 & ( for d being Element of NAT st d in dom fp holds
fp . d,n are_coprime ) implies for fr being FinSequence of NAT st len fr = len fp & ( for d being Element of NAT st d in dom fr holds
fr . d = order ((fp . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) holds
order ((Product fp),n) = Product fr ) ; :: thesis: verum