defpred S1[ 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 ;
A3: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
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
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
b5,b3 . b4 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
b5,b3 . b4 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
b4,b2 . b3 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
b4,b2 . b3 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 b3,b1 . b2 are_coprime )
assume A12: mm = (Product m) / (m . i9) ; :: thesis: b3,b1 . b2 are_coprime
per cases ( k > 0 or k = 0 ) ;
suppose k > 0 ; :: thesis: b3,b1 . b2 are_coprime
then reconsider m1 = m | k as CR_Sequence by A5, Th24, NAT_1:11;
per cases ( i in dom m1 or not i in dom m1 ) ;
suppose A13: i in dom m1 ; :: thesis: b3,b1 . b2 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 ;
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;
suppose A17: not i in dom m1 ; :: thesis: b3,b1 . b2 are_coprime
m . (k + 1) in rng m by A8, FUNCT_1:3;
then A18: m . (k + 1) > 0 by PARTFUN3:def 1;
defpred S2[ 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;
A20: now :: thesis: for j being Element of NAT st 0 <= j & j < len m1 & S2[j] holds
S2[j + 1]
let j be Element of NAT ; :: thesis: ( 0 <= j & j < len m1 & S2[j] implies S2[j + 1] )
assume that
0 <= j and
A21: j < len m1 ; :: thesis: ( S2[j] implies S2[j + 1] )
assume A22: S2[j] ; :: thesis: S2[j + 1]
now :: thesis: ( j + 1 <= len m1 implies S2[j + 1] )
assume A23: j + 1 <= len m1 ; :: thesis: S2[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;
now :: thesis: for s being Element of NAT st s = j + 1 holds
Product (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;
hence S2[j + 1] ; :: thesis: verum
end;
hence S2[j + 1] ; :: thesis: verum
end;
m1 | 0 is empty ;
then A32: S2[ 0 ] by RVSUM_1:94, WSIERP_1:9;
A33: for j being Element of NAT st 0 <= j & j <= len m1 holds
S2[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;
end;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A39: S1[ 0 ] ;
A40: for k being Nat holds S1[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