Theorem ltlenle ≪ | index | src | ≫

theorem ltlenle (a b: nat): $ a < b <-> a <= b /\ ~b <= a $;

Step	Hyp	Ref	Expression
1		ltle	a < b -> a <= b
2		ltirr	~a < a
3	2	a1i	a < b -> ~a < a
4		ltletr	a < b -> b <= a -> a < a
5	3, 4	mtd	a < b -> ~b <= a
6	1, 5	iand	a < b -> a <= b /\ ~b <= a
7		ltlene	a < b <-> a <= b /\ a != b
8		anl	a <= b /\ ~b <= a -> a <= b
9		con3	(a = b -> b <= a) -> ~b <= a -> ~a = b
10	9	conv ne	(a = b -> b <= a) -> ~b <= a -> a != b
11		eqler	a = b -> b <= a
12	10, 11	ax_mp	~b <= a -> a != b
13	12	anwr	a <= b /\ ~b <= a -> a != b
14	8, 13	iand	a <= b /\ ~b <= a -> a <= b /\ a != b
15	7, 14	sylibr	a <= b /\ ~b <= a -> a < b
16	6, 15	ibii	a < b <-> a <= b /\ ~b <= a

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_peano (peano1, peano2, peano5, addeq, add0, addS)