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 )