Theorem natle ≪ | index | src | ≫

theorem natle (p q: wff): $ p -> q <-> nat p <= nat q $;

Step	Hyp	Ref	Expression
1		bicom	(nat p <= nat q <-> p -> q) -> (p -> q <-> nat p <= nat q)
2		bitr	(nat p <= nat q <-> true (nat p) -> true (nat q)) -> (true (nat p) -> true (nat q) <-> p -> q) -> (nat p <= nat q <-> p -> q)
3		letrueb	bool (nat p) -> (nat p <= nat q <-> true (nat p) -> true (nat q))
4		boolnat	bool (nat p)
5	3, 4	ax_mp	nat p <= nat q <-> true (nat p) -> true (nat q)
6	2, 5	ax_mp	(true (nat p) -> true (nat q) <-> p -> q) -> (nat p <= nat q <-> p -> q)
7		truenat	true (nat p) <-> p
8		truenat	true (nat q) <-> q
9	7, 8	imeqi	true (nat p) -> true (nat q) <-> p -> q
10	6, 9	ax_mp	nat p <= nat q <-> p -> q
11	1, 10	ax_mp	p -> q <-> nat p <= nat q

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