1lt2pi

Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	1lt2pi	$⊢ 1_{𝑜} <_{𝑵} (1_{𝑜} +_{𝑵} 1_{𝑜})$

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		nna0	$⊢ 1_{𝑜} \in ω \to 1_{𝑜} +_{𝑜} \emptyset = 1_{𝑜}$
3	1 2	ax-mp	$⊢ 1_{𝑜} +_{𝑜} \emptyset = 1_{𝑜}$
4		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
5		peano1	$⊢ \emptyset \in ω$
6		nnaord	$⊢ (\emptyset \in ω \land 1_{𝑜} \in ω \land 1_{𝑜} \in ω) \to (\emptyset \in 1_{𝑜} \leftrightarrow 1_{𝑜} +_{𝑜} \emptyset \in (1_{𝑜} +_{𝑜} 1_{𝑜}))$
7	5 1 1 6	mp3an	$⊢ \emptyset \in 1_{𝑜} \leftrightarrow 1_{𝑜} +_{𝑜} \emptyset \in (1_{𝑜} +_{𝑜} 1_{𝑜})$
8	4 7	mpbi	$⊢ 1_{𝑜} +_{𝑜} \emptyset \in (1_{𝑜} +_{𝑜} 1_{𝑜})$
9	3 8	eqeltrri	$⊢ 1_{𝑜} \in (1_{𝑜} +_{𝑜} 1_{𝑜})$
10		1pi	$⊢ 1_{𝑜} \in 𝑵$
11		addpiord	$⊢ (1_{𝑜} \in 𝑵 \land 1_{𝑜} \in 𝑵) \to 1_{𝑜} +_{𝑵} 1_{𝑜} = 1_{𝑜} +_{𝑜} 1_{𝑜}$
12	10 10 11	mp2an	$⊢ 1_{𝑜} +_{𝑵} 1_{𝑜} = 1_{𝑜} +_{𝑜} 1_{𝑜}$
13	9 12	eleqtrri	$⊢ 1_{𝑜} \in (1_{𝑜} +_{𝑵} 1_{𝑜})$
14		addclpi	$⊢ (1_{𝑜} \in 𝑵 \land 1_{𝑜} \in 𝑵) \to 1_{𝑜} +_{𝑵} 1_{𝑜} \in 𝑵$
15	10 10 14	mp2an	$⊢ 1_{𝑜} +_{𝑵} 1_{𝑜} \in 𝑵$
16		ltpiord	$⊢ (1_{𝑜} \in 𝑵 \land 1_{𝑜} +_{𝑵} 1_{𝑜} \in 𝑵) \to (1_{𝑜} <_{𝑵} (1_{𝑜} +_{𝑵} 1_{𝑜}) \leftrightarrow 1_{𝑜} \in (1_{𝑜} +_{𝑵} 1_{𝑜}))$
17	10 15 16	mp2an	$⊢ 1_{𝑜} <_{𝑵} (1_{𝑜} +_{𝑵} 1_{𝑜}) \leftrightarrow 1_{𝑜} \in (1_{𝑜} +_{𝑵} 1_{𝑜})$
18	13 17	mpbir	$⊢ 1_{𝑜} <_{𝑵} (1_{𝑜} +_{𝑵} 1_{𝑜})$

Metamath Proof Explorer