Theorem mulsub | index | src |

theorem mulsub (a b c: nat): $ a * (b - c) = a * b - a * c $;
StepHypRefExpression
1 eor
(c <= b -> a * (b - c) = a * b - a * c) -> (b <= c -> a * (b - c) = a * b - a * c) -> c <= b \/ b <= c -> a * (b - c) = a * b - a * c
2 eqsub1
a * (b - c) + a * c = a * b -> a * b - a * c = a * (b - c)
3 muladd
a * (b - c + c) = a * (b - c) + a * c
4 npcan
c <= b -> b - c + c = b
5 4 muleq2d
c <= b -> a * (b - c + c) = a * b
6 3, 5 syl5eqr
c <= b -> a * (b - c) + a * c = a * b
7 2, 6 syl
c <= b -> a * b - a * c = a * (b - c)
8 7 eqcomd
c <= b -> a * (b - c) = a * b - a * c
9 1, 8 ax_mp
(b <= c -> a * (b - c) = a * b - a * c) -> c <= b \/ b <= c -> a * (b - c) = a * b - a * c
10 mul02
a * 0 = 0
11 lesubeq0
b <= c <-> b - c = 0
12 muleq2
b - c = 0 -> a * (b - c) = a * 0
13 11, 12 sylbi
b <= c -> a * (b - c) = a * 0
14 10, 13 syl6eq
b <= c -> a * (b - c) = 0
15 lesubeq0
a * b <= a * c <-> a * b - a * c = 0
16 lemul2a
b <= c -> a * b <= a * c
17 15, 16 sylib
b <= c -> a * b - a * c = 0
18 14, 17 eqtr4d
b <= c -> a * (b - c) = a * b - a * c
19 9, 18 ax_mp
c <= b \/ b <= c -> a * (b - c) = a * b - a * c
20 leorle
c <= b \/ b <= c
21 19, 20 ax_mp
a * (b - c) = a * b - a * c

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)