Theorem nlt1pi

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

	Ref	Expression
Assertion	nlt1pi	|- -. A

Proof

Step	Hyp	Ref	Expression
1		elni	|- ( A e. N. <-> ( A e. _om /\ A =/= (/) ) )
2	1	simprbi	|- ( A e. N. -> A =/= (/) )
3		noel	|- -. A e. (/)
4		1pi	|- 1o e. N.
5		ltpiord	|- ( ( A e. N. /\ 1o e. N. ) -> ( A A e. 1o ) )
6	4 5	mpan2	|- ( A e. N. -> ( A A e. 1o ) )
7		df-1o	|- 1o = suc (/)
8	7	eleq2i	|- ( A e. 1o <-> A e. suc (/) )
9		elsucg	|- ( A e. N. -> ( A e. suc (/) <-> ( A e. (/) \/ A = (/) ) ) )
10	8 9	bitrid	|- ( A e. N. -> ( A e. 1o <-> ( A e. (/) \/ A = (/) ) ) )
11	6 10	bitrd	|- ( A e. N. -> ( A ( A e. (/) \/ A = (/) ) ) )
12	11	biimpa	|- ( ( A e. N. /\ A ( A e. (/) \/ A = (/) ) )
13	12	ord	|- ( ( A e. N. /\ A ( -. A e. (/) -> A = (/) ) )
14	3 13	mpi	|- ( ( A e. N. /\ A A = (/) )
15	14	ex	|- ( A e. N. -> ( A A = (/) ) )
16	15	necon3ad	|- ( A e. N. -> ( A =/= (/) -> -. A
17	2 16	mpd	|- ( A e. N. -> -. A
18		ltrelpi	|-
19	18	brel	|- ( A ( A e. N. /\ 1o e. N. ) )
20	19	simpld	|- ( A A e. N. )
21	20	con3i	|- ( -. A e. N. -> -. A
22	17 21	pm2.61i	|- -. A