Theorem eqalle2 ≪ | index | src | ≫

theorem eqalle2 (a b: nat) {i: nat}: $ a = b <-> A. i (a <= i <-> b <= i) $;

Step	Hyp	Ref	Expression
1		leeq1	a = b -> (a <= i <-> b <= i)
2	1	iald	a = b -> A. i (a <= i <-> b <= i)
3		leid	b <= b
4		leeq2	i = b -> (a <= i <-> a <= b)
5		leeq2	i = b -> (b <= i <-> b <= b)
6	4, 5	bieqd	i = b -> (a <= i <-> b <= i <-> (a <= b <-> b <= b))
7	6	eale	A. i (a <= i <-> b <= i) -> (a <= b <-> b <= b)
8	3, 7	mpbiri	A. i (a <= i <-> b <= i) -> a <= b
9		leid	a <= a
10		leeq2	i = a -> (a <= i <-> a <= a)
11		leeq2	i = a -> (b <= i <-> b <= a)
12	10, 11	bieqd	i = a -> (a <= i <-> b <= i <-> (a <= a <-> b <= a))
13	12	eale	A. i (a <= i <-> b <= i) -> (a <= a <-> b <= a)
14	9, 13	mpbii	A. i (a <= i <-> b <= i) -> b <= a
15	8, 14	leasymd	A. i (a <= i <-> b <= i) -> a = b
16	2, 15	ibii	a = b <-> A. i (a <= i <-> b <= i)

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)