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