Metamath Proof Explorer

Theorem nnge1

Description: A positive integer is one or greater. (Contributed by NM, 25-Aug-1999)

Ref Expression
Assertion nnge1 
|- ( A e. NN -> 1 <_ A )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = 1 -> ( 1 <_ x <-> 1 <_ 1 ) )
2 breq2 
 |-  ( x = y -> ( 1 <_ x <-> 1 <_ y ) )
3 breq2 
 |-  ( x = ( y + 1 ) -> ( 1 <_ x <-> 1 <_ ( y + 1 ) ) )
4 breq2 
 |-  ( x = A -> ( 1 <_ x <-> 1 <_ A ) )
5 1le1 
 |-  1 <_ 1
6 nnre 
 |-  ( y e. NN -> y e. RR )
7 recn 
 |-  ( y e. RR -> y e. CC )
8 7 addid1d 
 |-  ( y e. RR -> ( y + 0 ) = y )
9 8 breq2d 
 |-  ( y e. RR -> ( 1 <_ ( y + 0 ) <-> 1 <_ y ) )
10 0lt1 
 |-  0 < 1
11 0re 
 |-  0 e. RR
12 1re 
 |-  1 e. RR
13 axltadd 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ y e. RR ) -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
14 11 12 13 mp3an12 
 |-  ( y e. RR -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
15 10 14 mpi 
 |-  ( y e. RR -> ( y + 0 ) < ( y + 1 ) )
16 readdcl 
 |-  ( ( y e. RR /\ 0 e. RR ) -> ( y + 0 ) e. RR )
17 11 16 mpan2 
 |-  ( y e. RR -> ( y + 0 ) e. RR )
18 peano2re 
 |-  ( y e. RR -> ( y + 1 ) e. RR )
19 lttr 
 |-  ( ( ( y + 0 ) e. RR /\ ( y + 1 ) e. RR /\ 1 e. RR ) -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
20 12 19 mp3an3 
 |-  ( ( ( y + 0 ) e. RR /\ ( y + 1 ) e. RR ) -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
21 17 18 20 syl2anc 
 |-  ( y e. RR -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
22 15 21 mpand 
 |-  ( y e. RR -> ( ( y + 1 ) < 1 -> ( y + 0 ) < 1 ) )
23 22 con3d 
 |-  ( y e. RR -> ( -. ( y + 0 ) < 1 -> -. ( y + 1 ) < 1 ) )
24 lenlt 
 |-  ( ( 1 e. RR /\ ( y + 0 ) e. RR ) -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
25 12 17 24 sylancr 
 |-  ( y e. RR -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
26 lenlt 
 |-  ( ( 1 e. RR /\ ( y + 1 ) e. RR ) -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
27 12 18 26 sylancr 
 |-  ( y e. RR -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
28 23 25 27 3imtr4d 
 |-  ( y e. RR -> ( 1 <_ ( y + 0 ) -> 1 <_ ( y + 1 ) ) )
29 9 28 sylbird 
 |-  ( y e. RR -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
30 6 29 syl 
 |-  ( y e. NN -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
31 1 2 3 4 5 30 nnind 
 |-  ( A e. NN -> 1 <_ A )