Metamath Proof Explorer

Theorem nnne0

Description: A positive integer is nonzero. See nnne0ALT for a shorter proof using ax-pre-mulgt0 . This proof avoids 0lt1 , and thus ax-pre-mulgt0 , by splitting ax-1ne0 into the two separate cases 0 < 1 and 1 < 0 . (Contributed by NM, 27-Sep-1999) Remove dependency on ax-pre-mulgt0 . (Revised by Steven Nguyen, 30-Jan-2023)

Ref Expression
Assertion nnne0 
|- ( A e. NN -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 ax-1ne0 
 |-  1 =/= 0
2 1re 
 |-  1 e. RR
3 0re 
 |-  0 e. RR
4 2 3 lttri2i 
 |-  ( 1 =/= 0 <-> ( 1 < 0 \/ 0 < 1 ) )
5 1 4 mpbi 
 |-  ( 1 < 0 \/ 0 < 1 )
6 breq1 
 |-  ( x = 1 -> ( x < 0 <-> 1 < 0 ) )
7 6 imbi2d 
 |-  ( x = 1 -> ( ( 1 < 0 -> x < 0 ) <-> ( 1 < 0 -> 1 < 0 ) ) )
8 breq1 
 |-  ( x = y -> ( x < 0 <-> y < 0 ) )
9 8 imbi2d 
 |-  ( x = y -> ( ( 1 < 0 -> x < 0 ) <-> ( 1 < 0 -> y < 0 ) ) )
10 breq1 
 |-  ( x = ( y + 1 ) -> ( x < 0 <-> ( y + 1 ) < 0 ) )
11 10 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( 1 < 0 -> x < 0 ) <-> ( 1 < 0 -> ( y + 1 ) < 0 ) ) )
12 breq1 
 |-  ( x = A -> ( x < 0 <-> A < 0 ) )
13 12 imbi2d 
 |-  ( x = A -> ( ( 1 < 0 -> x < 0 ) <-> ( 1 < 0 -> A < 0 ) ) )
14 id 
 |-  ( 1 < 0 -> 1 < 0 )
15 simp1 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> y e. NN )
16 15 nnred 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> y e. RR )
17 1red 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> 1 e. RR )
18 16 17 readdcld 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( y + 1 ) e. RR )
19 3 2 readdcli 
 |-  ( 0 + 1 ) e. RR
20 19 a1i 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( 0 + 1 ) e. RR )
21 0red 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> 0 e. RR )
22 simp3 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> y < 0 )
23 16 21 17 22 ltadd1dd 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( y + 1 ) < ( 0 + 1 ) )
24 ax-1cn 
 |-  1 e. CC
25 24 addid2i 
 |-  ( 0 + 1 ) = 1
26 simp2 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> 1 < 0 )
27 25 26 eqbrtrid 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( 0 + 1 ) < 0 )
28 18 20 21 23 27 lttrd 
 |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( y + 1 ) < 0 )
29 28 3exp 
 |-  ( y e. NN -> ( 1 < 0 -> ( y < 0 -> ( y + 1 ) < 0 ) ) )
30 29 a2d 
 |-  ( y e. NN -> ( ( 1 < 0 -> y < 0 ) -> ( 1 < 0 -> ( y + 1 ) < 0 ) ) )
31 7 9 11 13 14 30 nnind 
 |-  ( A e. NN -> ( 1 < 0 -> A < 0 ) )
32 31 imp 
 |-  ( ( A e. NN /\ 1 < 0 ) -> A < 0 )
33 32 lt0ne0d 
 |-  ( ( A e. NN /\ 1 < 0 ) -> A =/= 0 )
34 33 ex 
 |-  ( A e. NN -> ( 1 < 0 -> A =/= 0 ) )
35 breq2 
 |-  ( x = 1 -> ( 0 < x <-> 0 < 1 ) )
36 35 imbi2d 
 |-  ( x = 1 -> ( ( 0 < 1 -> 0 < x ) <-> ( 0 < 1 -> 0 < 1 ) ) )
37 breq2 
 |-  ( x = y -> ( 0 < x <-> 0 < y ) )
38 37 imbi2d 
 |-  ( x = y -> ( ( 0 < 1 -> 0 < x ) <-> ( 0 < 1 -> 0 < y ) ) )
39 breq2 
 |-  ( x = ( y + 1 ) -> ( 0 < x <-> 0 < ( y + 1 ) ) )
40 39 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( 0 < 1 -> 0 < x ) <-> ( 0 < 1 -> 0 < ( y + 1 ) ) ) )
41 breq2 
 |-  ( x = A -> ( 0 < x <-> 0 < A ) )
42 41 imbi2d 
 |-  ( x = A -> ( ( 0 < 1 -> 0 < x ) <-> ( 0 < 1 -> 0 < A ) ) )
43 id 
 |-  ( 0 < 1 -> 0 < 1 )
44 simp1 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> y e. NN )
45 44 nnred 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> y e. RR )
46 1red 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> 1 e. RR )
47 simp3 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> 0 < y )
48 simp2 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> 0 < 1 )
49 45 46 47 48 addgt0d 
 |-  ( ( y e. NN /\ 0 < 1 /\ 0 < y ) -> 0 < ( y + 1 ) )
50 49 3exp 
 |-  ( y e. NN -> ( 0 < 1 -> ( 0 < y -> 0 < ( y + 1 ) ) ) )
51 50 a2d 
 |-  ( y e. NN -> ( ( 0 < 1 -> 0 < y ) -> ( 0 < 1 -> 0 < ( y + 1 ) ) ) )
52 36 38 40 42 43 51 nnind 
 |-  ( A e. NN -> ( 0 < 1 -> 0 < A ) )
53 52 imp 
 |-  ( ( A e. NN /\ 0 < 1 ) -> 0 < A )
54 53 gt0ne0d 
 |-  ( ( A e. NN /\ 0 < 1 ) -> A =/= 0 )
55 54 ex 
 |-  ( A e. NN -> ( 0 < 1 -> A =/= 0 ) )
56 34 55 jaod 
 |-  ( A e. NN -> ( ( 1 < 0 \/ 0 < 1 ) -> A =/= 0 ) )
57 5 56 mpi 
 |-  ( A e. NN -> A =/= 0 )