Theorem muladddiv2 | index | src |

theorem muladddiv2 (a b c: nat): $ b != 0 -> (b * a + c) // b = a + c // b $;
StepHypRefExpression
1 modlt
b != 0 -> c % b < b
2 eqtr
b * (a + c // b) + c % b = b * a + b * (c // b) + c % b -> b * a + b * (c // b) + c % b = b * a + c -> b * (a + c // b) + c % b = b * a + c
3 addeq1
b * (a + c // b) = b * a + b * (c // b) -> b * (a + c // b) + c % b = b * a + b * (c // b) + c % b
4 muladd
b * (a + c // b) = b * a + b * (c // b)
5 3, 4 ax_mp
b * (a + c // b) + c % b = b * a + b * (c // b) + c % b
6 2, 5 ax_mp
b * a + b * (c // b) + c % b = b * a + c -> b * (a + c // b) + c % b = b * a + c
7 eqtr
b * a + b * (c // b) + c % b = b * a + (b * (c // b) + c % b) -> b * a + (b * (c // b) + c % b) = b * a + c -> b * a + b * (c // b) + c % b = b * a + c
8 addass
b * a + b * (c // b) + c % b = b * a + (b * (c // b) + c % b)
9 7, 8 ax_mp
b * a + (b * (c // b) + c % b) = b * a + c -> b * a + b * (c // b) + c % b = b * a + c
10 addeq2
b * (c // b) + c % b = c -> b * a + (b * (c // b) + c % b) = b * a + c
11 divmod
b * (c // b) + c % b = c
12 10, 11 ax_mp
b * a + (b * (c // b) + c % b) = b * a + c
13 9, 12 ax_mp
b * a + b * (c // b) + c % b = b * a + c
14 6, 13 ax_mp
b * (a + c // b) + c % b = b * a + c
15 14 a1i
b != 0 -> b * (a + c // b) + c % b = b * a + c
16 1, 15 eqdivmod
b != 0 -> (b * a + c) // b = a + c // b /\ (b * a + c) % b = c % b
17 16 anld
b != 0 -> (b * a + c) // b = a + c // b

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)