Metamath Proof Explorer


Theorem sn-nnne0

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

Ref Expression
Assertion sn-nnne0 ( 𝐴 ∈ ℕ → 𝐴 ≠ 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 ( 𝑥 = 1 → ( 0 < 𝑥 ↔ 0 < 1 ) )
7 breq2 ( 𝑥 = 𝑦 → ( 0 < 𝑥 ↔ 0 < 𝑦 ) )
8 breq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑦 + 1 ) ) )
9 breq2 ( 𝑥 = 𝐴 → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
10 id ( 0 < 1 → 0 < 1 )
11 nnre ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
12 11 ad2antlr ( ( ( 0 < 1 ∧ 𝑦 ∈ ℕ ) ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ )
13 1red ( ( ( 0 < 1 ∧ 𝑦 ∈ ℕ ) ∧ 0 < 𝑦 ) → 1 ∈ ℝ )
14 simpr ( ( ( 0 < 1 ∧ 𝑦 ∈ ℕ ) ∧ 0 < 𝑦 ) → 0 < 𝑦 )
15 simpll ( ( ( 0 < 1 ∧ 𝑦 ∈ ℕ ) ∧ 0 < 𝑦 ) → 0 < 1 )
16 12 13 14 15 sn-addgt0d ( ( ( 0 < 1 ∧ 𝑦 ∈ ℕ ) ∧ 0 < 𝑦 ) → 0 < ( 𝑦 + 1 ) )
17 6 7 8 9 10 16 nnindd ( ( 0 < 1 ∧ 𝐴 ∈ ℕ ) → 0 < 𝐴 )
18 17 gt0ne0d ( ( 0 < 1 ∧ 𝐴 ∈ ℕ ) → 𝐴 ≠ 0 )
19 18 ancoms ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 𝐴 ≠ 0 )
20 breq1 ( 𝑥 = 1 → ( 𝑥 < 0 ↔ 1 < 0 ) )
21 breq1 ( 𝑥 = 𝑦 → ( 𝑥 < 0 ↔ 𝑦 < 0 ) )
22 breq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 < 0 ↔ ( 𝑦 + 1 ) < 0 ) )
23 breq1 ( 𝑥 = 𝐴 → ( 𝑥 < 0 ↔ 𝐴 < 0 ) )
24 id ( 1 < 0 → 1 < 0 )
25 11 ad2antlr ( ( ( 1 < 0 ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 < 0 ) → 𝑦 ∈ ℝ )
26 1red ( ( ( 1 < 0 ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 < 0 ) → 1 ∈ ℝ )
27 simpr ( ( ( 1 < 0 ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 < 0 ) → 𝑦 < 0 )
28 simpll ( ( ( 1 < 0 ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 < 0 ) → 1 < 0 )
29 25 26 27 28 sn-addlt0d ( ( ( 1 < 0 ∧ 𝑦 ∈ ℕ ) ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) < 0 )
30 20 21 22 23 24 29 nnindd ( ( 1 < 0 ∧ 𝐴 ∈ ℕ ) → 𝐴 < 0 )
31 30 lt0ne0d ( ( 1 < 0 ∧ 𝐴 ∈ ℕ ) → 𝐴 ≠ 0 )
32 31 ancoms ( ( 𝐴 ∈ ℕ ∧ 1 < 0 ) → 𝐴 ≠ 0 )
33 19 32 jaodan ( ( 𝐴 ∈ ℕ ∧ ( 0 < 1 ∨ 1 < 0 ) ) → 𝐴 ≠ 0 )
34 5 33 mpan2 ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )