Theorem lepr2 ≪ | index | src | ≫

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

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