let fp be FinSequence of NAT ; :: thesis: ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for b being Element of NAT st b in dom fp holds
(Product (Del (fp,b))) gcd (fp . b) = 1 )
defpred S1[ FinSequence of NAT ] means for b being Element of NAT st b in dom $1 holds
(Product (Del ($1,b))) gcd ($1 . b) = 1;
defpred S2[ FinSequence of NAT ] means for b, c being Element of NAT st b in dom $1 & c in dom $1 & b <> c holds
($1 . b) gcd ($1 . c) = 1;
defpred S3[ set ] means ex f being FinSequence of NAT st
( f = $1 & ( len f >= 2 & S2[f] implies S1[f] ) );
A1: now :: thesis: for fp being FinSequence of NAT
for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let d be Element of NAT ; :: thesis: ( S3[fp] implies S3[fp ^ <*d*>] )
assume A2: S3[fp] ; :: thesis: S3[fp ^ <*d*>]
set k = len fp;
set fp1 = fp ^ <*d*>;
now :: thesis: ( len (fp ^ <*d*>) >= 2 & S2[fp ^ <*d*>] implies S1[fp ^ <*d*>] )
assume that
A3: len (fp ^ <*d*>) >= 2 and
A4: S2[fp ^ <*d*>] ; :: thesis: S1[fp ^ <*d*>]
A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16;
now :: thesis: S1[fp ^ <*d*>]
per cases ( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 ) by A3, XXREAL_0:1;
suppose A6: len (fp ^ <*d*>) = 2 ; :: thesis: S1[fp ^ <*d*>]
then ( 1 in dom (fp ^ <*d*>) & 2 in dom (fp ^ <*d*>) ) by FINSEQ_3:25;
then A7: ((fp ^ <*d*>) . 2) gcd ((fp ^ <*d*>) . 1) = 1 by A4;
A8: fp ^ <*d*> = <*((fp ^ <*d*>) . 1),((fp ^ <*d*>) . 2)*> by A6, FINSEQ_1:44;
for b being Element of NAT st b in dom (fp ^ <*d*>) holds
(Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
proof
let b be Element of NAT ; :: thesis: ( b in dom (fp ^ <*d*>) implies (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 )
assume b in dom (fp ^ <*d*>) ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
then A9: b in Seg (len (fp ^ <*d*>)) by FINSEQ_1:def 3;
per cases ( b = 1 or b = 2 ) by A6, A9, FINSEQ_1:2, TARSKI:def 2;
suppose b = 1 ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product <*((fp ^ <*d*>) . 2)*>) gcd ((fp ^ <*d*>) . 1) by A8, WSIERP_1:19
.= 1 by A7, RVSUM_1:95 ;
:: thesis: verum
end;
suppose b = 2 ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product <*((fp ^ <*d*>) . 1)*>) gcd ((fp ^ <*d*>) . 2) by A8, WSIERP_1:19
.= 1 by A7, RVSUM_1:95 ;
:: thesis: verum
end;
end;
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
suppose len (fp ^ <*d*>) > 2 ; :: thesis: S1[fp ^ <*d*>]
then A10: (len fp) + 1 > 1 + 1 by FINSEQ_2:16;
then len fp >= 1 + 1 by NAT_1:13;
then consider n being Nat such that
A11: len fp = n + 1 by NAT_1:6;
A12: S2[fp]
proof
A13: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26;
let b, c be Element of NAT ; :: thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 )
assume that
A14: ( b in dom fp & c in dom fp ) and
A15: b <> c ; :: thesis: (fp . b) gcd (fp . c) = 1
( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A14, FINSEQ_1:def 7;
hence (fp . b) gcd (fp . c) = 1 by A4, A14, A15, A13; :: thesis: verum
end;
A16: for a being Nat st a in dom fp holds
(fp . a) gcd d = 1
proof
let a be Nat; :: thesis: ( a in dom fp implies (fp . a) gcd d = 1 )
A17: (len fp) + 1 in dom (fp ^ <*d*>) by A5, FINSEQ_5:6;
A18: ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . ((len fp) + 1) = d ) by FINSEQ_1:26, FINSEQ_1:42;
assume A19: a in dom fp ; :: thesis: (fp . a) gcd d = 1
(len fp) + 1 > len fp by NAT_1:13;
then A20: (len fp) + 1 <> a by A19, FINSEQ_3:25;
(fp ^ <*d*>) . a = fp . a by A19, FINSEQ_1:def 7;
hence (fp . a) gcd d = 1 by A4, A19, A18, A20, A17; :: thesis: verum
end;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A21: len fp = n + 1 by A11;
for b being Element of NAT st b in dom (fp ^ <*d*>) holds
(Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
proof
let b be Element of NAT ; :: thesis: ( b in dom (fp ^ <*d*>) implies (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 )
assume A22: b in dom (fp ^ <*d*>) ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
A23: b >= 1 by A22, FINSEQ_3:25;
A24: b <= (len fp) + 1 by A5, A22, FINSEQ_3:25;
per cases ( b <= len fp or b = (len fp) + 1 ) by A24, NAT_1:8;
suppose b <= len fp ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
then A25: b in dom fp by A23, FINSEQ_3:25;
then ( (Product (Del (fp,b))) gcd (fp . b) = 1 & (fp . b) gcd d = 1 ) by A2, A10, A12, A16, NAT_1:13;
then ((Product (Del (fp,b))) * d) gcd (fp . b) = 1 by WSIERP_1:7;
then A26: (Product ((Del (fp,b)) ^ <*d*>)) gcd (fp . b) = 1 by RVSUM_1:96;
Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*> by A21, A25, Th30;
hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1 by A25, A26, FINSEQ_1:def 7; :: thesis: verum
end;
suppose b = (len fp) + 1 ; :: thesis: (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = 1
hence (Product (Del ((fp ^ <*d*>),b))) gcd ((fp ^ <*d*>) . b) = (Product (Del ((fp ^ <*d*>),((len fp) + 1)))) gcd d by FINSEQ_1:42
.= (Product fp) gcd d by WSIERP_1:40
.= 1 by A16, WSIERP_1:36 ;
:: thesis: verum
end;
end;
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
end;
end;
hence S1[fp ^ <*d*>] ; :: thesis: verum
end;
hence S3[fp ^ <*d*>] ; :: thesis: verum
end;
A27: S3[ <*> NAT]
proof
take <*> NAT ; :: thesis: ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) )
thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) ; :: thesis: verum
end;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A27, A1);
 then ex f being FinSequence of NAT st
( f = fp & ( len f >= 2 & S2[f] implies S1[f] ) ) ;
hence ( len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for b being Element of NAT st b in dom fp holds
(Product (Del (fp,b))) gcd (fp . b) = 1 ) ; :: thesis: verum