# 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 ∈ ℕ → A ≠ 0$

### Proof

Step Hyp Ref Expression
1 ax-1ne0 $⊢ 1 ≠ 0$
2 1re $⊢ 1 ∈ ℝ$
3 0re $⊢ 0 ∈ ℝ$
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 ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y ∈ ℕ$
16 15 nnred $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y ∈ ℝ$
17 1red $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → 1 ∈ ℝ$
18 16 17 readdcld $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y + 1 ∈ ℝ$
19 3 2 readdcli $⊢ 0 + 1 ∈ ℝ$
20 19 a1i $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → 0 + 1 ∈ ℝ$
21 0red $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → 0 ∈ ℝ$
22 simp3 $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y < 0$
23 16 21 17 22 ltadd1dd $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y + 1 < 0 + 1$
24 ax-1cn $⊢ 1 ∈ ℂ$
25 24 addid2i $⊢ 0 + 1 = 1$
26 simp2 $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → 1 < 0$
27 25 26 eqbrtrid $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → 0 + 1 < 0$
28 18 20 21 23 27 lttrd $⊢ y ∈ ℕ ∧ 1 < 0 ∧ y < 0 → y + 1 < 0$
29 28 3exp $⊢ y ∈ ℕ → 1 < 0 → y < 0 → y + 1 < 0$
30 29 a2d $⊢ y ∈ ℕ → 1 < 0 → y < 0 → 1 < 0 → y + 1 < 0$
31 7 9 11 13 14 30 nnind $⊢ A ∈ ℕ → 1 < 0 → A < 0$
32 31 imp $⊢ A ∈ ℕ ∧ 1 < 0 → A < 0$
33 32 lt0ne0d $⊢ A ∈ ℕ ∧ 1 < 0 → A ≠ 0$
34 33 ex $⊢ A ∈ ℕ → 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 ∈ ℕ ∧ 0 < 1 ∧ 0 < y → y ∈ ℕ$
45 44 nnred $⊢ y ∈ ℕ ∧ 0 < 1 ∧ 0 < y → y ∈ ℝ$
46 1red $⊢ y ∈ ℕ ∧ 0 < 1 ∧ 0 < y → 1 ∈ ℝ$
47 simp3 $⊢ y ∈ ℕ ∧ 0 < 1 ∧ 0 < y → 0 < y$
48 simp2 $⊢ y ∈ ℕ ∧ 0 < 1 ∧ 0 < y → 0 < 1$
49 45 46 47 48 addgt0d $⊢ y ∈ ℕ ∧ 0 < 1 ∧ 0 < y → 0 < y + 1$
50 49 3exp $⊢ y ∈ ℕ → 0 < 1 → 0 < y → 0 < y + 1$
51 50 a2d $⊢ y ∈ ℕ → 0 < 1 → 0 < y → 0 < 1 → 0 < y + 1$
52 36 38 40 42 43 51 nnind $⊢ A ∈ ℕ → 0 < 1 → 0 < A$
53 52 imp $⊢ A ∈ ℕ ∧ 0 < 1 → 0 < A$
54 53 gt0ne0d $⊢ A ∈ ℕ ∧ 0 < 1 → A ≠ 0$
55 54 ex $⊢ A ∈ ℕ → 0 < 1 → A ≠ 0$
56 34 55 jaod $⊢ A ∈ ℕ → 1 < 0 ∨ 0 < 1 → A ≠ 0$
57 5 56 mpi $⊢ A ∈ ℕ → A ≠ 0$