# 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\in ℝ$
2 ax-rnegex ${⊢}0\in ℝ\to \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}0+{c}=0$
3 oveq2 ${⊢}{c}=0\to 0+{c}=0+0$
4 3 eqeq1d ${⊢}{c}=0\to \left(0+{c}=0↔0+0=0\right)$
5 4 biimpd ${⊢}{c}=0\to \left(0+{c}=0\to 0+0=0\right)$
6 5 adantld ${⊢}{c}=0\to \left(\left({c}\in ℝ\wedge 0+{c}=0\right)\to 0+0=0\right)$
7 ax-rrecex ${⊢}\left({c}\in ℝ\wedge {c}\ne 0\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{c}{y}=1$
8 7 adantlr ${⊢}\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{c}{y}=1$
9 simplll ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}\in ℝ$
10 9 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}\in ℂ$
11 simprl ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {y}\in ℝ$
12 11 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {y}\in ℂ$
13 0cn ${⊢}0\in ℂ$
14 mulass ${⊢}\left({c}\in ℂ\wedge {y}\in ℂ\wedge 0\in ℂ\right)\to {c}{y}\cdot 0={c}{y}\cdot 0$
15 13 14 mp3an3 ${⊢}\left({c}\in ℂ\wedge {y}\in ℂ\right)\to {c}{y}\cdot 0={c}{y}\cdot 0$
16 10 12 15 syl2anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0={c}{y}\cdot 0$
17 oveq1 ${⊢}{c}{y}=1\to {c}{y}\cdot 0=1\cdot 0$
18 13 mulid2i ${⊢}1\cdot 0=0$
19 17 18 syl6eq ${⊢}{c}{y}=1\to {c}{y}\cdot 0=0$
20 19 ad2antll ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0=0$
21 16 20 eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0=0$
22 21 oveq1d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0+0=0+0$
23 simpllr ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0+{c}=0$
24 23 oveq1d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to \left(0+{c}\right){y}\cdot 0=0\cdot {y}\cdot 0$
25 remulcl ${⊢}\left({y}\in ℝ\wedge 0\in ℝ\right)\to {y}\cdot 0\in ℝ$
26 1 25 mpan2 ${⊢}{y}\in ℝ\to {y}\cdot 0\in ℝ$
27 26 ad2antrl ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {y}\cdot 0\in ℝ$
28 27 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {y}\cdot 0\in ℂ$
29 adddir ${⊢}\left(0\in ℂ\wedge {c}\in ℂ\wedge {y}\cdot 0\in ℂ\right)\to \left(0+{c}\right){y}\cdot 0=0\cdot {y}\cdot 0+{c}{y}\cdot 0$
30 13 10 28 29 mp3an2i ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to \left(0+{c}\right){y}\cdot 0=0\cdot {y}\cdot 0+{c}{y}\cdot 0$
31 24 30 eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0=0\cdot {y}\cdot 0+{c}{y}\cdot 0$
32 31 oveq1d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0+0=0\cdot {y}\cdot 0+{c}{y}\cdot 0+0$
33 remulcl ${⊢}\left(0\in ℝ\wedge {y}\cdot 0\in ℝ\right)\to 0\cdot {y}\cdot 0\in ℝ$
34 1 26 33 sylancr ${⊢}{y}\in ℝ\to 0\cdot {y}\cdot 0\in ℝ$
35 34 ad2antrl ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0\in ℝ$
36 35 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0\in ℂ$
37 remulcl ${⊢}\left({c}\in ℝ\wedge {y}\cdot 0\in ℝ\right)\to {c}{y}\cdot 0\in ℝ$
38 9 27 37 syl2anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0\in ℝ$
39 38 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0\in ℂ$
40 addass ${⊢}\left(0\cdot {y}\cdot 0\in ℂ\wedge {c}{y}\cdot 0\in ℂ\wedge 0\in ℂ\right)\to 0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+{c}{y}\cdot 0+0$
41 13 40 mp3an3 ${⊢}\left(0\cdot {y}\cdot 0\in ℂ\wedge {c}{y}\cdot 0\in ℂ\right)\to 0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+{c}{y}\cdot 0+0$
42 36 39 41 syl2anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+{c}{y}\cdot 0+0$
43 32 42 eqtr2d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+0$
44 26 37 sylan2 ${⊢}\left({c}\in ℝ\wedge {y}\in ℝ\right)\to {c}{y}\cdot 0\in ℝ$
45 readdcl ${⊢}\left({c}{y}\cdot 0\in ℝ\wedge 0\in ℝ\right)\to {c}{y}\cdot 0+0\in ℝ$
46 44 1 45 sylancl ${⊢}\left({c}\in ℝ\wedge {y}\in ℝ\right)\to {c}{y}\cdot 0+0\in ℝ$
47 9 11 46 syl2anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0+0\in ℝ$
48 readdcan ${⊢}\left({c}{y}\cdot 0+0\in ℝ\wedge 0\in ℝ\wedge 0\cdot {y}\cdot 0\in ℝ\right)\to \left(0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+0↔{c}{y}\cdot 0+0=0\right)$
49 1 48 mp3an2 ${⊢}\left({c}{y}\cdot 0+0\in ℝ\wedge 0\cdot {y}\cdot 0\in ℝ\right)\to \left(0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+0↔{c}{y}\cdot 0+0=0\right)$
50 47 35 49 syl2anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to \left(0\cdot {y}\cdot 0+{c}{y}\cdot 0+0=0\cdot {y}\cdot 0+0↔{c}{y}\cdot 0+0=0\right)$
51 43 50 mpbid ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to {c}{y}\cdot 0+0=0$
52 22 51 eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\wedge \left({y}\in ℝ\wedge {c}{y}=1\right)\right)\to 0+0=0$
53 8 52 rexlimddv ${⊢}\left(\left({c}\in ℝ\wedge 0+{c}=0\right)\wedge {c}\ne 0\right)\to 0+0=0$
54 53 expcom ${⊢}{c}\ne 0\to \left(\left({c}\in ℝ\wedge 0+{c}=0\right)\to 0+0=0\right)$
55 6 54 pm2.61ine ${⊢}\left({c}\in ℝ\wedge 0+{c}=0\right)\to 0+0=0$
56 55 rexlimiva ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}0+{c}=0\to 0+0=0$
57 1 2 56 mp2b ${⊢}0+0=0$