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 e. RR
2		resubadd	|- ( ( 0 e. RR /\ 0 e. RR /\ 0 e. RR ) -> ( ( 0 -R 0 ) = 0 <-> ( 0 + 0 ) = 0 ) )
3	1 1 1 2	mp3an	|- ( ( 0 -R 0 ) = 0 <-> ( 0 + 0 ) = 0 )
4		df-ne	|- ( ( 0 -R 0 ) =/= 0 <-> -. ( 0 -R 0 ) = 0 )
5		sn-00idlem2	|- ( ( 0 -R 0 ) =/= 0 -> ( 0 -R 0 ) = 1 )
6		sn-00idlem3	|- ( ( 0 -R 0 ) = 1 -> ( 0 + 0 ) = 0 )
7	5 6	syl	|- ( ( 0 -R 0 ) =/= 0 -> ( 0 + 0 ) = 0 )
8	4 7	sylbir	|- ( -. ( 0 -R 0 ) = 0 -> ( 0 + 0 ) = 0 )
9	3 8	sylnbir	|- ( -. ( 0 + 0 ) = 0 -> ( 0 + 0 ) = 0 )
10	9	pm2.18i	|- ( 0 + 0 ) = 0