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 S_{1}[ 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 S_{2}[ FinSequence of NAT ] means Product $1 divides a;

defpred S_{3}[ set ] means ex f being FinSequence of NAT st

( f = $1 & ( S_{1}[f] implies S_{2}[f] ) );

_{3}[ <*> NAT]
_{3}[fp]
from FINSEQ_2:sch 2(A16, A1);

then ex f being FinSequence of NAT st

( f = fp & ( S_{1}[f] implies S_{2}[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

(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 S

($1 . b) gcd ($1 . c) = 1 ) & ( for b being Element of NAT st b in dom $1 holds

$1 . b divides a ) );

defpred S

defpred S

( f = $1 & ( S

A1: now :: thesis: for fp being FinSequence of NAT

for d being Element of NAT st S_{3}[fp] holds

S_{3}[fp ^ <*d*>]

A16:
Sfor d being Element of NAT st S

S

let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S_{3}[fp] holds

S_{3}[fp ^ <*d*>]

let d be Element of NAT ; :: thesis: ( S_{3}[fp] implies S_{3}[fp ^ <*d*>] )

assume A2: S_{3}[fp]
; :: thesis: S_{3}[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;

_{3}[fp ^ <*d*>]
; :: thesis: verum

end;S

let d be Element of NAT ; :: thesis: ( S

assume A2: S

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: ( S_{1}[fp ^ <*d*>] implies S_{2}[fp ^ <*d*>] )

hence
Sassume A4:
S_{1}[fp ^ <*d*>]
; :: thesis: S_{2}[fp ^ <*d*>]

for a being Nat st a in dom fp holds

(fp . a) gcd d = 1

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

fp . b divides a

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 S_{2}[fp ^ <*d*>]
by RVSUM_1:96; :: thesis: verum

end;for a being Nat st a in dom fp holds

(fp . a) gcd d = 1

proof

then
(Product fp) gcd d = 1
by WSIERP_1:36;
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;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

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

A14:
for b being Element of NAT st b in dom fp holds
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;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

fp . b divides a

proof

len (fp ^ <*d*>) in dom (fp ^ <*d*>)
by FINSEQ_5:6;
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;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

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 S

proof

for fp being FinSequence of NAT holds S
take
<*> NAT
; :: thesis: ( <*> NAT = <*> NAT & ( S_{1}[ <*> NAT] implies S_{2}[ <*> NAT] ) )

thus ( <*> NAT = <*> NAT & ( S_{1}[ <*> NAT] implies S_{2}[ <*> NAT] ) )
by NAT_D:6, RVSUM_1:94; :: thesis: verum

end;thus ( <*> NAT = <*> NAT & ( S

then ex f being FinSequence of NAT st

( f = fp & ( S

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