nlt1pi

Description: No positive integer is less than one. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	nlt1pi	$⊢ \neg A <_{𝑵} 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		elni	$⊢ A \in 𝑵 \leftrightarrow (A \in ω \land A \neq \emptyset)$
2	1	simprbi	$⊢ A \in 𝑵 \to A \neq \emptyset$
3		noel	$⊢ \neg A \in \emptyset$
4		1pi	$⊢ 1_{𝑜} \in 𝑵$
5		ltpiord	$⊢ (A \in 𝑵 \land 1_{𝑜} \in 𝑵) \to (A <_{𝑵} 1_{𝑜} \leftrightarrow A \in 1_{𝑜})$
6	4 5	mpan2	$⊢ A \in 𝑵 \to (A <_{𝑵} 1_{𝑜} \leftrightarrow A \in 1_{𝑜})$
7		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
8	7	eleq2i	$⊢ A \in 1_{𝑜} \leftrightarrow A \in suc \emptyset$
9		elsucg	$⊢ A \in 𝑵 \to (A \in suc \emptyset \leftrightarrow (A \in \emptyset \lor A = \emptyset))$
10	8 9	syl5bb	$⊢ A \in 𝑵 \to (A \in 1_{𝑜} \leftrightarrow (A \in \emptyset \lor A = \emptyset))$
11	6 10	bitrd	$⊢ A \in 𝑵 \to (A <_{𝑵} 1_{𝑜} \leftrightarrow (A \in \emptyset \lor A = \emptyset))$
12	11	biimpa	$⊢ (A \in 𝑵 \land A <_{𝑵} 1_{𝑜}) \to (A \in \emptyset \lor A = \emptyset)$
13	12	ord	$⊢ (A \in 𝑵 \land A <_{𝑵} 1_{𝑜}) \to (\neg A \in \emptyset \to A = \emptyset)$
14	3 13	mpi	$⊢ (A \in 𝑵 \land A <_{𝑵} 1_{𝑜}) \to A = \emptyset$
15	14	ex	$⊢ A \in 𝑵 \to (A <_{𝑵} 1_{𝑜} \to A = \emptyset)$
16	15	necon3ad	$⊢ A \in 𝑵 \to (A \neq \emptyset \to \neg A <_{𝑵} 1_{𝑜})$
17	2 16	mpd	$⊢ A \in 𝑵 \to \neg A <_{𝑵} 1_{𝑜}$
18		ltrelpi	$⊢ <_{𝑵} \subseteq 𝑵 \times 𝑵$
19	18	brel	$⊢ A <_{𝑵} 1_{𝑜} \to (A \in 𝑵 \land 1_{𝑜} \in 𝑵)$
20	19	simpld	$⊢ A <_{𝑵} 1_{𝑜} \to A \in 𝑵$
21	20	con3i	$⊢ \neg A \in 𝑵 \to \neg A <_{𝑵} 1_{𝑜}$
22	17 21	pm2.61i	$⊢ \neg A <_{𝑵} 1_{𝑜}$

Metamath Proof Explorer

Theorem nlt1pi

Proof