let fp be FinSequence of NAT ; :: thesis: for a being Nat st ( 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 ) & ( for b being Element of NAT st b in dom fp holds
fp . b divides a ) holds
Product fp divides a
let a be Nat; :: thesis: ( ( 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 ) & ( for b being Element of NAT st b in dom fp holds
fp . b divides a ) implies Product fp divides a )
defpred S1[ 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 ) & ( for b being Element of NAT st b in dom $1 holds
$1 . b divides a ) );
defpred S2[ FinSequence of NAT ] means Product $1 divides a;
defpred S3[ set ] means ex f being FinSequence of NAT st
( f = $1 & ( S1[f] implies S2[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 fp1 = fp ^ <*d*>;
(len fp) + 1 >= 0 + 1 by XREAL_1:6;
then A3: len (fp ^ <*d*>) >= 1 by FINSEQ_2:16;
now :: thesis: ( S1[fp ^ <*d*>] implies S2[fp ^ <*d*>] )
assume A4: S1[fp ^ <*d*>] ; :: thesis: S2[fp ^ <*d*>]
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 )
A5: len (fp ^ <*d*>) in dom (fp ^ <*d*>) by A3, FINSEQ_3:25;
assume A6: a in dom fp ; :: thesis: (fp . a) gcd d = 1
then a <= len fp by FINSEQ_3:25;
then a < (len fp) + 1 by XREAL_1:39;
then A7: a < len (fp ^ <*d*>) by FINSEQ_2:16;
a in dom (fp ^ <*d*>) by A6, FINSEQ_2:15;
then ((fp ^ <*d*>) . a) gcd ((fp ^ <*d*>) . (len (fp ^ <*d*>))) = 1 by A4, A7, A5;
then A8: ((fp ^ <*d*>) . a) gcd ((fp ^ <*d*>) . ((len fp) + 1)) = 1 by FINSEQ_2:16;
(fp ^ <*d*>) . a = fp . a by A6, FINSEQ_1:def 7;
hence (fp . a) gcd d = 1 by A8, FINSEQ_1:42; :: thesis: verum
end;
then (Product fp) gcd d = 1 by WSIERP_1:36;
then A9: Product fp,d are_coprime by INT_2:def 3;
A10: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26;
A11: 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
proof
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
A12: ( b in dom fp & c in dom fp ) and
A13: b <> c ; :: thesis: (fp . b) gcd (fp . c) = 1
( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A12, FINSEQ_1:def 7;
hence (fp . b) gcd (fp . c) = 1 by A4, A10, A12, A13; :: thesis: verum
end;
A14: for b being Element of NAT st b in dom fp holds
fp . b divides a
proof
let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides a )
assume A15: b in dom fp ; :: thesis: fp . b divides a
then (fp ^ <*d*>) . b = fp . b by FINSEQ_1:def 7;
hence fp . b divides a by A4, A10, A15; :: thesis: verum
end;
len (fp ^ <*d*>) in dom (fp ^ <*d*>) by FINSEQ_5:6;
then (fp ^ <*d*>) . (len (fp ^ <*d*>)) divides a by A4;
then (fp ^ <*d*>) . ((len fp) + 1) divides a by FINSEQ_2:16;
then d divides a by FINSEQ_1:42;
then (Product fp) * d divides a by A2, A11, A14, A9, PEPIN:4;
hence S2[fp ^ <*d*>] by RVSUM_1:96; :: thesis: verum
end;
hence S3[fp ^ <*d*>] ; :: thesis: verum
end;
A16: S3[ <*> NAT]
proof
take <*> NAT ; :: thesis: ( <*> NAT = <*> NAT & ( S1[ <*> NAT] implies S2[ <*> NAT] ) )
thus ( <*> NAT = <*> NAT & ( S1[ <*> NAT] implies S2[ <*> NAT] ) ) by NAT_D:6, RVSUM_1:94; :: thesis: verum
end;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A16, A1);
 then ex f being FinSequence of NAT st
( f = fp & ( S1[f] implies S2[f] ) ) ;
hence ( ( 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 ) & ( for b being Element of NAT st b in dom fp holds
fp . b divides a ) implies Product fp divides a ) ; :: thesis: verum