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[ FinSequence of NAT ] means ( len $1 >= 2 & S2[$1] implies S1[$1] );
A1: now
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
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:19;
now
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:27;
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:61;
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:4, 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:26
.= 1 by A7, RVSUM_1:125 ;
:: 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:26
.= 1 by A7, RVSUM_1:125 ;
:: 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:19;
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:39;
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:39, FINSEQ_1:59;
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:27;
(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 13;
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:27;
A24: b <= (len fp) + 1 by A5, A22, FINSEQ_3:27;
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:27;
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:12;
then A26: (Product ((Del fp,b) ^ <*d*>)) gcd (fp . b) = 1 by RVSUM_1:126;
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:59
.= (Product fp) gcd d by WSIERP_1:48
.= 1 by A16, WSIERP_1:43 ;
:: 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 ] ;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A27, A1);
 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