Theorem 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	$$⊢\left(0\in ℝ\wedge 0\in ℝ\wedge 0\in ℝ\right)\to \left(0{-}_{ℝ}0=0\leftrightarrow 0+0=0\right)$$
3	1 1 1 2	mp3an	$$⊢0{-}_{ℝ}0=0\leftrightarrow 0+0=0$$
4		df-ne	$$⊢0{-}_{ℝ}0\ne 0\leftrightarrow \neg 0{-}_{ℝ}0=0$$
5		sn-00idlem2	$$⊢0{-}_{ℝ}0\ne 0\to 0{-}_{ℝ}0=1$$
6		sn-00idlem3	$$⊢0{-}_{ℝ}0=1\to 0+0=0$$
7	5 6	syl	$$⊢0{-}_{ℝ}0\ne 0\to 0+0=0$$
8	4 7	sylbir	$$⊢\neg 0{-}_{ℝ}0=0\to 0+0=0$$
9	3 8	sylnbir	$$⊢\neg 0+0=0\to 0+0=0$$
10	9	pm2.18i	$$⊢0+0=0$$