Theorem lepr1 ≪ | index | src | ≫

theorem lepr1 (a b c: nat): $ a <= b <-> a, c <= b, c $;

Step	Hyp	Ref	Expression
1		contra	(~a, c <= b, c -> a, c <= b, c) -> a, c <= b, c
2		eqle	a, c = b, c -> a, c <= b, c
3		anl	a <= b /\ ~a, c <= b, c -> a <= b
4		leadd1	b <= a <-> b + c <= a + c
5		prlem2	b, c <= a, c -> b + c <= a + c
6		leorle	a, c <= b, c \/ b, c <= a, c
7	6	conv or	~a, c <= b, c -> b, c <= a, c
8	7	anwr	a <= b /\ ~a, c <= b, c -> b, c <= a, c
9	5, 8	syl	a <= b /\ ~a, c <= b, c -> b + c <= a + c
10	4, 9	sylibr	a <= b /\ ~a, c <= b, c -> b <= a
11	3, 10	leasymd	a <= b /\ ~a, c <= b, c -> a = b
12	11	preq1d	a <= b /\ ~a, c <= b, c -> a, c = b, c
13	2, 12	syl	a <= b /\ ~a, c <= b, c -> a, c <= b, c
14	1, 13	syla	a <= b -> a, c <= b, c
15		leadd1	a <= b <-> a + c <= b + c
16		prlem2	a, c <= b, c -> a + c <= b + c
17	15, 16	sylibr	a, c <= b, c -> a <= b
18	14, 17	ibii	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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)