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
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 ) ) ) )
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: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
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;
then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def 4;
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;
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 ) ) ) )
deffunc H1( 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 = H1(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
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ppn or y in INT )
assume y in rng ppn ; :: thesis: y in INT
then consider x being object such that
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;
then reconsider ppn = ppn as FinSequence of INT by FINSEQ_1:def 4;
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 H2( Nat) -> Element of NAT = n2 mod (m2 * (2 |^ ($1 -' 1)));
deffunc H3( Nat) -> Element of NAT = m2 * (2 |^ ($1 -' 1));
A14: 0 + 1 <= i0 + 1 by XREAL_1:7;
A15: now :: thesis: not i0 > n2
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 ( 1 <= 1 + ii0 & i0 + 1 <= n2 + 1 ) by NAT_1:11, 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 ;
now :: thesis: not i0 = 0
assume i0 = 0 ; :: thesis: contradiction
then m2 * 1 > n2 by A13, NEWTON:4;
hence contradiction by A6; :: thesis: verum
end;
then A23: ii0 >= 0 + 1 by NAT_1:13;
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 = H2(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
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ssn or y in INT )
assume y in rng ssn ; :: thesis: y in INT
then consider x being object such that
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;
then reconsider ssn = ssn as FinSequence of INT by FINSEQ_1:def 4;
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 = H3(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
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ssm or y in INT )
assume y in rng ssm ; :: thesis: y in INT
then consider x being object such that
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;
then reconsider ssm = ssm as FinSequence of INT by FINSEQ_1:def 4;
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
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;
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 ) )
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;
thus ( not ssn . ((i0 + 1) - (j - 1)) >= ssm . ((i0 + 1) - j) implies ( ssn . ((i0 + 1) - j) = ssn . ((i0 + 1) - (j - 1)) & ppn . ((i0 + 1) - j) = (ppn . ((i0 + 1) - (j - 1))) * 2 ) ) :: thesis: verum
proof
( j + 1 <= i0 + 1 & jj < jj + 1 ) by 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;
end;
i0 < n2 + 1 by A15, NAT_1:13;
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
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;
A101: for k being Integer st 1 <= k & k < i0 holds
( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n )
proof
let k be Integer; :: thesis: ( 1 <= k & k < i0 implies ( ssm . (k + 1) = (ssm . k) * 2 & not ssm . (k + 1) > n ) )
assume that
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;
A104: ssm . (i0 + 1) > n by A34, A35, A13, A19, A18;
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;
end;
end;
hence idiv1_prg (n2,m2) = n2 div m2 by A1, Def1; :: thesis: verum