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
2 ax-rnegex 0 c 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 0 + c = 0 0 + 0 = 0
7 ax-rrecex c c 0 y c y = 1
8 7 adantlr c 0 + c = 0 c 0 y c y = 1
9 simplll c 0 + c = 0 c 0 y c y = 1 c
10 9 recnd c 0 + c = 0 c 0 y c y = 1 c
11 simprl c 0 + c = 0 c 0 y c y = 1 y
12 11 recnd c 0 + c = 0 c 0 y c y = 1 y
13 0cn 0
14 mulass c y 0 c y 0 = c y 0
15 13 14 mp3an3 c y c y 0 = c y 0
16 10 12 15 syl2anc c 0 + c = 0 c 0 y c y = 1 c y 0 = c y 0
17 oveq1 c y = 1 c y 0 = 1 0
18 13 mulid2i 1 0 = 0
19 17 18 eqtrdi c y = 1 c y 0 = 0
20 19 ad2antll c 0 + c = 0 c 0 y c y = 1 c y 0 = 0
21 16 20 eqtr3d c 0 + c = 0 c 0 y c y = 1 c y 0 = 0
22 21 oveq1d c 0 + c = 0 c 0 y c y = 1 c y 0 + 0 = 0 + 0
23 simpllr c 0 + c = 0 c 0 y c y = 1 0 + c = 0
24 23 oveq1d c 0 + c = 0 c 0 y c y = 1 0 + c y 0 = 0 y 0
25 remulcl y 0 y 0
26 1 25 mpan2 y y 0
27 26 ad2antrl c 0 + c = 0 c 0 y c y = 1 y 0
28 27 recnd c 0 + c = 0 c 0 y c y = 1 y 0
29 adddir 0 c y 0 0 + c y 0 = 0 y 0 + c y 0
30 13 10 28 29 mp3an2i c 0 + c = 0 c 0 y c y = 1 0 + c y 0 = 0 y 0 + c y 0
31 24 30 eqtr3d c 0 + c = 0 c 0 y c y = 1 0 y 0 = 0 y 0 + c y 0
32 31 oveq1d c 0 + c = 0 c 0 y c y = 1 0 y 0 + 0 = 0 y 0 + c y 0 + 0
33 remulcl 0 y 0 0 y 0
34 1 26 33 sylancr y 0 y 0
35 34 ad2antrl c 0 + c = 0 c 0 y c y = 1 0 y 0
36 35 recnd c 0 + c = 0 c 0 y c y = 1 0 y 0
37 remulcl c y 0 c y 0
38 9 27 37 syl2anc c 0 + c = 0 c 0 y c y = 1 c y 0
39 38 recnd c 0 + c = 0 c 0 y c y = 1 c y 0
40 addass 0 y 0 c y 0 0 0 y 0 + c y 0 + 0 = 0 y 0 + c y 0 + 0
41 13 40 mp3an3 0 y 0 c y 0 0 y 0 + c y 0 + 0 = 0 y 0 + c y 0 + 0
42 36 39 41 syl2anc c 0 + c = 0 c 0 y c y = 1 0 y 0 + c y 0 + 0 = 0 y 0 + c y 0 + 0
43 32 42 eqtr2d c 0 + c = 0 c 0 y c y = 1 0 y 0 + c y 0 + 0 = 0 y 0 + 0
44 26 37 sylan2 c y c y 0
45 readdcl c y 0 0 c y 0 + 0
46 44 1 45 sylancl c y c y 0 + 0
47 9 11 46 syl2anc c 0 + c = 0 c 0 y c y = 1 c y 0 + 0
48 readdcan c y 0 + 0 0 0 y 0 0 y 0 + c y 0 + 0 = 0 y 0 + 0 c y 0 + 0 = 0
49 1 48 mp3an2 c y 0 + 0 0 y 0 0 y 0 + c y 0 + 0 = 0 y 0 + 0 c y 0 + 0 = 0
50 47 35 49 syl2anc c 0 + c = 0 c 0 y c y = 1 0 y 0 + c y 0 + 0 = 0 y 0 + 0 c y 0 + 0 = 0
51 43 50 mpbid c 0 + c = 0 c 0 y c y = 1 c y 0 + 0 = 0
52 22 51 eqtr3d c 0 + c = 0 c 0 y c y = 1 0 + 0 = 0
53 8 52 rexlimddv c 0 + c = 0 c 0 0 + 0 = 0
54 53 expcom c 0 c 0 + c = 0 0 + 0 = 0
55 6 54 pm2.61ine c 0 + c = 0 0 + 0 = 0
56 55 rexlimiva c 0 + c = 0 0 + 0 = 0
57 1 2 56 mp2b 0 + 0 = 0