Theorem subsub ≪ | index | src | ≫ 

theorem subsub (a b c: nat): $ a - b - c = a - (b + c) $;
StepHypRefExpression
1 eor 
(a <= b + c -> a - b - c = a - (b + c)) -> (b + c <= a -> a - b - c = a - (b + c)) -> a <= b + c \/ b + c <= a -> a - b - c = a - (b + c)
2 lesubeq0 
a - b <= c <-> a - b - c = 0
3 lesubadd2 
a - b <= c <-> a <= b + c
4 3 bi2i 
a <= b + c -> a - b <= c
5 2, 4 sylib 
a <= b + c -> a - b - c = 0
6 lesubeq0 
a <= b + c <-> a - (b + c) = 0
7 6 bi1i 
a <= b + c -> a - (b + c) = 0
8 5, 7 eqtr4d 
a <= b + c -> a - b - c = a - (b + c)
9 1, 8 ax_mp 
(b + c <= a -> a - b - c = a - (b + c)) -> a <= b + c \/ b + c <= a -> a - b - c = a - (b + c)
10 eqsub1 
a - b - c + (b + c) = a -> a - (b + c) = a - b - c
11 addlass 
a - b - c + (b + c) = b + (a - b - c + c)
12 npcan 
c <= a - b -> a - b - c + c = a - b
13 leaddsub2i 
b + c <= a -> c <= a - b
14 12, 13 syl 
b + c <= a -> a - b - c + c = a - b
15 14 addeq2d 
b + c <= a -> b + (a - b - c + c) = b + (a - b)
16 pncan3 
b <= a -> b + (a - b) = a
17 letr 
b <= b + c -> b + c <= a -> b <= a
18 leaddid1 
b <= b + c
19 17, 18 ax_mp 
b + c <= a -> b <= a
20 16, 19 syl 
b + c <= a -> b + (a - b) = a
21 15, 20 eqtrd 
b + c <= a -> b + (a - b - c + c) = a
22 11, 21 syl5eq 
b + c <= a -> a - b - c + (b + c) = a
23 10, 22 syl 
b + c <= a -> a - (b + c) = a - b - c
24 23 eqcomd 
b + c <= a -> a - b - c = a - (b + c)
25 9, 24 ax_mp 
a <= b + c \/ b + c <= a -> a - b - c = a - (b + c)
26 leorle 
a <= b + c \/ b + c <= a
27 25, 26 ax_mp 
a - b - c = a - (b + 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, add0, addS)