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 addlidi ⊢ ( 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 breq2 ⊢ ( 𝑥 = 1 → ( 0 < 𝑥 ↔ 0 < 1 ) )
35 34 imbi2d ⊢ ( 𝑥 = 1 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 1 ) ) )
36 breq2 ⊢ ( 𝑥 = 𝑦 → ( 0 < 𝑥 ↔ 0 < 𝑦 ) )
37 36 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝑦 ) ) )
38 breq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑦 + 1 ) ) )
39 38 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
40 breq2 ⊢ ( 𝑥 = 𝐴 → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
41 40 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝐴 ) ) )
42 id ⊢ ( 0 < 1 → 0 < 1 )
43 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℕ )
44 43 nnred ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ )
45 1red ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 1 ∈ ℝ )
46 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 𝑦 )
47 simp2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 1 )
48 44 45 46 47 addgt0d ⊢ ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < ( 𝑦 + 1 ) )
49 48 3exp ⊢ ( 𝑦 ∈ ℕ → ( 0 < 1 → ( 0 < 𝑦 → 0 < ( 𝑦 + 1 ) ) ) )
50 49 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 0 < 1 → 0 < 𝑦 ) → ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
51 35 37 39 41 42 50 nnind ⊢ ( 𝐴 ∈ ℕ → ( 0 < 1 → 0 < 𝐴 ) )
52 51 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 0 < 𝐴 )
53 52 gt0ne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 𝐴 ≠ 0 )
54 33 53 jaodan ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 1 < 0 ∨ 0 < 1 ) ) → 𝐴 ≠ 0 )
55 5 54 mpan2 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )