This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )