let b, m be FinSequence of INT ; :: thesis: ( 2 <= len b & ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_coprime ) & m . 1 = 1 implies for k being Nat st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_coprime )

assume 2 <= len b ; :: thesis: ( ex i, j being Nat st
( i in Seg (len b) & j in Seg (len b) & i <> j & not b . i,b . j are_coprime ) or not m . 1 = 1 or for k being Nat st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_coprime )

assume A1: ( ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_coprime ) & m . 1 = 1 ) ; :: thesis: for k being Nat st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_coprime

defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= \$1 holds
m . (i + 1) = (m . i) * (b . i) ) implies for j being Nat st \$1 + 1 <= j & j <= len b holds
m . (\$1 + 1),b . j are_coprime );
reconsider I0 = 0 as Element of NAT ;
A2: S1[ 0 ] ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
assume A5: ( 1 <= k + 1 & k + 1 <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k + 1 holds
m . (i + 1) = (m . i) * (b . i) ) ) ; :: thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime

A6: k <= k + 1 by NAT_1:12;
per cases ( k = 0 or k <> 0 ) ;
suppose A7: k = 0 ; :: thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime

A8: m . ((k + 1) + 1) = (m . 1) * (b . 1) by A5, A7
.= b . 1 by A1 ;
for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime
proof
let j be Nat; :: thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_coprime )
assume A9: ( (k + 1) + 1 <= j & j <= len b ) ; :: thesis: m . ((k + 1) + 1),b . j are_coprime
then A10: ( 1 <= j & j <= len b ) by ;
then A11: j in Seg (len b) ;
( 1 <= 1 & 1 <= len b ) by ;
then A12: 1 in Seg (len b) ;
1 <> j by A9, A7;
hence m . ((k + 1) + 1),b . j are_coprime by A8, A1, A11, A12; :: thesis: verum
end;
hence for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime ; :: thesis: verum
end;
suppose A13: k <> 0 ; :: thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime

A14: now :: thesis: for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i)
let i be Nat; :: thesis: ( 1 <= i & i <= k implies m . (i + 1) = (m . i) * (b . i) )
assume ( 1 <= i & i <= k ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)
then ( 1 <= i & i <= k + 1 ) by NAT_1:12;
hence m . (i + 1) = (m . i) * (b . i) by A5; :: thesis: verum
end;
thus for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_coprime :: thesis: verum
proof
let j be Nat; :: thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_coprime )
assume A15: ( (k + 1) + 1 <= j & j <= len b ) ; :: thesis: m . ((k + 1) + 1),b . j are_coprime
k + 1 <= (k + 1) + 1 by NAT_1:12;
then A16: ( k + 1 <= j & j <= len b ) by ;
then A17: m . (k + 1),b . j are_coprime by ;
A18: 1 <= k + 1 by NAT_1:12;
k + 1 <= len b by ;
then A19: k + 1 in Seg (len b) by A18;
( 1 <= j & j <= len b ) by ;
then A20: j in Seg (len b) ;
k + 1 < j by ;
then A21: b . (k + 1),b . j are_coprime by A1, A19, A20;
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by A5;
hence m . ((k + 1) + 1),b . j are_coprime by ; :: thesis: verum
end;
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
hence for k being Nat st 1 <= k & k <= (len b) - 1 & ( for i being Nat st 1 <= i & i <= k holds
m . (i + 1) = (m . i) * (b . i) ) holds
for j being Nat st k + 1 <= j & j <= len b holds
m . (k + 1),b . j are_coprime ; :: thesis: verum