reconsider n2 = n, m2 = m as Element of NAT by A1, A2, INT_1:3;
per cases ( n < m or n >= m ) ;
suppose A3: n < m ; :: thesis: ex b1 being Integer ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) )
set ssm = (Seg (n2 + 1)) --> 1;
A4: dom ((Seg (n2 + 1)) --> 1) = Seg (n2 + 1) by FUNCOP_1:13;
then reconsider ssm = (Seg (n2 + 1)) --> 1 as FinSequence by FINSEQ_1:def 2;
A5: rng ssm c= {1} by FUNCOP_1:13;
rng ssm c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ssm or y in INT )
assume y in rng ssm ; :: thesis: y in INT
then y = 1 by A5, TARSKI:def 1;
hence y in INT by INT_1:def 2; :: thesis: verum
end;
then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def 4;
len ssm = n + 1 by A4, FINSEQ_1:def 3;
hence ex b1 being Integer ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) ) by A3; :: thesis: verum
end;
suppose A6: n >= m ; :: thesis: ex b1 being Integer ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) )
deffunc H1( Nat) -> Element of NAT = n2 div (m2 * (2 |^ ($1 -' 1)));
A7: m2 * (2 |^ 0) = m2 * 1 by NEWTON:4
.= m2 ;
ex ppn being FinSequence st
( len ppn = n2 + 1 & ( for k2 being Nat st k2 in dom ppn holds
ppn . k2 = H1(k2) ) ) from FINSEQ_1:sch 2();
then consider ppn being FinSequence such that
A8: len ppn = n + 1 and
A9: for k2 being Nat st k2 in dom ppn holds
ppn . k2 = n2 div (m2 * (2 |^ (k2 -' 1))) ;
A10: dom ppn = Seg (n2 + 1) by A8, FINSEQ_1:def 3;
rng ppn c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ppn or y in INT )
assume y in rng ppn ; :: thesis: y in INT
then consider x being object such that
A11: x in dom ppn and
A12: y = ppn . x by FUNCT_1:def 3;
reconsider n3 = x as Element of NAT by A11;
ppn . n3 = n2 div (m2 * (2 |^ (n3 -' 1))) by A9, A11;
hence y in INT by A12, INT_1:def 2; :: thesis: verum
end;
then reconsider ppn = ppn as FinSequence of INT by FINSEQ_1:def 4;
n2 >= 0 + 1 by A2, A6, NAT_1:13;
then 1 < n2 + 1 by NAT_1:13;
then A13: 1 in Seg (n2 + 1) by FINSEQ_1:1;
then A14: ppn . 1 = n2 div (m2 * (2 |^ (1 -' 1))) by A9, A10
.= n2 div m2 by A7, XREAL_1:232 ;
deffunc H2( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1)));
deffunc H3( Nat) -> Element of NAT = m2 * (2 |^ ($1 -' 1));
ex ssm being FinSequence st
( len ssm = n2 + 1 & ( for k2 being Nat st k2 in dom ssm holds
ssm . k2 = H3(k2) ) ) from FINSEQ_1:sch 2();
then consider ssm being FinSequence such that
A15: len ssm = n2 + 1 and
A16: for k2 being Nat st k2 in dom ssm holds
ssm . k2 = m * (2 |^ (k2 -' 1)) ;
A17: dom ssm = Seg (n2 + 1) by A15, FINSEQ_1:def 3;
A18: rng ssm c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ssm or y in INT )
assume y in rng ssm ; :: thesis: y in INT
then consider x being object such that
A19: x in dom ssm and
A20: y = ssm . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A19;
ssm . n = m * (2 |^ (n -' 1)) by A16, A19;
hence y in INT by A20, INT_1:def 2; :: thesis: verum
end;
ex ssn being FinSequence st
( len ssn = n2 + 1 & ( for k2 being Nat st k2 in dom ssn holds
ssn . k2 = H2(k2) ) ) from FINSEQ_1:sch 2();
then consider ssn being FinSequence such that
A21: len ssn = n2 + 1 and
A22: for k2 being Nat st k2 in dom ssn holds
ssn . k2 = n2 mod (m2 * (2 |^ (k2 -' 1))) ;
A23: dom ssn = Seg (n2 + 1) by A21, FINSEQ_1:def 3;
rng ssn c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ssn or y in INT )
assume y in rng ssn ; :: thesis: y in INT
then consider x being object such that
A24: x in dom ssn and
A25: y = ssn . x by FUNCT_1:def 3;
reconsider n3 = x as Element of NAT by A24;
ssn . n3 = n2 mod (m2 * (2 |^ (n3 -' 1))) by A22, A24;
hence y in INT by A25, INT_1:def 2; :: thesis: verum
end;
then reconsider ssn = ssn as FinSequence of INT by FINSEQ_1:def 4;
consider ii0 being Element of NAT such that
A26: for k2 being Element of NAT st k2 < ii0 holds
m * (2 |^ k2) <= n2 and
A27: m2 * (2 |^ ii0) > n2 by A2, Th6;
reconsider i0 = ii0 as Integer ;
A28: 0 + 1 <= i0 + 1 by XREAL_1:7;
now :: thesis: not i0 = 0
assume i0 = 0 ; :: thesis: contradiction
then m2 * 1 > n2 by A27, NEWTON:4;
hence contradiction by A6; :: thesis: verum
end;
then A29: ii0 >= 0 + 1 by NAT_1:13;
then A30: i0 - 1 >= 0 by XREAL_1:48;
A31: now :: thesis: not i0 > n2
1 + 0 <= m2 by A2, NAT_1:13;
then A32: 1 * (2 |^ n2) <= m2 * (2 |^ n2) by XREAL_1:64;
A33: n2 + 1 <= 2 |^ n2 by NEWTON:85;
assume i0 > n2 ; :: thesis: contradiction
then m * (2 |^ n2) <= n2 by A26;
then 2 |^ n2 <= n2 by A32, XXREAL_0:2;
hence contradiction by A33, NAT_1:13; :: thesis: verum
end;
then ( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 ) by NAT_1:11, XREAL_1:7;
then A34: ii0 + 1 in Seg (n2 + 1) by FINSEQ_1:1;
reconsider k5 = m2 * (2 |^ ((ii0 + 1) -' 1)) as Element of NAT ;
A35: k5 > n2 by A27, NAT_D:34;
i0 < n2 + 1 by A31, NAT_1:13;
then ii0 + 1 <= n2 + 1 by NAT_1:13;
then ii0 + 1 in Seg (n2 + 1) by A28, FINSEQ_1:1;
then ssn . (i0 + 1) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' 1))) by A22, A23;
then A36: ssn . (i0 + 1) = n by A35, NAT_D:24;
(ii0 + 1) -' 1 = (i0 - 1) + 1 by NAT_D:34
.= (ii0 -' 1) + 1 by A30, XREAL_0:def 2 ;
then A37: 2 |^ ((ii0 + 1) -' 1) = (2 |^ (ii0 -' 1)) * 2 by NEWTON:6;
A38: 1 <= i0 + 1 by A29, NAT_1:13;
reconsider ssm = ssm as FinSequence of INT by A18, FINSEQ_1:def 4;
A39: ssm . 1 = m * (2 |^ (1 -' 1)) by A13, A16, A17
.= m * (2 |^ 0) by XREAL_1:232
.= m * 1 by NEWTON:4
.= m ;
A40: (ii0 + 1) -' 1 = ii0 by NAT_D:34;
then n2 div (m2 * (2 |^ ((ii0 + 1) -' 1))) = 0 by A27, NAT_D:27;
then A41: ppn . (i0 + 1) = 0 by A9, A10, A34;
A42: for j being Integer st 1 <= j & j <= i0 holds
( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) )
proof
let j be Integer; :: thesis: ( 1 <= j & j <= i0 implies ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) ) )
assume that
A43: 1 <= j and
A44: j <= i0 ; :: thesis: ( ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) & ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) )
reconsider jj = j as Element of NAT by A43, INT_1:3;
A45: j - 1 >= 0 by A43, XREAL_1:48;
A46: i0 - j >= 0 by A44, XREAL_1:48;
then A47: ii0 -' jj = i0 - j by XREAL_0:def 2;
thus ( ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) ) :: thesis: ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) )
proof
ii0 < ii0 + 1 by NAT_1:13;
then j < i0 + 1 by A44, XXREAL_0:2;
then (i0 + 1) - j >= 0 by XREAL_1:48;
then A48: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;
i0 + 1 <= n2 + j by A31, A43, XREAL_1:7;
then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;
then A49: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A48, XREAL_1:7;
assume A50: ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; :: thesis: ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 )
( j + 1 <= i0 + 1 & j < j + 1 ) by A44, XREAL_1:7, XREAL_1:29;
then A51: j < i0 + 1 by XXREAL_0:2;
jj -' 1 <= j by NAT_D:35;
then jj -' 1 < i0 + 1 by A51, XXREAL_0:2;
then A52: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;
( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7;
then A53: j < i0 + 1 by XXREAL_0:2;
jj -' 1 <= jj by NAT_D:35;
then jj -' 1 < i0 + 1 by A53, XXREAL_0:2;
then A54: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;
2 |^ (ii0 -' jj) <> 0 by CARD_4:3;
then A55: m2 * (2 |^ (ii0 -' jj)) > m2 * 0 by A2, XREAL_1:68;
ii0 < ii0 + 1 by NAT_1:13;
then j < i0 + 1 by A44, XXREAL_0:2;
then A56: (i0 + 1) - j > 0 by XREAL_1:50;
then A57: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;
then A58: (ii0 + 1) -' jj >= 0 + 1 by A56, NAT_1:13;
then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;
then A59: ((ii0 + 1) -' jj) -' 1 = i0 - j by A57, XREAL_0:def 2;
( (ii0 + 1) -' jj <= i0 + 1 & i0 + 1 <= n2 + 1 ) by A31, NAT_D:35, XREAL_1:7;
then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;
then A60: (ii0 + 1) -' jj in Seg (n2 + 1) by A58, FINSEQ_1:1;
then A61: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A22, A23;
(ii0 + 1) -' jj = (i0 - j) + 1 by A56, XREAL_0:def 2;
then ((ii0 + 1) -' jj) - 1 >= 0 by A44, XREAL_1:48;
then A62: ((ii0 + 1) -' jj) -' 1 = i0 - j by A57, XREAL_0:def 2
.= ii0 -' jj by A46, XREAL_0:def 2 ;
then A63: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A16, A17, A60;
A64: jj -' 1 = j - 1 by A45, XREAL_0:def 2;
then A65: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A52, XREAL_0:def 2;
then A66: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A57, NAT_D:34;
1 <= (ii0 + 1) -' (jj -' 1) by A57, A65, NAT_1:11;
then A67: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A57, A65, A49, FINSEQ_1:1;
then A68: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1))) by A22, A23;
jj -' 1 = j - 1 by A45, XREAL_0:def 2;
then (ii0 + 1) -' (jj -' 1) = ((ii0 + 1) -' jj) + 1 by A57, A54, XREAL_0:def 2;
then A69: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by A68, NAT_D:34;
A70: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A64, A52, XREAL_0:def 2;
A71: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A47, A56, XREAL_0:def 2
.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6
.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;
(ii0 + 1) -' jj = (i0 + 1) - j by A56, XREAL_0:def 2;
then A72: (ssn . ((ii0 + 1) -' (jj -' 1))) - (ssm . ((ii0 + 1) -' jj)) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A50, A65, A69, A71, A63, A55, Th2;
ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A9, A10, A60
.= ((n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2) + 1 by A50, A57, A66, A70, A68, A62, A71, A63, A55, Th3
.= ((ppn . ((ii0 + 1) -' (jj -' 1))) * 2) + 1 by A9, A10, A67 ;
hence ( ssn . ((i0 + 1) - j) = (ssn . ((i0 + 1) - (j - 1))) - (ssm . ((i0 + 1) - j)) & ppn . ((i0 + 1) - j) = ((ppn . ((i0 + 1) - (j - 1))) * 2) + 1 ) by A57, A65, A59, A61, A72, XREAL_0:def 2; :: thesis: verum
end;
thus ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) :: thesis: verum
proof
( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7;
then A73: j < i0 + 1 by XXREAL_0:2;
jj -' 1 <= j by NAT_D:35;
then jj -' 1 < i0 + 1 by A73, XXREAL_0:2;
then A74: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;
( j + 1 <= i0 + 1 & jj < jj + 1 ) by A44, NAT_1:13, XREAL_1:7;
then A75: j < i0 + 1 by XXREAL_0:2;
jj -' 1 <= jj by NAT_D:35;
then jj -' 1 < i0 + 1 by A75, XXREAL_0:2;
then A76: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;
ii0 < ii0 + 1 by NAT_1:13;
then j < i0 + 1 by A44, XXREAL_0:2;
then (i0 + 1) - j >= 0 by XREAL_1:48;
then A77: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;
i0 + 1 <= n2 + j by A31, A43, XREAL_1:7;
then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;
then A78: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A77, XREAL_1:7;
assume A79: not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) ; :: thesis: ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 )
ii0 < ii0 + 1 by NAT_1:13;
then j < i0 + 1 by A44, XXREAL_0:2;
then A80: (i0 + 1) - j > 0 by XREAL_1:50;
then A81: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;
then A82: (ii0 + 1) -' jj >= 0 + 1 by A80, NAT_1:13;
then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;
then A83: ((ii0 + 1) -' jj) -' 1 = i0 - j by A81, XREAL_0:def 2;
( (ii0 + 1) -' jj <= ii0 + 1 & i0 + 1 <= n2 + 1 ) by A31, NAT_D:35, XREAL_1:7;
then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;
then A84: (ii0 + 1) -' jj in Seg (n2 + 1) by A82, FINSEQ_1:1;
then ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A22, A23;
then A85: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A83, XREAL_0:def 2;
(ii0 + 1) -' jj = (i0 - j) + 1 by A80, XREAL_0:def 2;
then ((ii0 + 1) -' jj) - 1 >= 0 by A44, XREAL_1:48;
then A86: ((ii0 + 1) -' jj) -' 1 = i0 - j by A81, XREAL_0:def 2
.= ii0 -' jj by A46, XREAL_0:def 2 ;
then A87: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A16, A17, A84;
A88: jj -' 1 = j - 1 by A45, XREAL_0:def 2;
then A89: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A76, XREAL_0:def 2;
then A90: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A81, NAT_D:34;
1 <= (ii0 + 1) -' (jj -' 1) by A81, A89, NAT_1:11;
then A91: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A81, A89, A78, FINSEQ_1:1;
then A92: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1))) by A22, A23;
jj -' 1 = j - 1 by A45, XREAL_0:def 2;
then (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A74, XREAL_0:def 2
.= ((ii0 + 1) -' jj) + 1 by A80, XREAL_0:def 2 ;
then A93: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by A92, NAT_D:34;
A94: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A88, A76, XREAL_0:def 2;
A95: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A47, A80, XREAL_0:def 2
.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6
.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;
ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A9, A10, A84
.= (n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2 by A79, A81, A90, A92, A94, A86, A95, A87, Th5
.= (ppn . ((ii0 + 1) -' (jj -' 1))) * 2 by A9, A10, A91 ;
hence ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) by A79, A81, A89, A85, A93, A95, A87, Th4; :: thesis: verum
end;
end;
A96: for k being Element of NAT st 1 <= k & k < i0 holds
( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )
proof
let k be Element of NAT ; :: thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) )
assume that
A97: 1 <= k and
A98: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )
A99: k <= n2 by A31, A98, XXREAL_0:2;
then A100: k + 1 <= n2 + 1 by XREAL_1:7;
k <= n2 + 1 by A99, NAT_1:12;
then k in Seg (n2 + 1) by A97, FINSEQ_1:1;
then A101: ssm . k = m * (2 |^ (k -' 1)) by A16, A17;
1 < k + 1 by A97, NAT_1:13;
then k + 1 in Seg (n2 + 1) by A100, FINSEQ_1:1;
then A102: ( (k + 1) -' 1 = k & ssm . (k + 1) = m * (2 |^ ((k + 1) -' 1)) ) by A16, A17, NAT_D:34;
A103: k - 1 >= 0 by A97, XREAL_1:48;
(k + 1) -' 1 = (k - 1) + 1 by NAT_D:34
.= (k -' 1) + 1 by A103, XREAL_0:def 2 ;
then 2 |^ ((k + 1) -' 1) = (2 |^ (k -' 1)) * 2 by NEWTON:6;
hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A26, A98, A102, A101; :: thesis: verum
end;
A104: for k being Integer st 1 <= k & k < i0 holds
( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )
proof
let k be Integer; :: thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) )
assume that
A105: 1 <= k and
A106: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )
reconsider kk = k as Element of NAT by A105, INT_1:3;
ssm . (kk + 1) = (ssm . kk) * 2 by A96, A105, A106;
hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A96, A105, A106; :: thesis: verum
end;
i0 < n2 + 1 by A31, NAT_1:13;
then A107: ii0 in Seg (n2 + 1) by A29, FINSEQ_1:1;
i0 + 1 <= n2 + 1 by A31, XREAL_1:7;
then ii0 + 1 in Seg (n2 + 1) by A38, FINSEQ_1:1;
then ssm . (i0 + 1) = m * (2 |^ ((ii0 + 1) -' 1)) by A16, A17;
then A108: ssm . (i0 + 1) = (m * (2 |^ (ii0 -' 1))) * 2 by A37
.= (ssm . i0) * 2 by A16, A17, A107 ;
ssm . (i0 + 1) > n by A16, A17, A27, A40, A34;
hence ex b1 being Integer ex sm, sn, pn being FinSequence of INT st
( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b1 = 0 ) & ( not n < m implies ( sm . 1 = m & ex i being Integer st
( 1 <= i & i <= n & ( for k being Integer st 1 <= k & k < i holds
( sm . (k + 1) = (sm . k) * 2 & not sm . (k + 1) > n ) ) & sm . (i + 1) = (sm . i) * 2 & sm . (i + 1) > n & pn . (i + 1) = 0 & sn . (i + 1) = n & ( for j being Integer st 1 <= j & j <= i holds
( ( sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = (sn . ((i + 1) - (j - 1))) - (sm . ((i + 1) - j)) & pn . ((i + 1) - j) = ((pn . ((i + 1) - (j - 1))) * 2) + 1 ) ) & ( not sn . ((i + 1) - (j - 1)) >= sm . ((i + 1) - j) implies ( sn . ((i + 1) - j) = sn . ((i + 1) - (j - 1)) & pn . ((i + 1) - j) = (pn . ((i + 1) - (j - 1))) * 2 ) ) ) ) & b1 = pn . 1 ) ) ) ) by A6, A15, A21, A8, A14, A39, A29, A31, A108, A104, A41, A36, A42; :: thesis: verum
end;
end;