# Metamath Proof Explorer

## Theorem 00id

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion 00id
`|- ( 0 + 0 ) = 0`

### Proof

Step Hyp Ref Expression
1 0re
` |-  0 e. RR`
2 ax-rnegex
` |-  ( 0 e. RR -> E. c e. RR ( 0 + c ) = 0 )`
3 oveq2
` |-  ( c = 0 -> ( 0 + c ) = ( 0 + 0 ) )`
4 3 eqeq1d
` |-  ( c = 0 -> ( ( 0 + c ) = 0 <-> ( 0 + 0 ) = 0 ) )`
5 4 biimpd
` |-  ( c = 0 -> ( ( 0 + c ) = 0 -> ( 0 + 0 ) = 0 ) )`
` |-  ( c = 0 -> ( ( c e. RR /\ ( 0 + c ) = 0 ) -> ( 0 + 0 ) = 0 ) )`
7 ax-rrecex
` |-  ( ( c e. RR /\ c =/= 0 ) -> E. y e. RR ( c x. y ) = 1 )`
` |-  ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) -> E. y e. RR ( c x. y ) = 1 )`
9 simplll
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> c e. RR )`
10 9 recnd
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> c e. CC )`
11 simprl
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> y e. RR )`
12 11 recnd
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> y e. CC )`
13 0cn
` |-  0 e. CC`
14 mulass
` |-  ( ( c e. CC /\ y e. CC /\ 0 e. CC ) -> ( ( c x. y ) x. 0 ) = ( c x. ( y x. 0 ) ) )`
15 13 14 mp3an3
` |-  ( ( c e. CC /\ y e. CC ) -> ( ( c x. y ) x. 0 ) = ( c x. ( y x. 0 ) ) )`
16 10 12 15 syl2anc
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( c x. y ) x. 0 ) = ( c x. ( y x. 0 ) ) )`
17 oveq1
` |-  ( ( c x. y ) = 1 -> ( ( c x. y ) x. 0 ) = ( 1 x. 0 ) )`
18 13 mulid2i
` |-  ( 1 x. 0 ) = 0`
19 17 18 eqtrdi
` |-  ( ( c x. y ) = 1 -> ( ( c x. y ) x. 0 ) = 0 )`
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( c x. y ) x. 0 ) = 0 )`
21 16 20 eqtr3d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( c x. ( y x. 0 ) ) = 0 )`
22 21 oveq1d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( c x. ( y x. 0 ) ) + 0 ) = ( 0 + 0 ) )`
23 simpllr
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( 0 + c ) = 0 )`
24 23 oveq1d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( 0 + c ) x. ( y x. 0 ) ) = ( 0 x. ( y x. 0 ) ) )`
25 remulcl
` |-  ( ( y e. RR /\ 0 e. RR ) -> ( y x. 0 ) e. RR )`
26 1 25 mpan2
` |-  ( y e. RR -> ( y x. 0 ) e. RR )`
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( y x. 0 ) e. RR )`
28 27 recnd
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( y x. 0 ) e. CC )`
` |-  ( ( 0 e. CC /\ c e. CC /\ ( y x. 0 ) e. CC ) -> ( ( 0 + c ) x. ( y x. 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) )`
30 13 10 28 29 mp3an2i
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( 0 + c ) x. ( y x. 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) )`
31 24 30 eqtr3d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( 0 x. ( y x. 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) )`
32 31 oveq1d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( 0 x. ( y x. 0 ) ) + 0 ) = ( ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) + 0 ) )`
33 remulcl
` |-  ( ( 0 e. RR /\ ( y x. 0 ) e. RR ) -> ( 0 x. ( y x. 0 ) ) e. RR )`
34 1 26 33 sylancr
` |-  ( y e. RR -> ( 0 x. ( y x. 0 ) ) e. RR )`
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( 0 x. ( y x. 0 ) ) e. RR )`
36 35 recnd
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( 0 x. ( y x. 0 ) ) e. CC )`
37 remulcl
` |-  ( ( c e. RR /\ ( y x. 0 ) e. RR ) -> ( c x. ( y x. 0 ) ) e. RR )`
38 9 27 37 syl2anc
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( c x. ( y x. 0 ) ) e. RR )`
39 38 recnd
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( c x. ( y x. 0 ) ) e. CC )`
` |-  ( ( ( 0 x. ( y x. 0 ) ) e. CC /\ ( c x. ( y x. 0 ) ) e. CC /\ 0 e. CC ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) + 0 ) = ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) )`
41 13 40 mp3an3
` |-  ( ( ( 0 x. ( y x. 0 ) ) e. CC /\ ( c x. ( y x. 0 ) ) e. CC ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) + 0 ) = ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) )`
42 36 39 41 syl2anc
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( c x. ( y x. 0 ) ) ) + 0 ) = ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) )`
43 32 42 eqtr2d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + 0 ) )`
44 26 37 sylan2
` |-  ( ( c e. RR /\ y e. RR ) -> ( c x. ( y x. 0 ) ) e. RR )`
` |-  ( ( ( c x. ( y x. 0 ) ) e. RR /\ 0 e. RR ) -> ( ( c x. ( y x. 0 ) ) + 0 ) e. RR )`
46 44 1 45 sylancl
` |-  ( ( c e. RR /\ y e. RR ) -> ( ( c x. ( y x. 0 ) ) + 0 ) e. RR )`
47 9 11 46 syl2anc
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( c x. ( y x. 0 ) ) + 0 ) e. RR )`
` |-  ( ( ( ( c x. ( y x. 0 ) ) + 0 ) e. RR /\ 0 e. RR /\ ( 0 x. ( y x. 0 ) ) e. RR ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + 0 ) <-> ( ( c x. ( y x. 0 ) ) + 0 ) = 0 ) )`
49 1 48 mp3an2
` |-  ( ( ( ( c x. ( y x. 0 ) ) + 0 ) e. RR /\ ( 0 x. ( y x. 0 ) ) e. RR ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + 0 ) <-> ( ( c x. ( y x. 0 ) ) + 0 ) = 0 ) )`
50 47 35 49 syl2anc
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( ( 0 x. ( y x. 0 ) ) + ( ( c x. ( y x. 0 ) ) + 0 ) ) = ( ( 0 x. ( y x. 0 ) ) + 0 ) <-> ( ( c x. ( y x. 0 ) ) + 0 ) = 0 ) )`
51 43 50 mpbid
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( ( c x. ( y x. 0 ) ) + 0 ) = 0 )`
52 22 51 eqtr3d
` |-  ( ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) /\ ( y e. RR /\ ( c x. y ) = 1 ) ) -> ( 0 + 0 ) = 0 )`
53 8 52 rexlimddv
` |-  ( ( ( c e. RR /\ ( 0 + c ) = 0 ) /\ c =/= 0 ) -> ( 0 + 0 ) = 0 )`
54 53 expcom
` |-  ( c =/= 0 -> ( ( c e. RR /\ ( 0 + c ) = 0 ) -> ( 0 + 0 ) = 0 ) )`
55 6 54 pm2.61ine
` |-  ( ( c e. RR /\ ( 0 + c ) = 0 ) -> ( 0 + 0 ) = 0 )`
56 55 rexlimiva
` |-  ( E. c e. RR ( 0 + c ) = 0 -> ( 0 + 0 ) = 0 )`
57 1 2 56 mp2b
` |-  ( 0 + 0 ) = 0`