Theorem nlt1pi

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

	Ref	Expression
Assertion	nlt1pi	⊢ ¬ 𝐴 <N 1o

Proof

Step	Hyp	Ref	Expression
1		elni	⊢ ( 𝐴 ∈ N ↔ ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) )
2	1	simprbi	⊢ ( 𝐴 ∈ N → 𝐴 ≠ ∅ )
3		noel	⊢ ¬ 𝐴 ∈ ∅
4		1pi	⊢ 1o ∈ N
5		ltpiord	⊢ ( ( 𝐴 ∈ N ∧ 1o ∈ N ) → ( 𝐴 <N 1o ↔ 𝐴 ∈ 1o ) )
6	4 5	mpan2	⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o ↔ 𝐴 ∈ 1o ) )
7		df-1o	⊢ 1o = suc ∅
8	7	eleq2i	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 ∈ suc ∅ )
9		elsucg	⊢ ( 𝐴 ∈ N → ( 𝐴 ∈ suc ∅ ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
10	8 9	syl5bb	⊢ ( 𝐴 ∈ N → ( 𝐴 ∈ 1o ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
11	6 10	bitrd	⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
12	11	biimpa	⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) )
13	12	ord	⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → ( ¬ 𝐴 ∈ ∅ → 𝐴 = ∅ ) )
14	3 13	mpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → 𝐴 = ∅ )
15	14	ex	⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o → 𝐴 = ∅ ) )
16	15	necon3ad	⊢ ( 𝐴 ∈ N → ( 𝐴 ≠ ∅ → ¬ 𝐴 <N 1o ) )
17	2 16	mpd	⊢ ( 𝐴 ∈ N → ¬ 𝐴 <N 1o )
18		ltrelpi	⊢ <N ⊆ ( N × N )
19	18	brel	⊢ ( 𝐴 <N 1o → ( 𝐴 ∈ N ∧ 1o ∈ N ) )
20	19	simpld	⊢ ( 𝐴 <N 1o → 𝐴 ∈ N )
21	20	con3i	⊢ ( ¬ 𝐴 ∈ N → ¬ 𝐴 <N 1o )
22	17 21	pm2.61i	⊢ ¬ 𝐴 <N 1o