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 ) )
6 5 adantld
 |-  ( 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 )
8 7 adantlr
 |-  ( ( ( 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 )
20 19 ad2antll
 |-  ( ( ( ( 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 )
27 26 ad2antrl
 |-  ( ( ( ( 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 )
29 adddir
 |-  ( ( 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 )
35 34 ad2antrl
 |-  ( ( ( ( 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 )
40 addass
 |-  ( ( ( 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 )
45 readdcl
 |-  ( ( ( 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 )
48 readdcan
 |-  ( ( ( ( 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