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 S_{1}[ 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: S_{1}[ 0 ]
;

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

S_{1}[k + 1]
_{1}[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

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 S

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

A3: for k being Nat st S

S

proof

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

assume A4: S_{1}[k]
; :: thesis: S_{1}[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;

end;assume A4: S

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

end;

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

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

m . ((k + 1) + 1),b . j are_coprime ; :: thesis: verum

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

hence
for j being Nat st (k + 1) + 1 <= j & j <= len b holds
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 A7, XXREAL_0:2;

then A11: j in Seg (len b) ;

( 1 <= 1 & 1 <= len b ) by A10, XXREAL_0:2;

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;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 A7, XXREAL_0:2;

then A11: j in Seg (len b) ;

( 1 <= 1 & 1 <= len b ) by A10, XXREAL_0:2;

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

m . ((k + 1) + 1),b . j are_coprime ; :: thesis: verum

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

m . ((k + 1) + 1),b . j are_coprime :: thesis: verumend;

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)

thus
for j being Nat st (k + 1) + 1 <= j & j <= len b 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;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

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 A15, XXREAL_0:2;

then A17: m . (k + 1),b . j are_coprime by A14, A4, A5, A6, A13, NAT_1:14, XXREAL_0:2;

A18: 1 <= k + 1 by NAT_1:12;

k + 1 <= len b by A16, XXREAL_0:2;

then A19: k + 1 in Seg (len b) by A18;

( 1 <= j & j <= len b ) by A16, A18, XXREAL_0:2;

then A20: j in Seg (len b) ;

k + 1 < j by A15, NAT_1:16, XXREAL_0:2;

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 A21, A17, INT_2:26; :: thesis: verum

end;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 A15, XXREAL_0:2;

then A17: m . (k + 1),b . j are_coprime by A14, A4, A5, A6, A13, NAT_1:14, XXREAL_0:2;

A18: 1 <= k + 1 by NAT_1:12;

k + 1 <= len b by A16, XXREAL_0:2;

then A19: k + 1 in Seg (len b) by A18;

( 1 <= j & j <= len b ) by A16, A18, XXREAL_0:2;

then A20: j in Seg (len b) ;

k + 1 < j by A15, NAT_1:16, XXREAL_0:2;

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 A21, A17, INT_2:26; :: thesis: verum

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