Metamath Proof Explorer

Theorem sn-nnne0

Description: nnne0 without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion sn-nnne0 ⊢ A ∈ ℕ → A ≠ 0

Proof

Step Hyp Ref Expression
1 0ne1 ⊢ 0 ≠ 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 2 3 lttri2i ⊢ 0 ≠ 1 ↔ 0 < 1 ∨ 1 < 0
5 1 4 mpbi ⊢ 0 < 1 ∨ 1 < 0
6 breq2 ⊢ x = 1 → 0 < x ↔ 0 < 1
7 breq2 ⊢ x = y → 0 < x ↔ 0 < y
8 breq2 ⊢ x = y + 1 → 0 < x ↔ 0 < y + 1
9 breq2 ⊢ x = A → 0 < x ↔ 0 < A
10 id ⊢ 0 < 1 → 0 < 1
11 nnre ⊢ y ∈ ℕ → y ∈ ℝ
12 11 ad2antlr ⊢ 0 < 1 ∧ y ∈ ℕ ∧ 0 < y → y ∈ ℝ
13 1red ⊢ 0 < 1 ∧ y ∈ ℕ ∧ 0 < y → 1 ∈ ℝ
14 simpr ⊢ 0 < 1 ∧ y ∈ ℕ ∧ 0 < y → 0 < y
15 simpll ⊢ 0 < 1 ∧ y ∈ ℕ ∧ 0 < y → 0 < 1
16 12 13 14 15 sn-addgt0d ⊢ 0 < 1 ∧ y ∈ ℕ ∧ 0 < y → 0 < y + 1
17 6 7 8 9 10 16 nnindd ⊢ 0 < 1 ∧ A ∈ ℕ → 0 < A
18 17 gt0ne0d ⊢ 0 < 1 ∧ A ∈ ℕ → A ≠ 0
19 18 ancoms ⊢ A ∈ ℕ ∧ 0 < 1 → A ≠ 0
20 breq1 ⊢ x = 1 → x < 0 ↔ 1 < 0
21 breq1 ⊢ x = y → x < 0 ↔ y < 0
22 breq1 ⊢ x = y + 1 → x < 0 ↔ y + 1 < 0
23 breq1 ⊢ x = A → x < 0 ↔ A < 0
24 id ⊢ 1 < 0 → 1 < 0
25 11 ad2antlr ⊢ 1 < 0 ∧ y ∈ ℕ ∧ y < 0 → y ∈ ℝ
26 1red ⊢ 1 < 0 ∧ y ∈ ℕ ∧ y < 0 → 1 ∈ ℝ
27 simpr ⊢ 1 < 0 ∧ y ∈ ℕ ∧ y < 0 → y < 0
28 simpll ⊢ 1 < 0 ∧ y ∈ ℕ ∧ y < 0 → 1 < 0
29 25 26 27 28 sn-addlt0d ⊢ 1 < 0 ∧ y ∈ ℕ ∧ y < 0 → y + 1 < 0
30 20 21 22 23 24 29 nnindd ⊢ 1 < 0 ∧ A ∈ ℕ → A < 0
31 30 lt0ne0d ⊢ 1 < 0 ∧ A ∈ ℕ → A ≠ 0
32 31 ancoms ⊢ A ∈ ℕ ∧ 1 < 0 → A ≠ 0
33 19 32 jaodan ⊢ A ∈ ℕ ∧ 0 < 1 ∨ 1 < 0 → A ≠ 0
34 5 33 mpan2 ⊢ A ∈ ℕ → A ≠ 0