Metamath Proof Explorer


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 ∈ ℝ
2 resubadd ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 − 0 ) = 0 ↔ ( 0 + 0 ) = 0 ) )
3 1 1 1 2 mp3an ( ( 0 − 0 ) = 0 ↔ ( 0 + 0 ) = 0 )
4 df-ne ( ( 0 − 0 ) ≠ 0 ↔ ¬ ( 0 − 0 ) = 0 )
5 sn-00idlem2 ( ( 0 − 0 ) ≠ 0 → ( 0 − 0 ) = 1 )
6 sn-00idlem3 ( ( 0 − 0 ) = 1 → ( 0 + 0 ) = 0 )
7 5 6 syl ( ( 0 − 0 ) ≠ 0 → ( 0 + 0 ) = 0 )
8 4 7 sylbir ( ¬ ( 0 − 0 ) = 0 → ( 0 + 0 ) = 0 )
9 3 8 sylnbir ( ¬ ( 0 + 0 ) = 0 → ( 0 + 0 ) = 0 )
10 9 pm2.18i ( 0 + 0 ) = 0