# 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}\in ℕ\to {A}\ne 0$

### Proof

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