Theorem divlem1 ≪ | index | src | ≫ 

theorem divlem1 (G: wff) (b q1 q2 r1 r2: nat):
  $ G -> r1 < b $ >
  $ G -> r2 < b $ >
  $ G -> b * q1 + r1 <= b * q2 + r2 $ >
  $ G -> q1 <= q2 $;
StepHypRefExpression
1 leltsuc 
q1 <= q2 <-> q1 < suc q2
2 ltmul2 
0 < b -> (q1 < suc q2 <-> b * q1 < b * suc q2)
3 le01 
0 <= r1
4 3 a1i 
G -> 0 <= r1
5 hyp h1 
G -> r1 < b
6 4, 5 lelttrd 
G -> 0 < b
7 2, 6 syl 
G -> (q1 < suc q2 <-> b * q1 < b * suc q2)
8 leaddid1 
b * q1 <= b * q1 + r1
9 8 a1i 
G -> b * q1 <= b * q1 + r1
10 hyp h3 
G -> b * q1 + r1 <= b * q2 + r2
11 lteq2 
b * suc q2 = b * q2 + b -> (b * q2 + r2 < b * suc q2 <-> b * q2 + r2 < b * q2 + b)
12 mulS 
b * suc q2 = b * q2 + b
13 11, 12 ax_mp 
b * q2 + r2 < b * suc q2 <-> b * q2 + r2 < b * q2 + b
14 ltadd2 
r2 < b <-> b * q2 + r2 < b * q2 + b
15 hyp h2 
G -> r2 < b
16 14, 15 sylib 
G -> b * q2 + r2 < b * q2 + b
17 13, 16 sylibr 
G -> b * q2 + r2 < b * suc q2
18 10, 17 lelttrd 
G -> b * q1 + r1 < b * suc q2
19 9, 18 lelttrd 
G -> b * q1 < b * suc q2
20 7, 19 mpbird 
G -> q1 < suc q2
21 1, 20 sylibr 
G -> q1 <= q2

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)