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 |
| 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 | 3 | necon3abii | |- ( ( 0 -R 0 ) =/= 0 <-> -. ( 0 + 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 + 0 ) = 0 -> ( 0 + 0 ) = 0 ) |
| 9 | 8 | pm2.18i | |- ( 0 + 0 ) = 0 |