defpred S_{1}[ Nat] means for m being CR_Sequence st len m = $1 holds

for i being Nat st i in dom m holds

for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime ;

let m be CR_Sequence; :: thesis: for i being Nat st i in dom m holds

for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime

let i be Nat; :: thesis: ( i in dom m implies for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime )

assume A1: i in dom m ; :: thesis: for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime

let mm be Integer; :: thesis: ( mm = (Product m) / (m . i) implies mm,m . i are_coprime )

A2: ex l being Element of NAT st len m = l ;

_{1}[ 0 ]
;

A40: for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A39, A3);

assume mm = (Product m) / (m . i) ; :: thesis: mm,m . i are_coprime

hence mm,m . i are_coprime by A1, A40, A2; :: thesis: verum

for i being Nat st i in dom m holds

for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime ;

let m be CR_Sequence; :: thesis: for i being Nat st i in dom m holds

for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime

let i be Nat; :: thesis: ( i in dom m implies for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime )

assume A1: i in dom m ; :: thesis: for mm being Integer st mm = (Product m) / (m . i) holds

mm,m . i are_coprime

let mm be Integer; :: thesis: ( mm = (Product m) / (m . i) implies mm,m . i are_coprime )

A2: ex l being Element of NAT st len m = l ;

A3: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A39:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

now :: thesis: for m being CR_Sequence st len m = k + 1 holds

for i9 being Nat st i9 in dom m holds

for mm being Integer st mm = (Product m) / (m . i9) holds

mm,m . i9 are_coprime

hence
Sfor i9 being Nat st i9 in dom m holds

for mm being Integer st mm = (Product m) / (m . i9) holds

mm,m . i9 are_coprime

let m be CR_Sequence; :: thesis: ( len m = k + 1 implies for i9 being Nat st i9 in dom m holds

for mm being Integer st mm = (Product m) / (m . i9) holds

b_{5},b_{3} . b_{4} are_coprime )

set m1 = m | k;

assume A5: len m = k + 1 ; :: thesis: for i9 being Nat st i9 in dom m holds

for mm being Integer st mm = (Product m) / (m . i9) holds

b_{5},b_{3} . b_{4} are_coprime

then A6: (m | k) ^ <*(m . (k + 1))*> = m | (k + 1) by Th5

.= m by A5, FINSEQ_1:58 ;

A7: len (m | k) = k by A5, FINSEQ_1:59, NAT_1:11;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (k + 1) ;

then A8: k + 1 in dom m by A5, FINSEQ_1:def 3;

let i9 be Nat; :: thesis: ( i9 in dom m implies for mm being Integer st mm = (Product m) / (m . i9) holds

b_{4},b_{2} . b_{3} are_coprime )

reconsider i = i9 as Element of NAT by ORDINAL1:def 12;

assume A9: i9 in dom m ; :: thesis: for mm being Integer st mm = (Product m) / (m . i9) holds

b_{4},b_{2} . b_{3} are_coprime

then A10: i in Seg (k + 1) by A5, FINSEQ_1:def 3;

then A11: i <= k + 1 by FINSEQ_1:1;

let mm be Integer; :: thesis: ( mm = (Product m) / (m . i9) implies b_{3},b_{1} . b_{2} are_coprime )

assume A12: mm = (Product m) / (m . i9) ; :: thesis: b_{3},b_{1} . b_{2} are_coprime

end;for mm being Integer st mm = (Product m) / (m . i9) holds

b

set m1 = m | k;

assume A5: len m = k + 1 ; :: thesis: for i9 being Nat st i9 in dom m holds

for mm being Integer st mm = (Product m) / (m . i9) holds

b

then A6: (m | k) ^ <*(m . (k + 1))*> = m | (k + 1) by Th5

.= m by A5, FINSEQ_1:58 ;

A7: len (m | k) = k by A5, FINSEQ_1:59, NAT_1:11;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (k + 1) ;

then A8: k + 1 in dom m by A5, FINSEQ_1:def 3;

