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 S_{1}[ 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 S_{2}[ 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 S_{3}[ set ] means ex f being FinSequence of NAT st

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

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

then ex f being FinSequence of NAT st

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

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

(Product (Del ($1,b))) gcd ($1 . b) = 1;

defpred S

($1 . b) gcd ($1 . c) = 1;

defpred S

( f = $1 & ( len f >= 2 & 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*>]

A27:
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 k = len fp;

set fp1 = fp ^ <*d*>;

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

end;S

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

assume A2: S

set k = len fp;

set fp1 = fp ^ <*d*>;

now :: thesis: ( len (fp ^ <*d*>) >= 2 & S_{2}[fp ^ <*d*>] implies S_{1}[fp ^ <*d*>] )

hence
Sassume that

A3: len (fp ^ <*d*>) >= 2 and

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

A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16;

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

end;A3: len (fp ^ <*d*>) >= 2 and

A4: S

A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16;

now :: thesis: S_{1}[fp ^ <*d*>]end;

hence
Sper cases
( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 )
by A3, XXREAL_0:1;

end;

suppose A6:
len (fp ^ <*d*>) = 2
; :: thesis: S_{1}[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_{1}[fp ^ <*d*>]
; :: thesis: verum

end;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

hence
S
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;

end;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;

end;

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

(fp . a) gcd d = 1

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_{1}[fp ^ <*d*>]
; :: thesis: verum

end;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: S

proof

A16:
for a being Nat st a in dom fp holds
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;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

(fp . a) gcd d = 1

proof

reconsider n = n as Element of NAT by ORDINAL1:def 12;
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;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

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

hence
S
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;

end;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;

end;

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;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

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;.= (Product fp) gcd d by WSIERP_1:40

.= 1 by A16, WSIERP_1:36 ;

:: thesis: verum

proof

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

thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S_{2}[ <*> NAT] implies S_{1}[ <*> NAT] ) )
; :: thesis: verum

end;thus ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S

then ex f being FinSequence of NAT st

( f = fp & ( len f >= 2 & S

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