Theorem nlt1pi 9096

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 9066	. . . 4 |- ( A e. N. <-> ( A e. om /\ A =/= (/) ) )
2	1	simprbi 464	. . 3 |- ( A e. N. -> A =/= (/) )
3		noel 3662	. . . . . 6 |- -. A e. (/)
4		1pi 9073	. . . . . . . . . 10 |- 1o e. N.
5		ltpiord 9077	. . . . . . . . . 10 |- ( ( A e. N. /\ 1o e. N. ) -> ( A <N 1o <-> A e. 1o ) )
6	4, 5	mpan2 671	. . . . . . . . 9 |- ( A e. N. -> ( A <N 1o <-> A e. 1o ) )
7		df-1o 6941	. . . . . . . . . . 11 |- 1o = suc (/)
8	7	eleq2i 2507	. . . . . . . . . 10 |- ( A e. 1o <-> A e. suc (/) )
9		elsucg 4807	. . . . . . . . . 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 484	. . . . . . 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 2668	. . 3 |- ( A e. N. -> ( A =/= (/) -> -. A <N 1o ) )
17	2, 16	mpd 15	. 2 |- ( A e. N. -> -. A <N 1o )
18		ltrelpi 9079	. . . . 5 |- <N C_ ( N. X. N. )
19	18	brel 4908	. . . 4 |- ( A <N 1o -> ( A e. N. /\ 1o e. N. ) )
20	19	simpld 459	. . 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 1369   e. wcel 1756   =/= wne 2620   (/)c0 3658   class class class wbr 4313   suc csuc 4742   omcom 6497   1oc1o 6934   N.cnpi 9032   <N clti 9035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552  ax-un 6393

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-om 6498  df-1o 6941  df-ni 9062  df-lti 9065

This theorem is referenced by:  indpi  9097  pinq  9117  archnq  9170