sn-00id

Description: 00id proven without ax-mulcom but using ax-1ne0 . (Though note that the current version of 00id can be changed to avoid ax-icn , ax-addcl , ax-mulcl , ax-i2m1 , ax-cnre . Most of this is by using 0cnALT3 instead of 0cn ). (Contributed by SN, 25-Dec-2023) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	sn-00id	$⊢ 0 + 0 = 0$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		resubadd	$⊢ (0 \in ℝ \land 0 \in ℝ \land 0 \in ℝ) \to (0 -_{ℝ} 0 = 0 \leftrightarrow 0 + 0 = 0)$
3	1 1 1 2	mp3an	$⊢ 0 -_{ℝ} 0 = 0 \leftrightarrow 0 + 0 = 0$
4	3	necon3abii	$⊢ 0 -_{ℝ} 0 \neq 0 \leftrightarrow \neg 0 + 0 = 0$
5		sn-00idlem2	$⊢ 0 -_{ℝ} 0 \neq 0 \to 0 -_{ℝ} 0 = 1$
6		sn-00idlem3	$⊢ 0 -_{ℝ} 0 = 1 \to 0 + 0 = 0$
7	5 6	syl	$⊢ 0 -_{ℝ} 0 \neq 0 \to 0 + 0 = 0$
8	4 7	sylbir	$⊢ \neg 0 + 0 = 0 \to 0 + 0 = 0$
9	8	pm2.18i	$⊢ 0 + 0 = 0$

Metamath Proof Explorer

Theorem sn-00id

Proof