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