reconsider n2 = n, m2 = m as Element of NAT by A1, A2, INT_1:3;

per cases
( n < m or n >= m )
;

end;

suppose A3:
n < m
; :: thesis: ex b_{1} 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 b_{1} = 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 ) ) ) ) & b_{1} = pn . 1 ) ) ) )

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b

( 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 ) ) ) ) & b

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

len ssm = n + 1 by A4, FINSEQ_1:def 3;

hence ex b_{1} 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 b_{1} = 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 ) ) ) ) & b_{1} = pn . 1 ) ) ) )
by A3; :: thesis: verum

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

then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def 4;
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;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

len ssm = n + 1 by A4, FINSEQ_1:def 3;

hence ex b

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b

( 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 ) ) ) ) & b

suppose A6:
n >= m
; :: thesis: ex b_{1} 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 b_{1} = 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 ) ) ) ) & b_{1} = pn . 1 ) ) ) )

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b

( 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 ) ) ) ) & b

deffunc H_{1}( 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 = H_{1}(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

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 H_{2}( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1)));

deffunc H_{3}( 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 = H_{3}(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

( len ssn = n2 + 1 & ( for k2 being Nat st k2 in dom ssn holds

ssn . k2 = H_{2}(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

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;

then A30: i0 - 1 >= 0 by XREAL_1:48;

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

( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

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 b_{1} 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 b_{1} = 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 ) ) ) ) & b_{1} = pn . 1 ) ) ) )
by A6, A15, A21, A8, A14, A39, A29, A31, A108, A104, A41, A36, A42; :: thesis: verum

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

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

then reconsider ppn = ppn as FinSequence of INT by FINSEQ_1:def 4;
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;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

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 H

deffunc H

ex ssm being FinSequence st

( len ssm = n2 + 1 & ( for k2 being Nat st k2 in dom ssm holds

ssm . k2 = H

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

ex ssn being FinSequence st
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;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

( len ssn = n2 + 1 & ( for k2 being Nat st k2 in dom ssn holds

ssn . k2 = H

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

then reconsider ssn = ssn as FinSequence of INT by FINSEQ_1:def 4;
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;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

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

then A29:
ii0 >= 0 + 1
by NAT_1:13;assume
i0 = 0
; :: thesis: contradiction

then m2 * 1 > n2 by A27, NEWTON:4;

hence contradiction by A6; :: thesis: verum

end;then m2 * 1 > n2 by A27, NEWTON:4;

hence contradiction by A6; :: thesis: verum

then A30: i0 - 1 >= 0 by XREAL_1:48;

A31: now :: thesis: not i0 > n2

then
( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 )
by NAT_1:11, XREAL_1:7;
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 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

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

A96:
for k being Element of NAT st 1 <= k & k < i0 holds
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 ) )

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

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

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

( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

proof

A104:
for k being Integer st 1 <= k & k < i0 holds
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;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

( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

proof

i0 < n2 + 1
by A31, NAT_1:13;
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;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

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 b

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies b

( 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 ) ) ) ) & b