Theorem lesub1i | index | src |

theorem lesub1i (a b c: nat): $ a <= b -> a - c <= b - c $;
StepHypRefExpression
1 leadd1
a - c <= b - c <-> a - c + c <= b - c + c
2 npcan
c <= a -> a - c + c = a
3 2 anwl
c <= a /\ a <= b -> a - c + c = a
4 npcan
c <= b -> b - c + c = b
5 letr
c <= a -> a <= b -> c <= b
6 5 imp
c <= a /\ a <= b -> c <= b
7 4, 6 syl
c <= a /\ a <= b -> b - c + c = b
8 3, 7 leeqd
c <= a /\ a <= b -> (a - c + c <= b - c + c <-> a <= b)
9 anr
c <= a /\ a <= b -> a <= b
10 8, 9 mpbird
c <= a /\ a <= b -> a - c + c <= b - c + c
11 1, 10 sylibr
c <= a /\ a <= b -> a - c <= b - c
12 11 exp
c <= a -> a <= b -> a - c <= b - c
13 le01
0 <= b - c
14 nlesubeq0
~c <= a -> a - c = 0
15 14 leeq1d
~c <= a -> (a - c <= b - c <-> 0 <= b - c)
16 13, 15 mpbiri
~c <= a -> a - c <= b - c
17 16 a1d
~c <= a -> a <= b -> a - c <= b - c
18 12, 17 cases
a <= b -> a - c <= 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 (peano2, peano5, addeq, add0, addS)