Theorem nlt1pi 9071

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

Assertion

Ref	Expression
nlt1pi	|- -. A <N 1o

Proof of Theorem nlt1pi

Step	Hyp	Ref	Expression
1		elni 9041	. . . 4 |- ( A e. N. <-> ( A e. om /\ A =/= (/) ) )
2	1	simprbi 461	. . 3 |- ( A e. N. -> A =/= (/) )
3		noel 3638	. . . . . 6 |- -. A e. (/)
4		1pi 9048	. . . . . . . . . 10 |- 1o e. N.
5		ltpiord 9052	. . . . . . . . . 10 |- ( ( A e. N. /\ 1o e. N. ) -> ( A <N 1o <-> A e. 1o ) )
6	4, 5	mpan2 666	. . . . . . . . 9 |- ( A e. N. -> ( A <N 1o <-> A e. 1o ) )
7		df-1o 6916	. . . . . . . . . . 11 |- 1o = suc (/)
8	7	eleq2i 2505	. . . . . . . . . 10 |- ( A e. 1o <-> A e. suc (/) )
9		elsucg 4782	. . . . . . . . . 10 |- ( A e. N. -> ( A e. suc (/) <-> ( A e. (/) \/ A = (/) ) ) )
10	8, 9	syl5bb 257	. . . . . . . . 9 |- ( A e. N. -> ( A e. 1o <-> ( A e. (/) \/ A = (/) ) ) )
11	6, 10	bitrd 253	. . . . . . . 8 |- ( A e. N. -> ( A <N 1o <-> ( A e. (/) \/ A = (/) ) ) )
12	11	biimpa 481	. . . . . . 7 |- ( ( A e. N. /\ A <N 1o ) -> ( A e. (/) \/ A = (/) ) )
13	12	ord 377	. . . . . 6 |- ( ( A e. N. /\ A <N 1o ) -> ( -. A e. (/) -> A = (/) ) )
14	3, 13	mpi 17	. . . . 5 |- ( ( A e. N. /\ A <N 1o ) -> A = (/) )
15	14	ex 434	. . . 4 |- ( A e. N. -> ( A <N 1o -> A = (/) ) )
16	15	necon3ad 2642	. . 3 |- ( A e. N. -> ( A =/= (/) -> -. A <N 1o ) )
17	2, 16	mpd 15	. 2 |- ( A e. N. -> -. A <N 1o )
18		ltrelpi 9054	. . . . 5 |- <N C_ ( N. X. N. )
19	18	brel 4883	. . . 4 |- ( A <N 1o -> ( A e. N. /\ 1o e. N. ) )
20	19	simpld 456	. . 3 |- ( A <N 1o -> A e. N. )
21	20	con3i 135	. 2 |- ( -. A e. N. -> -. A <N 1o )
22	17, 21	pm2.61i 164	1 |- -. A <N 1o

Syntax hints:   -. wn 3   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1364   e. wcel 1761   =/= wne 2604   (/)c0 3634   class class class wbr 4289   suc csuc 4717   omcom 6475   1oc1o 6909   N.cnpi 9007   <N clti 9010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-tr 4383  df-eprel 4628  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-om 6476  df-1o 6916  df-ni 9037  df-lti 9040

This theorem is referenced by:  indpi  9072  pinq  9092  archnq  9145