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 ( 𝐴 ∈ ℕ → 𝐴 ≠ 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 ⊢ ( 𝑥 = 1 → ( 𝑥 < 0 ↔ 1 < 0 ) )
7 6 imbi2d ⊢ ( 𝑥 = 1 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 1 < 0 ) ) )
8 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 < 0 ↔ 𝑦 < 0 ) )
9 8 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 𝑦 < 0 ) ) )
10 breq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 < 0 ↔ ( 𝑦 + 1 ) < 0 ) )
11 10 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
12 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 < 0 ↔ 𝐴 < 0 ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 𝐴 < 0 ) ) )
14 id ⊢ ( 1 < 0 → 1 < 0 )
15 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 ∈ ℕ )
16 15 nnred ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 ∈ ℝ )
17 1red ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 1 ∈ ℝ )
18 16 17 readdcld ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) ∈ ℝ )
19 3 2 readdcli ⊢ ( 0 + 1 ) ∈ ℝ
20 19 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 0 + 1 ) ∈ ℝ )
21 0red ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 0 ∈ ℝ )
22 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 < 0 )
23 16 21 17 22 ltadd1dd ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) < ( 0 + 1 ) )
24 ax-1cn ⊢ 1 ∈ ℂ
25 24 addid2i ⊢ ( 0 + 1 ) = 1
26 simp2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 1 < 0 )
27 25 26 eqbrtrid ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 0 + 1 ) < 0 )
28 18 20 21 23 27 lttrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) < 0 )
29 28 3exp ⊢ ( 𝑦 ∈ ℕ → ( 1 < 0 → ( 𝑦 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
30 29 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 1 < 0 → 𝑦 < 0 ) → ( 1 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
31 7 9 11 13 14 30 nnind ⊢ ( 𝐴 ∈ ℕ → ( 1 < 0 → 𝐴 < 0 ) )
32 31 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ 1 < 0 ) → 𝐴 < 0 )
33 32 lt0ne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 1 < 0 ) → 𝐴 ≠ 0 )
34 33 ex ⊢ ( 𝐴 ∈ ℕ → ( 1 < 0 → 𝐴 ≠ 0 ) )
35 breq2 ⊢ ( 𝑥 = 1 → ( 0 < 𝑥 ↔ 0 < 1 ) )
36 35 imbi2d ⊢ ( 𝑥 = 1 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 1 ) ) )
37 breq2 ⊢ ( 𝑥 = 𝑦 → ( 0 < 𝑥 ↔ 0 < 𝑦 ) )
38 37 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝑦 ) ) )
39 breq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑦 + 1 ) ) )
40 39 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
41 breq2 ⊢ ( 𝑥 = 𝐴 → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
42 41 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝐴 ) ) )
43 id ⊢ ( 0 < 1 → 0 < 1 )
44 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℕ )
45 44 nnred ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ )
46 1red ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 1 ∈ ℝ )
47 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 𝑦 )
48 simp2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 1 )
49 45 46 47 48 addgt0d ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < ( 𝑦 + 1 ) )
50 49 3exp ⊢ ( 𝑦 ∈ ℕ → ( 0 < 1 → ( 0 < 𝑦 → 0 < ( 𝑦 + 1 ) ) ) )
51 50 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 0 < 1 → 0 < 𝑦 ) → ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
52 36 38 40 42 43 51 nnind ⊢ ( 𝐴 ∈ ℕ → ( 0 < 1 → 0 < 𝐴 ) )
53 52 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 0 < 𝐴 )
54 53 gt0ne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 𝐴 ≠ 0 )
55 54 ex ⊢ ( 𝐴 ∈ ℕ → ( 0 < 1 → 𝐴 ≠ 0 ) )
56 34 55 jaod ⊢ ( 𝐴 ∈ ℕ → ( ( 1 < 0 ∨ 0 < 1 ) → 𝐴 ≠ 0 ) )
57 5 56 mpi ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )