let n2, m2 be Element of NAT ; :: thesis: ( m2 > 0 implies idiv1_prg (n2,m2) = n2 div m2 )

reconsider n = n2, m = m2 as Integer ;

assume A1: m2 > 0 ; :: thesis: idiv1_prg (n2,m2) = n2 div m2

reconsider n = n2, m = m2 as Integer ;

assume A1: m2 > 0 ; :: thesis: idiv1_prg (n2,m2) = n2 div m2

now :: thesis: ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )end;

hence
idiv1_prg (n2,m2) = n2 div m2
by A1, Def1; :: thesis: verum( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )

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

end;

suppose A2:
n < m
; :: thesis: ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )

set ssm = (Seg (n2 + 1)) --> 1;

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

A4: rng ssm c= {1} by FUNCOP_1:13;

rng ssm c= INT

A5: ( n < m implies n2 div m2 = 0 ) by PRE_FF:4;

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

hence ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A2, A5; :: thesis: verum

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

A4: 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 A4, 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 A4, TARSKI:def 1;

hence y in INT by INT_1:def 2; :: thesis: verum

A5: ( n < m implies n2 div m2 = 0 ) by PRE_FF:4;

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

hence ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A2, A5; :: thesis: verum

suppose A6:
n >= m
; :: thesis: ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) )

