Metamath Proof Explorer


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 syl5bb
 |-  ( 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