Theorem divmod ≪ | index | src | ≫ 

pub theorem divmod (a b: nat): $ b * (a // b) + a % b = a $;
StepHypRefExpression
1 pncan3 
b * (a // b) <= a -> b * (a // b) + (a - b * (a // b)) = a
2 1 conv mod 
b * (a // b) <= a -> b * (a // b) + a % b = a
3 le01 
0 <= a
4 mul0 
b * 0 = 0
5 div0 
a // 0 = 0
6 diveq2 
b = 0 -> a // b = a // 0
7 5, 6 syl6eq 
b = 0 -> a // b = 0
8 7 muleq2d 
b = 0 -> b * (a // b) = b * 0
9 4, 8 syl6eq 
b = 0 -> b * (a // b) = 0
10 9 leeq1d 
b = 0 -> (b * (a // b) <= a <-> 0 <= a)
11 3, 10 mpbiri 
b = 0 -> b * (a // b) <= a
12 divlem3 
b != 0 -> E. q E. r (r < b /\ b * q + r = a)
13 12 conv ne 
~b = 0 -> E. q E. r (r < b /\ b * q + r = a)
14 leaddid1 
b * (a // b) <= b * (a // b) + r
15 anrl 
~b = 0 /\ (r < b /\ b * q + r = a) -> r < b
16 anrr 
~b = 0 /\ (r < b /\ b * q + r = a) -> b * q + r = a
17 15, 16 divlem2 
~b = 0 /\ (r < b /\ b * q + r = a) -> (E. y (y < b /\ b * x + y = a) <-> x = q)
18 17 eqtheabd 
~b = 0 /\ (r < b /\ b * q + r = a) -> the {x | E. y (y < b /\ b * x + y = a)} = q
19 18 conv div 
~b = 0 /\ (r < b /\ b * q + r = a) -> a // b = q
20 19 muleq2d 
~b = 0 /\ (r < b /\ b * q + r = a) -> b * (a // b) = b * q
21 20 addeq1d 
~b = 0 /\ (r < b /\ b * q + r = a) -> b * (a // b) + r = b * q + r
22 21, 16 eqtrd 
~b = 0 /\ (r < b /\ b * q + r = a) -> b * (a // b) + r = a
23 22 leeq2d 
~b = 0 /\ (r < b /\ b * q + r = a) -> (b * (a // b) <= b * (a // b) + r <-> b * (a // b) <= a)
24 14, 23 mpbii 
~b = 0 /\ (r < b /\ b * q + r = a) -> b * (a // b) <= a
25 24 eexda 
~b = 0 -> E. r (r < b /\ b * q + r = a) -> b * (a // b) <= a
26 25 eexd 
~b = 0 -> E. q E. r (r < b /\ b * q + r = a) -> b * (a // b) <= a
27 13, 26 mpd 
~b = 0 -> b * (a // b) <= a
28 11, 27 cases 
b * (a // b) <= a
29 2, 28 ax_mp 
b * (a // b) + a % b = a

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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)