# 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 )`
` |-  ( ( y e. NN /\ 1 < 0 /\ y < 0 ) -> ( y + 1 ) e. RR )`
` |-  ( 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`
` |-  ( 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 )`