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_relative_prime ) & m . 1 = 1 implies for k being Element of 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_relative_prime )
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_relative_prime ) or not m . 1 = 1 or for k being Element of 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_relative_prime )
assume A2: ( ( for i, j being Nat st i in Seg (len b) & j in Seg (len b) & i <> j holds
b . i,b . j are_relative_prime ) & m . 1 = 1 ) ; :: thesis: for k being Element of 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_relative_prime
defpred S₁[ 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_relative_prime );
reconsider I0 = 0 as Element of NAT ;
P0: S₁[ 0 ] ;
P1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume P11: S₁[k] ; :: thesis: S₁[k + 1]
assume P12: ( 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_relative_prime
P14: k <= k + 1 by NAT_1:12;

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

suppose P15: k = 0 ; :: thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime

P16: m . ((k + 1) + 1) = (m . 1) * (b . 1) by P12, P15
.= b . 1 by A2 ;
for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime

proof

let j be Nat; :: thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime )
assume XX0: ( (k + 1) + 1 <= j & j <= len b ) ; :: thesis: m . ((k + 1) + 1),b . j are_relative_prime
then XX2: ( 1 <= j & j <= len b ) by XXREAL_0:2, P15;
then XX1: j in Seg (len b) by FINSEQ_1:1;
( 1 <= 1 & 1 <= len b ) by XXREAL_0:2, XX2;
then XX3: 1 in Seg (len b) ;
1 <> j by XX0, P15;
hence m . ((k + 1) + 1),b . j are_relative_prime by P16, A2, XX1, XX3; :: thesis: verum

end;

hence for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime ; :: thesis: verum

end;

suppose P19: k <> 0 ; :: thesis: for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime

P20: 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 P12; :: thesis: verum

end;

thus for j being Nat st (k + 1) + 1 <= j & j <= len b holds
m . ((k + 1) + 1),b . j are_relative_prime :: thesis: verum

proof

let j be Nat; :: thesis: ( (k + 1) + 1 <= j & j <= len b implies m . ((k + 1) + 1),b . j are_relative_prime )
assume XX6: ( (k + 1) + 1 <= j & j <= len b ) ; :: thesis: m . ((k + 1) + 1),b . j are_relative_prime
k + 1 <= (k + 1) + 1 by NAT_1:12;
then XX1: ( k + 1 <= j & j <= len b ) by XX6, XXREAL_0:2;
then P21: m . (k + 1),b . j are_relative_prime by P20, P11, P12, P14, XXREAL_0:2, NAT_1:14, P19;
XX2: 1 <= k + 1 by NAT_1:12;
k + 1 <= len b by XX1, XXREAL_0:2;
then XX3: k + 1 in Seg (len b) by XX2;
( 1 <= j & j <= len b ) by XX1, XX2, XXREAL_0:2;
then XX4: j in Seg (len b) by FINSEQ_1:1;
k + 1 < j by XX6, XXREAL_0:2, NAT_1:16;
then P23: b . (k + 1),b . j are_relative_prime by A2, XX3, XX4;
m . ((k + 1) + 1) = (m . (k + 1)) * (b . (k + 1)) by P12;
hence m . ((k + 1) + 1),b . j are_relative_prime by P23, P21, INT_2:26; :: thesis: verum

end;

end;

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P0, P1);
hence for k being Element of 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_relative_prime ; :: thesis: verum