deffunc H_{1}( Nat) -> Element of NAT = n2 div (m2 * (2 |^ ($1 -' 1)));

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

A7: len ppn = n2 + 1 and

A8: for k2 being Nat st k2 in dom ppn holds

ppn . k2 = n2 div (m2 * (2 |^ (k2 -' 1))) ;

A9: dom ppn = Seg (n2 + 1) by A7, FINSEQ_1:def 3;

rng ppn c= INT

consider ii0 being Element of NAT such that

A12: for k2 being Element of NAT st k2 < ii0 holds

m * (2 |^ k2) <= n2 and

A13: m2 * (2 |^ ii0) > n2 by A1, Th6;

reconsider i0 = ii0 as Integer ;

deffunc H_{2}( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1)));

deffunc H_{3}( Nat) -> Element of NAT = m2 * (2 |^ ($1 -' 1));

A14: 0 + 1 <= i0 + 1 by XREAL_1:7;

then A18: ii0 + 1 in Seg (n2 + 1) by FINSEQ_1:1;

A19: (ii0 + 1) -' 1 = ii0 by NAT_D:34;

then n2 div (m2 * (2 |^ ((ii0 + 1) -' 1))) = 0 by A13, NAT_D:27;

then A20: ppn . (i0 + 1) = 0 by A8, A9, A18;

n2 >= 0 + 1 by A1, A6, NAT_1:13;

then 1 < n2 + 1 by NAT_1:13;

then A21: 1 in Seg (n2 + 1) by FINSEQ_1:1;

then A22: ppn . 1 = n2 div (m2 * (2 |^ (1 -' 1))) by A8, A9

.= n2 div (m2 * (2 |^ 0)) by XREAL_1:232

.= n2 div (m2 * 1) by NEWTON:4

.= n2 div m2 ;

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

reconsider k5 = m2 * (2 |^ ((ii0 + 1) -' 1)) as Element of NAT ;

A25: k5 > n2 by A13, NAT_D:34;

(ii0 + 1) -' 1 = (i0 - 1) + 1 by NAT_D:34

.= (ii0 -' 1) + 1 by A24, XREAL_0:def 2 ;

then A26: 2 |^ ((ii0 + 1) -' 1) = (2 |^ (ii0 -' 1)) * 2 by NEWTON:6;

ex ssn being FinSequence st

( 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

A27: len ssn = n2 + 1 and

A28: for k2 being Nat st k2 in dom ssn holds

ssn . k2 = n2 mod (m2 * (2 |^ (k2 -' 1))) ;

A29: dom ssn = Seg (n2 + 1) by A27, FINSEQ_1:def 3;

rng ssn c= INT

A32: 1 <= i0 + 1 by A23, NAT_1:13;

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

A33: len ssm = n2 + 1 and

A34: for k2 being Nat st k2 in dom ssm holds

ssm . k2 = m * (2 |^ (k2 -' 1)) ;

A35: dom ssm = Seg (n2 + 1) by A33, FINSEQ_1:def 3;

rng ssm c= INT

A38: ssm . 1 = m * (2 |^ (1 -' 1)) by A21, A34, A35

.= m * (2 |^ 0) by XREAL_1:232

.= m * 1 by NEWTON:4

.= m ;

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

then ii0 + 1 <= n2 + 1 by NAT_1:13;

then ii0 + 1 in Seg (n2 + 1) by A14, FINSEQ_1:1;

then ssn . (i0 + 1) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' 1))) by A28, A29;

then A91: ssn . (i0 + 1) = n by A25, NAT_D:24;

i0 < n2 + 1 by A15, NAT_1:13;

then A92: ii0 in Seg (n2 + 1) by A23, FINSEQ_1:1;

A93: for k being Element of NAT st 1 <= k & k < i0 holds

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

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

i0 + 1 <= n2 + 1 by A15, XREAL_1:7;

then ii0 + 1 in Seg (n2 + 1) by A32, FINSEQ_1:1;

then ssm . (i0 + 1) = m * (2 |^ ((ii0 + 1) -' 1)) by A34, A35

.= (m * (2 |^ (ii0 -' 1))) * 2 by A26

.= (ssm . i0) * 2 by A34, A35, A92 ;

hence ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A6, A33, A27, A7, A22, A38, A23, A15, A101, A104, A20, A91, A39; :: thesis: verum

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

A7: len ppn = n2 + 1 and

A8: for k2 being Nat st k2 in dom ppn holds

ppn . k2 = n2 div (m2 * (2 |^ (k2 -' 1))) ;

A9: dom ppn = Seg (n2 + 1) by A7, 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

A10: x in dom ppn and

A11: y = ppn . x by FUNCT_1:def 3;

reconsider n3 = x as Element of NAT by A10;

ppn . n3 = n2 div (m2 * (2 |^ (n3 -' 1))) by A8, A10;

hence y in INT by A11, INT_1:def 2; :: thesis: verum

end;assume y in rng ppn ; :: thesis: y in INT

then consider x being object such that

A10: x in dom ppn and

A11: y = ppn . x by FUNCT_1:def 3;

reconsider n3 = x as Element of NAT by A10;

ppn . n3 = n2 div (m2 * (2 |^ (n3 -' 1))) by A8, A10;

hence y in INT by A11, INT_1:def 2; :: thesis: verum

consider ii0 being Element of NAT such that

A12: for k2 being Element of NAT st k2 < ii0 holds

m * (2 |^ k2) <= n2 and

A13: m2 * (2 |^ ii0) > n2 by A1, Th6;

reconsider i0 = ii0 as Integer ;

deffunc H

deffunc H

A14: 0 + 1 <= i0 + 1 by XREAL_1:7;

A15: now :: thesis: not i0 > n2

then
( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 )
by NAT_1:11, XREAL_1:7;
1 + 0 <= m2
by A1, NAT_1:13;

then A16: 1 * (2 |^ n2) <= m2 * (2 |^ n2) by XREAL_1:64;

A17: n2 + 1 <= 2 |^ n2 by NEWTON:85;

assume i0 > n2 ; :: thesis: contradiction

then m * (2 |^ n2) <= n2 by A12;

then 2 |^ n2 <= n2 by A16, XXREAL_0:2;

hence contradiction by A17, NAT_1:13; :: thesis: verum

end;then A16: 1 * (2 |^ n2) <= m2 * (2 |^ n2) by XREAL_1:64;

A17: n2 + 1 <= 2 |^ n2 by NEWTON:85;

assume i0 > n2 ; :: thesis: contradiction

then m * (2 |^ n2) <= n2 by A12;

then 2 |^ n2 <= n2 by A16, XXREAL_0:2;

hence contradiction by A17, NAT_1:13; :: thesis: verum

then A18: ii0 + 1 in Seg (n2 + 1) by FINSEQ_1:1;

A19: (ii0 + 1) -' 1 = ii0 by NAT_D:34;

then n2 div (m2 * (2 |^ ((ii0 + 1) -' 1))) = 0 by A13, NAT_D:27;

then A20: ppn . (i0 + 1) = 0 by A8, A9, A18;

n2 >= 0 + 1 by A1, A6, NAT_1:13;

then 1 < n2 + 1 by NAT_1:13;

then A21: 1 in Seg (n2 + 1) by FINSEQ_1:1;

then A22: ppn . 1 = n2 div (m2 * (2 |^ (1 -' 1))) by A8, A9

.= n2 div (m2 * (2 |^ 0)) by XREAL_1:232

.= n2 div (m2 * 1) by NEWTON:4

.= n2 div m2 ;

now :: thesis: not i0 = 0

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

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

hence contradiction by A6; :: thesis: verum

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

hence contradiction by A6; :: thesis: verum

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

reconsider k5 = m2 * (2 |^ ((ii0 + 1) -' 1)) as Element of NAT ;

A25: k5 > n2 by A13, NAT_D:34;

(ii0 + 1) -' 1 = (i0 - 1) + 1 by NAT_D:34

.= (ii0 -' 1) + 1 by A24, XREAL_0:def 2 ;

then A26: 2 |^ ((ii0 + 1) -' 1) = (2 |^ (ii0 -' 1)) * 2 by NEWTON:6;

ex ssn being FinSequence st

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

ssn . k2 = H

then consider ssn being FinSequence such that

A27: len ssn = n2 + 1 and

A28: for k2 being Nat st k2 in dom ssn holds

ssn . k2 = n2 mod (m2 * (2 |^ (k2 -' 1))) ;

A29: dom ssn = Seg (n2 + 1) by A27, 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

A30: x in dom ssn and

A31: y = ssn . x by FUNCT_1:def 3;

reconsider n3 = x as Element of NAT by A30;

ssn . n3 = n2 mod (m2 * (2 |^ (n3 -' 1))) by A28, A30;

hence y in INT by A31, INT_1:def 2; :: thesis: verum

end;assume y in rng ssn ; :: thesis: y in INT

then consider x being object such that

A30: x in dom ssn and

A31: y = ssn . x by FUNCT_1:def 3;

reconsider n3 = x as Element of NAT by A30;

ssn . n3 = n2 mod (m2 * (2 |^ (n3 -' 1))) by A28, A30;

hence y in INT by A31, INT_1:def 2; :: thesis: verum

A32: 1 <= i0 + 1 by A23, NAT_1:13;

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

A33: len ssm = n2 + 1 and

A34: for k2 being Nat st k2 in dom ssm holds

ssm . k2 = m * (2 |^ (k2 -' 1)) ;

A35: dom ssm = Seg (n2 + 1) by A33, FINSEQ_1:def 3;

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 consider x being object such that

A36: x in dom ssm and

A37: y = ssm . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A36;

ssm . n = m * (2 |^ (n -' 1)) by A34, A36;

hence y in INT by A37, INT_1:def 2; :: thesis: verum

end;assume y in rng ssm ; :: thesis: y in INT

then consider x being object such that

A36: x in dom ssm and

A37: y = ssm . x by FUNCT_1:def 3;

reconsider n = x as Element of NAT by A36;

ssm . n = m * (2 |^ (n -' 1)) by A34, A36;

hence y in INT by A37, INT_1:def 2; :: thesis: verum

A38: ssm . 1 = m * (2 |^ (1 -' 1)) by A21, A34, A35

.= m * (2 |^ 0) by XREAL_1:232

.= m * 1 by NEWTON:4

.= m ;

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

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

A40: 1 <= j and

A41: 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 A40, INT_1:3;

A42: j - 1 >= 0 by A40, XREAL_1:48;

A43: i0 - j >= 0 by A41, XREAL_1:48;

then A44: ii0 -' jj = i0 - j by XREAL_0:def 2;

end;assume that

A40: 1 <= j and

A41: 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 A40, INT_1:3;

A42: j - 1 >= 0 by A40, XREAL_1:48;

A43: i0 - j >= 0 by A41, XREAL_1:48;

then A44: ii0 -' jj = i0 - j by XREAL_0:def 2;

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

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

then (i0 + 1) - j >= 0 by XREAL_1:48;

then A45: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

i0 + 1 <= n2 + j by A15, A40, XREAL_1:7;

then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;

then A46: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A45, XREAL_1:7;

assume A47: 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 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7;

then A48: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= jj by NAT_D:35;

then jj -' 1 < i0 + 1 by A48, XXREAL_0:2;

then A49: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

2 |^ (ii0 -' jj) <> 0 by CARD_4:3;

then A50: m2 * (2 |^ (ii0 -' jj)) > m2 * 0 by A1, XREAL_1:68;

( j + 1 <= i0 + 1 & j < j + 1 ) by A41, 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;

ii0 < ii0 + 1 by NAT_1:13;

then j < i0 + 1 by A41, XXREAL_0:2;

then A53: (i0 + 1) - j > 0 by XREAL_1:50;

then A54: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

then A55: (ii0 + 1) -' jj >= 0 + 1 by A53, NAT_1:13;

then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;

then A56: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def 2;

A57: jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then A58: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A52, XREAL_0:def 2;

then A59: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A54, NAT_D:34;

A60: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A57, A52, XREAL_0:def 2;

A61: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A53, XREAL_0:def 2

.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6

.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;

( (ii0 + 1) -' jj <= i0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7;

then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;

then A62: (ii0 + 1) -' jj in Seg (n2 + 1) by A55, FINSEQ_1:1;

then A63: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29;

(ii0 + 1) -' jj = (i0 - j) + 1 by A53, XREAL_0:def 2;

then ((ii0 + 1) -' jj) - 1 >= 0 by A41, XREAL_1:48;

then A64: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def 2

.= ii0 -' jj by A43, XREAL_0:def 2 ;

then A65: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A62;

1 <= (ii0 + 1) -' (jj -' 1) by A54, A58, NAT_1:11;

then A66: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A54, A58, A46, FINSEQ_1:1;

jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A49, XREAL_0:def 2

.= ((ii0 + 1) -' jj) + 1 by A53, XREAL_0:def 2 ;

then A67: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A66

.= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ;

(ii0 + 1) -' jj = (i0 + 1) - j by A53, XREAL_0:def 2;

then A68: (ssn . ((ii0 + 1) -' (jj -' 1))) - (ssm . ((ii0 + 1) -' jj)) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A47, A58, A67, A61, A65, A50, Th2;

ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A62

.= ((n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2) + 1 by A47, A54, A59, A60, A67, A64, A61, A65, A50, Th3

.= ((ppn . ((ii0 + 1) -' (jj -' 1))) * 2) + 1 by A8, A9, A66 ;

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 A54, A58, A56, A63, A68, XREAL_0:def 2; :: thesis: verum

end;then j < i0 + 1 by A41, XXREAL_0:2;

then (i0 + 1) - j >= 0 by XREAL_1:48;

then A45: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

i0 + 1 <= n2 + j by A15, A40, XREAL_1:7;

then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;

then A46: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A45, XREAL_1:7;

assume A47: 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 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7;

then A48: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= jj by NAT_D:35;

then jj -' 1 < i0 + 1 by A48, XXREAL_0:2;

then A49: (ii0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

2 |^ (ii0 -' jj) <> 0 by CARD_4:3;

then A50: m2 * (2 |^ (ii0 -' jj)) > m2 * 0 by A1, XREAL_1:68;

( j + 1 <= i0 + 1 & j < j + 1 ) by A41, 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;

ii0 < ii0 + 1 by NAT_1:13;

then j < i0 + 1 by A41, XXREAL_0:2;

then A53: (i0 + 1) - j > 0 by XREAL_1:50;

then A54: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

then A55: (ii0 + 1) -' jj >= 0 + 1 by A53, NAT_1:13;

then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;

then A56: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def 2;

A57: jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then A58: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A52, XREAL_0:def 2;

then A59: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A54, NAT_D:34;

A60: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A57, A52, XREAL_0:def 2;

A61: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A53, XREAL_0:def 2

.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6

.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;

( (ii0 + 1) -' jj <= i0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7;

then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;

then A62: (ii0 + 1) -' jj in Seg (n2 + 1) by A55, FINSEQ_1:1;

then A63: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29;

(ii0 + 1) -' jj = (i0 - j) + 1 by A53, XREAL_0:def 2;

then ((ii0 + 1) -' jj) - 1 >= 0 by A41, XREAL_1:48;

then A64: ((ii0 + 1) -' jj) -' 1 = i0 - j by A54, XREAL_0:def 2

.= ii0 -' jj by A43, XREAL_0:def 2 ;

then A65: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A62;

1 <= (ii0 + 1) -' (jj -' 1) by A54, A58, NAT_1:11;

then A66: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A54, A58, A46, FINSEQ_1:1;

jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A49, XREAL_0:def 2

.= ((ii0 + 1) -' jj) + 1 by A53, XREAL_0:def 2 ;

then A67: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A66

.= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ;

(ii0 + 1) -' jj = (i0 + 1) - j by A53, XREAL_0:def 2;

then A68: (ssn . ((ii0 + 1) -' (jj -' 1))) - (ssm . ((ii0 + 1) -' jj)) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A47, A58, A67, A61, A65, A50, Th2;

ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A62

.= ((n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2) + 1 by A47, A54, A59, A60, A67, A64, A61, A65, A50, Th3

.= ((ppn . ((ii0 + 1) -' (jj -' 1))) * 2) + 1 by A8, A9, A66 ;

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 A54, A58, A56, A63, A68, XREAL_0:def 2; :: thesis: verum

proof

( j + 1 <= i0 + 1 & jj < jj + 1 )
by A41, NAT_1:13, XREAL_1:7;

then A69: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= j by NAT_D:35;

then jj -' 1 < i0 + 1 by A69, XXREAL_0:2;

then A70: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

( j + 1 <= i0 + 1 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7;

then A71: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= jj by NAT_D:35;

then jj -' 1 < i0 + 1 by A71, XXREAL_0:2;

then A72: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

ii0 < ii0 + 1 by NAT_1:13;

then j < i0 + 1 by A41, XXREAL_0:2;

then (i0 + 1) - j >= 0 by XREAL_1:48;

then A73: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

i0 + 1 <= n2 + j by A15, A40, XREAL_1:7;

then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;

then A74: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A73, XREAL_1:7;

assume A75: 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 A41, XXREAL_0:2;

then A76: (i0 + 1) - j > 0 by XREAL_1:50;

then A77: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

then A78: (ii0 + 1) -' jj >= 0 + 1 by A76, NAT_1:13;

then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;

then A79: ((ii0 + 1) -' jj) -' 1 = i0 - j by A77, XREAL_0:def 2;

A80: jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then A81: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A72, XREAL_0:def 2;

then A82: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A77, NAT_D:34;

A83: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A80, A72, XREAL_0:def 2;

A84: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A76, XREAL_0:def 2

.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6

.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;

( (ii0 + 1) -' jj <= ii0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7;

then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;

then A85: (ii0 + 1) -' jj in Seg (n2 + 1) by A78, FINSEQ_1:1;

then ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29;

then A86: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A79, XREAL_0:def 2;

(ii0 + 1) -' jj = (i0 - j) + 1 by A76, XREAL_0:def 2;

then A87: ((ii0 + 1) -' jj) -' 1 = ((i0 - j) + 1) - 1 by A43, XREAL_0:def 2

.= ii0 -' jj by A43, XREAL_0:def 2 ;

then A88: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A85;

1 <= (ii0 + 1) -' (jj -' 1) by A77, A81, NAT_1:11;

then A89: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A77, A81, A74, FINSEQ_1:1;

jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then (ii0 + 1) -' (jj -' 1) = ((ii0 + 1) -' jj) + 1 by A77, A70, XREAL_0:def 2;

then A90: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A89

.= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ;

ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A85

.= (n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2 by A75, A77, A82, A83, A90, A87, A84, A88, Th5

.= (ppn . ((ii0 + 1) -' (jj -' 1))) * 2 by A8, A9, A89 ;

hence ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) by A75, A77, A81, A86, A90, A84, A88, Th4; :: thesis: verum

end;then A69: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= j by NAT_D:35;

then jj -' 1 < i0 + 1 by A69, XXREAL_0:2;

then A70: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

( j + 1 <= i0 + 1 & jj < jj + 1 ) by A41, NAT_1:13, XREAL_1:7;

then A71: j < i0 + 1 by XXREAL_0:2;

jj -' 1 <= jj by NAT_D:35;

then jj -' 1 < i0 + 1 by A71, XXREAL_0:2;

then A72: (i0 + 1) - (jj -' 1) >= 0 by XREAL_1:48;

ii0 < ii0 + 1 by NAT_1:13;

then j < i0 + 1 by A41, XXREAL_0:2;

then (i0 + 1) - j >= 0 by XREAL_1:48;

then A73: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

i0 + 1 <= n2 + j by A15, A40, XREAL_1:7;

then (i0 + 1) - j <= (n2 + j) - j by XREAL_1:9;

then A74: ((ii0 + 1) -' jj) + 1 <= n2 + 1 by A73, XREAL_1:7;

assume A75: 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 A41, XXREAL_0:2;

then A76: (i0 + 1) - j > 0 by XREAL_1:50;

then A77: (ii0 + 1) -' jj = (i0 + 1) - j by XREAL_0:def 2;

then A78: (ii0 + 1) -' jj >= 0 + 1 by A76, NAT_1:13;

then ((ii0 + 1) -' jj) - 1 >= 0 by XREAL_1:48;

then A79: ((ii0 + 1) -' jj) -' 1 = i0 - j by A77, XREAL_0:def 2;

A80: jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then A81: (ii0 + 1) -' (jj -' 1) = ((i0 + 1) - j) + 1 by A72, XREAL_0:def 2;

then A82: ((ii0 + 1) -' (jj -' 1)) -' 1 = (ii0 + 1) -' jj by A77, NAT_D:34;

A83: (ii0 + 1) -' (jj -' 1) = (i0 + 1) - (j - 1) by A80, A72, XREAL_0:def 2;

A84: m2 * (2 |^ ((ii0 + 1) -' jj)) = m2 * (2 |^ ((ii0 -' jj) + 1)) by A44, A76, XREAL_0:def 2

.= m2 * ((2 |^ (ii0 -' jj)) * 2) by NEWTON:6

.= 2 * (m2 * (2 |^ (ii0 -' jj))) ;

( (ii0 + 1) -' jj <= ii0 + 1 & i0 + 1 <= n2 + 1 ) by A15, NAT_D:35, XREAL_1:7;

then n2 + 1 >= (ii0 + 1) -' jj by XXREAL_0:2;

then A85: (ii0 + 1) -' jj in Seg (n2 + 1) by A78, FINSEQ_1:1;

then ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A28, A29;

then A86: ssn . ((ii0 + 1) -' jj) = n2 mod (m2 * (2 |^ (ii0 -' jj))) by A79, XREAL_0:def 2;

(ii0 + 1) -' jj = (i0 - j) + 1 by A76, XREAL_0:def 2;

then A87: ((ii0 + 1) -' jj) -' 1 = ((i0 - j) + 1) - 1 by A43, XREAL_0:def 2

.= ii0 -' jj by A43, XREAL_0:def 2 ;

then A88: ssm . ((ii0 + 1) -' jj) = m2 * (2 |^ (ii0 -' jj)) by A34, A35, A85;

1 <= (ii0 + 1) -' (jj -' 1) by A77, A81, NAT_1:11;

then A89: (ii0 + 1) -' (jj -' 1) in Seg (n2 + 1) by A77, A81, A74, FINSEQ_1:1;

jj -' 1 = j - 1 by A42, XREAL_0:def 2;

then (ii0 + 1) -' (jj -' 1) = ((ii0 + 1) -' jj) + 1 by A77, A70, XREAL_0:def 2;

then A90: ssn . ((ii0 + 1) -' (jj -' 1)) = n2 mod (m2 * (2 |^ ((((ii0 + 1) -' jj) + 1) -' 1))) by A28, A29, A89

.= n2 mod (m2 * (2 |^ ((ii0 + 1) -' jj))) by NAT_D:34 ;

ppn . ((ii0 + 1) -' jj) = n2 div (m2 * (2 |^ (((ii0 + 1) -' jj) -' 1))) by A8, A9, A85

.= (n2 div (m2 * (2 |^ (((ii0 + 1) -' (jj -' 1)) -' 1)))) * 2 by A75, A77, A82, A83, A90, A87, A84, A88, Th5

.= (ppn . ((ii0 + 1) -' (jj -' 1))) * 2 by A8, A9, A89 ;

hence ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) by A75, A77, A81, A86, A90, A84, A88, Th4; :: thesis: verum

then ii0 + 1 <= n2 + 1 by NAT_1:13;

then ii0 + 1 in Seg (n2 + 1) by A14, FINSEQ_1:1;

then ssn . (i0 + 1) = n2 mod (m2 * (2 |^ ((ii0 + 1) -' 1))) by A28, A29;

then A91: ssn . (i0 + 1) = n by A25, NAT_D:24;

i0 < n2 + 1 by A15, NAT_1:13;

then A92: ii0 in Seg (n2 + 1) by A23, FINSEQ_1:1;

A93: for k being Element of NAT st 1 <= k & k < i0 holds

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

proof

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

A94: 1 <= k and

A95: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

A96: k <= n2 by A15, A95, XXREAL_0:2;

then A97: k + 1 <= n2 + 1 by XREAL_1:7;

k <= n2 + 1 by A96, NAT_1:12;

then k in Seg (n2 + 1) by A94, FINSEQ_1:1;

then A98: ssm . k = m * (2 |^ (k -' 1)) by A34, A35;

1 < k + 1 by A94, NAT_1:13;

then k + 1 in Seg (n2 + 1) by A97, FINSEQ_1:1;

then A99: ( (k + 1) -' 1 = k & ssm . (k + 1) = m * (2 |^ ((k + 1) -' 1)) ) by A34, A35, NAT_D:34;

A100: k - 1 >= 0 by A94, XREAL_1:48;

(k + 1) -' 1 = (k - 1) + 1 by NAT_D:34

.= (k -' 1) + 1 by A100, 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 A12, A95, A99, A98; :: thesis: verum

end;assume that

A94: 1 <= k and

A95: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

A96: k <= n2 by A15, A95, XXREAL_0:2;

then A97: k + 1 <= n2 + 1 by XREAL_1:7;

k <= n2 + 1 by A96, NAT_1:12;

then k in Seg (n2 + 1) by A94, FINSEQ_1:1;

then A98: ssm . k = m * (2 |^ (k -' 1)) by A34, A35;

1 < k + 1 by A94, NAT_1:13;

then k + 1 in Seg (n2 + 1) by A97, FINSEQ_1:1;

then A99: ( (k + 1) -' 1 = k & ssm . (k + 1) = m * (2 |^ ((k + 1) -' 1)) ) by A34, A35, NAT_D:34;

A100: k - 1 >= 0 by A94, XREAL_1:48;

(k + 1) -' 1 = (k - 1) + 1 by NAT_D:34

.= (k -' 1) + 1 by A100, 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 A12, A95, A99, A98; :: thesis: verum

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

proof

A104:
ssm . (i0 + 1) > n
by A34, A35, A13, A19, A18;
let k be Integer; :: thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) )

assume that

A102: 1 <= k and

A103: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

reconsider kk = k as Element of NAT by A102, INT_1:3;

ssm . (kk + 1) = (ssm . kk) * 2 by A93, A102, A103;

hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A93, A102, A103; :: thesis: verum

end;assume that

A102: 1 <= k and

A103: k < i0 ; :: thesis: ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )

reconsider kk = k as Element of NAT by A102, INT_1:3;

ssm . (kk + 1) = (ssm . kk) * 2 by A93, A102, A103;

hence ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) by A93, A102, A103; :: thesis: verum

i0 + 1 <= n2 + 1 by A15, XREAL_1:7;

then ii0 + 1 in Seg (n2 + 1) by A32, FINSEQ_1:1;

then ssm . (i0 + 1) = m * (2 |^ ((ii0 + 1) -' 1)) by A34, A35

.= (m * (2 |^ (ii0 -' 1))) * 2 by A26

.= (ssm . i0) * 2 by A34, A35, A92 ;

hence ex sm, sn, pn being FinSequence of INT st

( len sm = n + 1 & len sn = n + 1 & len pn = n + 1 & ( n < m implies n2 div m2 = 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 ) ) ) ) & n2 div m2 = pn . 1 ) ) ) ) by A6, A33, A27, A7, A22, A38, A23, A15, A101, A104, A20, A91, A39; :: thesis: verum