let i9 be Nat; :: thesis: ( i9 in dom m implies for mm being Integer st mm = (Product m) / (m . i9) holds

b

reconsider i = i9 as Element of NAT by ORDINAL1:def 12;

assume A9: i9 in dom m ; :: thesis: for mm being Integer st mm = (Product m) / (m . i9) holds

b

then A10: i in Seg (k + 1) by A5, FINSEQ_1:def 3;

then A11: i <= k + 1 by FINSEQ_1:1;

let mm be Integer; :: thesis: ( mm = (Product m) / (m . i9) implies b

assume A12: mm = (Product m) / (m . i9) ; :: thesis: b

per cases
( k > 0 or k = 0 )
;

end;

suppose
k > 0
; :: thesis: b_{3},b_{1} . b_{2} are_coprime

then reconsider m1 = m | k as CR_Sequence by A5, Th24, NAT_1:11;

end;per cases
( i in dom m1 or not i in dom m1 )
;

end;

suppose A13:
i in dom m1
; :: thesis: b_{3},b_{1} . b_{2} are_coprime

then
i in Seg k
by A7, FINSEQ_1:def 3;

then i <= k by FINSEQ_1:1;

then i <> k + 1 by NAT_1:13;

then A14: m . i,m . (k + 1) are_coprime by A9, A8, Def2;

reconsider mm1 = (Product m1) / (m1 . i) as Integer by A13, Th9;

A15: m1 . i = m . i by A13, FUNCT_1:47;

then mm1,m . i are_coprime by A4, A7, A13;

then A16: (m . i) gcd (mm1 * (m . (k + 1))) = (m . i) gcd (m . (k + 1)) by Th19

.= 1 by A14 ;

mm1 * (m . (k + 1)) = ((Product m1) * (m . (k + 1))) * ((m . i) ") by A15

.= mm by A12, A6, RVSUM_1:96 ;

hence mm,m . i9 are_coprime by A16; :: thesis: verum

end;then i <= k by FINSEQ_1:1;

then i <> k + 1 by NAT_1:13;

then A14: m . i,m . (k + 1) are_coprime by A9, A8, Def2;

reconsider mm1 = (Product m1) / (m1 . i) as Integer by A13, Th9;

A15: m1 . i = m . i by A13, FUNCT_1:47;

then mm1,m . i are_coprime by A4, A7, A13;

then A16: (m . i) gcd (mm1 * (m . (k + 1))) = (m . i) gcd (m . (k + 1)) by Th19

.= 1 by A14 ;

mm1 * (m . (k + 1)) = ((Product m1) * (m . (k + 1))) * ((m . i) ") by A15

.= mm by A12, A6, RVSUM_1:96 ;

hence mm,m . i9 are_coprime by A16; :: thesis: verum

suppose A17:
not i in dom m1
; :: thesis: b_{3},b_{1} . b_{2} are_coprime

m . (k + 1) in rng m
by A8, FUNCT_1:3;

then A18: m . (k + 1) > 0 by PARTFUN3:def 1;

defpred S_{2}[ Nat] means ( $1 <= len m1 implies for s being Element of NAT st s = $1 holds

Product (m1 | s),m . (k + 1) are_coprime );

A19: m1 | (len m1) = m1 by FINSEQ_1:58;

then A32: S_{2}[ 0 ]
by RVSUM_1:94, WSIERP_1:9;

A33: for j being Element of NAT st 0 <= j & j <= len m1 holds

S_{2}[j]
from INT_1:sch 7(A32, A20);

not i in Seg k by A7, A17, FINSEQ_1:def 3;

then ( not 1 <= i or not i <= k ) ;

then not i < k + 1 by A10, FINSEQ_1:1, NAT_1:13;

then A34: i = k + 1 by A11, XXREAL_0:1;

then mm = ((Product m1) * (m . (k + 1))) * ((m . (k + 1)) ") by A12, A6, RVSUM_1:96

.= (Product m1) * ((m . (k + 1)) * ((m . (k + 1)) "))

.= (Product m1) * 1 by A18, XCMPLX_0:def 7 ;

hence mm,m . i9 are_coprime by A34, A33, A19; :: thesis: verum

end;then A18: m . (k + 1) > 0 by PARTFUN3:def 1;

defpred S

Product (m1 | s),m . (k + 1) are_coprime );

A19: m1 | (len m1) = m1 by FINSEQ_1:58;

A20: now :: thesis: for j being Element of NAT st 0 <= j & j < len m1 & S_{2}[j] holds

S_{2}[j + 1]

m1 | 0 is empty
;S

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len m1 & S_{2}[j] implies S_{2}[j + 1] )

assume that

0 <= j and

A21: j < len m1 ; :: thesis: ( S_{2}[j] implies S_{2}[j + 1] )

assume A22: S_{2}[j]
; :: thesis: S_{2}[j + 1]

_{2}[j + 1]
; :: thesis: verum

end;assume that

0 <= j and

A21: j < len m1 ; :: thesis: ( S

assume A22: S

now :: thesis: ( j + 1 <= len m1 implies S_{2}[j + 1] )

hence
Sassume A23:
j + 1 <= len m1
; :: thesis: S_{2}[j + 1]

A24: 0 + 1 <= j + 1 by XREAL_1:6;

then j + 1 in Seg (len m1) by A23;

then A25: j + 1 in dom m1 by FINSEQ_1:def 3;

j + 1 <= len m by A5, A7, A21, XREAL_1:8;

then j + 1 in Seg (len m) by A24;

then A26: j + 1 in dom m by FINSEQ_1:def 3;

j + 1 <= k by A5, A23, FINSEQ_1:59, NAT_1:11;

then A27: j + 1 <> k + 1 by NAT_1:13;

_{2}[j + 1]
; :: thesis: verum

end;A24: 0 + 1 <= j + 1 by XREAL_1:6;

then j + 1 in Seg (len m1) by A23;

then A25: j + 1 in dom m1 by FINSEQ_1:def 3;

j + 1 <= len m by A5, A7, A21, XREAL_1:8;

then j + 1 in Seg (len m) by A24;

then A26: j + 1 in dom m by FINSEQ_1:def 3;

j + 1 <= k by A5, A23, FINSEQ_1:59, NAT_1:11;

then A27: j + 1 <> k + 1 by NAT_1:13;

now :: thesis: for s being Element of NAT st s = j + 1 holds

Product (m1 | s),m . (k + 1) are_coprime

hence
SProduct (m1 | s),m . (k + 1) are_coprime

reconsider s9 = j as Element of NAT ;

let s be Element of NAT ; :: thesis: ( s = j + 1 implies Product (m1 | s),m . (k + 1) are_coprime )

A28: m1 . (j + 1) = m . (j + 1) by A25, FUNCT_1:47;

A29: m . (j + 1),m . (k + 1) are_coprime by A8, A27, A26, Def2;

j <= j + 1 by NAT_1:11;

then Product (m1 | s9),m . (k + 1) are_coprime by A22, A23, XXREAL_0:2;

then A30: ((Product (m1 | s9)) * (m . (j + 1))) gcd (m . (k + 1)) = (m . (j + 1)) gcd (m . (k + 1)) by Th19

.= 1 by A29 ;

assume A31: s = j + 1 ; :: thesis: Product (m1 | s),m . (k + 1) are_coprime

then (m1 | s9) ^ <*(m1 . s)*> = m1 | s by A23, Th5;

then (Product (m1 | s)) gcd (m . (k + 1)) = 1 by A31, A30, A28, RVSUM_1:96;

hence Product (m1 | s),m . (k + 1) are_coprime ; :: thesis: verum

end;let s be Element of NAT ; :: thesis: ( s = j + 1 implies Product (m1 | s),m . (k + 1) are_coprime )

A28: m1 . (j + 1) = m . (j + 1) by A25, FUNCT_1:47;

A29: m . (j + 1),m . (k + 1) are_coprime by A8, A27, A26, Def2;

j <= j + 1 by NAT_1:11;

then Product (m1 | s9),m . (k + 1) are_coprime by A22, A23, XXREAL_0:2;

then A30: ((Product (m1 | s9)) * (m . (j + 1))) gcd (m . (k + 1)) = (m . (j + 1)) gcd (m . (k + 1)) by Th19

.= 1 by A29 ;

assume A31: s = j + 1 ; :: thesis: Product (m1 | s),m . (k + 1) are_coprime

then (m1 | s9) ^ <*(m1 . s)*> = m1 | s by A23, Th5;

then (Product (m1 | s)) gcd (m . (k + 1)) = 1 by A31, A30, A28, RVSUM_1:96;

hence Product (m1 | s),m . (k + 1) are_coprime ; :: thesis: verum

then A32: S

A33: for j being Element of NAT st 0 <= j & j <= len m1 holds

S

not i in Seg k by A7, A17, FINSEQ_1:def 3;

then ( not 1 <= i or not i <= k ) ;

then not i < k + 1 by A10, FINSEQ_1:1, NAT_1:13;

then A34: i = k + 1 by A11, XXREAL_0:1;

then mm = ((Product m1) * (m . (k + 1))) * ((m . (k + 1)) ") by A12, A6, RVSUM_1:96

.= (Product m1) * ((m . (k + 1)) * ((m . (k + 1)) "))

.= (Product m1) * 1 by A18, XCMPLX_0:def 7 ;

hence mm,m . i9 are_coprime by A34, A33, A19; :: thesis: verum

suppose
k = 0
; :: thesis: b_{3},b_{1} . b_{2} are_coprime

then A35:
m = <*(m . 1)*>
by A5, FINSEQ_1:40;

then A36: dom m = Seg 1 by FINSEQ_1:38;

then A37: i <= 1 by A9, FINSEQ_1:1;

1 <= i by A9, A36, FINSEQ_1:1;

then A38: i = 1 by A37, XXREAL_0:1;

Product m = m . 1 by A35;

then mm = 1 by A12, A38, XCMPLX_0:def 7;

hence mm,m . i9 are_coprime by WSIERP_1:9; :: thesis: verum

end;then A36: dom m = Seg 1 by FINSEQ_1:38;

then A37: i <= 1 by A9, FINSEQ_1:1;

1 <= i by A9, A36, FINSEQ_1:1;

then A38: i = 1 by A37, XXREAL_0:1;

Product m = m . 1 by A35;

then mm = 1 by A12, A38, XCMPLX_0:def 7;

hence mm,m . i9 are_coprime by WSIERP_1:9; :: thesis: verum

A40: for k being Nat holds S

assume mm = (Product m) / (m . i) ; :: thesis: mm,m . i are_coprime

hence mm,m . i are_coprime by A1, A40, A2; :: thesis: verum