Theorem lesubadd2 ≪ | index | src | ≫ 

theorem lesubadd2 (a b c: nat): $ a - b <= c <-> a <= b + c $;
StepHypRefExpression
1 eor 
(a <= b -> a - b <= c -> a <= b + c) -> (b <= a -> a - b <= c -> a <= b + c) -> a <= b \/ b <= a -> a - b <= c -> a <= b + c
2 leaddid1 
b <= b + c
3 letr 
a <= b -> b <= b + c -> a <= b + c
4 2, 3 mpi 
a <= b -> a <= b + c
5 4 a1d 
a <= b -> a - b <= c -> a <= b + c
6 1, 5 ax_mp 
(b <= a -> a - b <= c -> a <= b + c) -> a <= b \/ b <= a -> a - b <= c -> a <= b + c
7 leadd2 
a - b <= c <-> b + (a - b) <= b + c
8 pncan3 
b <= a -> b + (a - b) = a
9 8 leeq1d 
b <= a -> (b + (a - b) <= b + c <-> a <= b + c)
10 7, 9 syl5bb 
b <= a -> (a - b <= c <-> a <= b + c)
11 10 bi1d 
b <= a -> a - b <= c -> a <= b + c
12 6, 11 ax_mp 
a <= b \/ b <= a -> a - b <= c -> a <= b + c
13 leorle 
a <= b \/ b <= a
14 12, 13 ax_mp 
a - b <= c -> a <= b + c
15 leeq2 
b + c - b = c -> (a - b <= b + c - b <-> a - b <= c)
16 pncan2 
b + c - b = c
17 15, 16 ax_mp 
a - b <= b + c - b <-> a - b <= c
18 lesub1i 
a <= b + c -> a - b <= b + c - b
19 17, 18 sylib 
a <= b + c -> a - b <= c
20 14, 19 ibii 
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)