let b, m be FinSequence of INT ; :: thesis: ( len b = len m & 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 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 )
assume len b = len m ; :: thesis: ( 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 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 )
assume A1: 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 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0
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 <= j & j <= $1 holds
(m . ($1 + 1)) mod (b . j) = 0 );
reconsider I0 = 0 as Element of NAT ;
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0
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 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0

A8: m . ((k + 1) + 1) = (m . 1) * (b . 1) by A5, A7
.= b . 1 by A1 ;
for j being Nat st 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0

proof

let j be Nat; :: thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 )
assume ( 1 <= j & j <= k + 1 ) ; :: thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
then j = 1 by A7, XXREAL_0:1;
hence (m . ((k + 1) + 1)) mod (b . j) = 0 by A8, INT_1:50; :: thesis: verum

end;

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

end;

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

A9: 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 1 <= j & j <= k + 1 holds
(m . ((k + 1) + 1)) mod (b . j) = 0 :: thesis: verum

proof

let j be Nat; :: thesis: ( 1 <= j & j <= k + 1 implies (m . ((k + 1) + 1)) mod (b . j) = 0 )
assume A10: ( 1 <= j & j <= k + 1 ) ; :: thesis: (m . ((k + 1) + 1)) mod (b . j) = 0
reconsider bj = b . j as Element of INT by INT_1:def 2;

per cases ( j = k + 1 or j <> k + 1 ) ;

suppose A11: j = k + 1 ; :: thesis: (m . ((k + 1) + 1)) mod (b . j) = 0

thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by A5
.= (((m . (k + 1)) mod (b . j)) * ((b . (k + 1)) mod (b . j))) mod (b . j) by NAT_D:67
.= (((m . (k + 1)) mod (b . j)) * 0) mod (b . j) by A11, INT_1:50
.= 0 by INT_1:73 ; :: thesis: verum

end;

suppose j <> k + 1 ; :: thesis: (m . ((k + 1) + 1)) mod (b . j) = 0

then j < k + 1 by A10, XXREAL_0:1;
then A12: j <= k by NAT_1:13;
thus (m . ((k + 1) + 1)) mod (b . j) = ((m . (k + 1)) * (b . (k + 1))) mod (b . j) by A5
.= (((m . (k + 1)) mod (b . j)) * ((b . (k + 1)) mod (b . j))) mod (b . j) by NAT_D:67
.= (0 * ((b . (k + 1)) mod (b . j))) mod (b . j) by A12, A9, A10, A4, A5, A6, XXREAL_0:2
.= 0 by INT_1:73 ; :: thesis: verum

end;

end;

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
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 1 <= j & j <= k holds
(m . (k + 1)) mod (b . j) = 0 ; :: thesis: verum