# Metamath Proof Explorer

Description: 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion addid1 ${⊢}{A}\in ℂ\to {A}+0={A}$

### Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 ax-rnegex ${⊢}1\in ℝ\to \exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}1+{c}=0$
3 ax-1ne0 ${⊢}1\ne 0$
4 oveq2 ${⊢}{c}=0\to 1+{c}=1+0$
5 4 eqeq1d ${⊢}{c}=0\to \left(1+{c}=0↔1+0=0\right)$
6 5 biimpcd ${⊢}1+{c}=0\to \left({c}=0\to 1+0=0\right)$
7 oveq2 ${⊢}1+0=0\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\left(1+0\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0$
8 ax-icn ${⊢}\mathrm{i}\in ℂ$
9 8 8 mulcli ${⊢}\mathrm{i}\mathrm{i}\in ℂ$
10 9 9 mulcli ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\in ℂ$
11 ax-1cn ${⊢}1\in ℂ$
12 0cn ${⊢}0\in ℂ$
13 10 11 12 adddii ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\left(1+0\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 1+\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0$
14 10 mulid1i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 1=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$
15 mul01 ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\in ℂ\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0=0$
16 10 15 ax-mp ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0=0$
17 ax-i2m1 ${⊢}\mathrm{i}\mathrm{i}+1=0$
18 16 17 eqtr4i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0=\mathrm{i}\mathrm{i}+1$
19 14 18 oveq12i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 1+\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1$
20 13 19 eqtri ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\left(1+0\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1$
21 20 16 eqeq12i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\left(1+0\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0↔\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1=0$
22 10 9 11 addassi ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1$
23 9 mulid1i ${⊢}\mathrm{i}\mathrm{i}\cdot 1=\mathrm{i}\mathrm{i}$
24 23 oveq2i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}\cdot 1=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}$
25 9 9 11 adddii ${⊢}\mathrm{i}\mathrm{i}\left(\mathrm{i}\mathrm{i}+1\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}\cdot 1$
26 17 oveq2i ${⊢}\mathrm{i}\mathrm{i}\left(\mathrm{i}\mathrm{i}+1\right)=\mathrm{i}\mathrm{i}\cdot 0$
27 mul01 ${⊢}\mathrm{i}\mathrm{i}\in ℂ\to \mathrm{i}\mathrm{i}\cdot 0=0$
28 9 27 ax-mp ${⊢}\mathrm{i}\mathrm{i}\cdot 0=0$
29 26 28 eqtri ${⊢}\mathrm{i}\mathrm{i}\left(\mathrm{i}\mathrm{i}+1\right)=0$
30 25 29 eqtr3i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}\cdot 1=0$
31 24 30 eqtr3i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}=0$
32 31 oveq1i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1=0+1$
33 22 32 eqtr3i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1=0+1$
34 00id ${⊢}0+0=0$
35 34 eqcomi ${⊢}0=0+0$
36 33 35 eqeq12i ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}+\mathrm{i}\mathrm{i}+1=0↔0+1=0+0$
37 0re ${⊢}0\in ℝ$
38 readdcan ${⊢}\left(1\in ℝ\wedge 0\in ℝ\wedge 0\in ℝ\right)\to \left(0+1=0+0↔1=0\right)$
39 1 37 37 38 mp3an ${⊢}0+1=0+0↔1=0$
40 21 36 39 3bitri ${⊢}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\left(1+0\right)=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\cdot 0↔1=0$
41 7 40 sylib ${⊢}1+0=0\to 1=0$
42 6 41 syl6 ${⊢}1+{c}=0\to \left({c}=0\to 1=0\right)$
43 42 necon3d ${⊢}1+{c}=0\to \left(1\ne 0\to {c}\ne 0\right)$
44 3 43 mpi ${⊢}1+{c}=0\to {c}\ne 0$
45 ax-rrecex ${⊢}\left({c}\in ℝ\wedge {c}\ne 0\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{c}{x}=1$
46 44 45 sylan2 ${⊢}\left({c}\in ℝ\wedge 1+{c}=0\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{c}{x}=1$
47 simpr ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}\in ℂ$
48 simplrl ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {x}\in ℝ$
49 48 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {x}\in ℂ$
50 47 49 mulcld ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}\in ℂ$
51 simplll ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}\in ℝ$
52 51 recnd ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}\in ℂ$
53 12 a1i ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 0\in ℂ$
54 50 52 53 adddid ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}\left({c}+0\right)={A}{x}{c}+{A}{x}\cdot 0$
55 11 a1i ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1\in ℂ$
56 55 52 53 addassd ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1+{c}+0=1+{c}+0$
57 simpllr ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1+{c}=0$
58 57 oveq1d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1+{c}+0=0+0$
59 56 58 eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1+{c}+0=0+0$
60 34 59 57 3eqtr4a ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1+{c}+0=1+{c}$
61 37 a1i ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 0\in ℝ$
62 51 61 readdcld ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}+0\in ℝ$
63 1 a1i ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1\in ℝ$
64 readdcan ${⊢}\left({c}+0\in ℝ\wedge {c}\in ℝ\wedge 1\in ℝ\right)\to \left(1+{c}+0=1+{c}↔{c}+0={c}\right)$
65 62 51 63 64 syl3anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to \left(1+{c}+0=1+{c}↔{c}+0={c}\right)$
66 60 65 mpbid ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}+0={c}$
67 66 oveq2d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}\left({c}+0\right)={A}{x}{c}$
68 54 67 eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}{c}+{A}{x}\cdot 0={A}{x}{c}$
69 mul31 ${⊢}\left({A}\in ℂ\wedge {x}\in ℂ\wedge {c}\in ℂ\right)\to {A}{x}{c}={c}{x}{A}$
70 47 49 52 69 syl3anc ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}{c}={c}{x}{A}$
71 simplrr ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}{x}=1$
72 71 oveq1d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {c}{x}{A}=1{A}$
73 47 mulid2d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to 1{A}={A}$
74 70 72 73 3eqtrd ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}{c}={A}$
75 mul01 ${⊢}{A}{x}\in ℂ\to {A}{x}\cdot 0=0$
76 50 75 syl ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}\cdot 0=0$
77 74 76 oveq12d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}{x}{c}+{A}{x}\cdot 0={A}+0$
78 68 77 74 3eqtr3d ${⊢}\left(\left(\left({c}\in ℝ\wedge 1+{c}=0\right)\wedge \left({x}\in ℝ\wedge {c}{x}=1\right)\right)\wedge {A}\in ℂ\right)\to {A}+0={A}$
79 78 exp42 ${⊢}\left({c}\in ℝ\wedge 1+{c}=0\right)\to \left({x}\in ℝ\to \left({c}{x}=1\to \left({A}\in ℂ\to {A}+0={A}\right)\right)\right)$
80 79 rexlimdv ${⊢}\left({c}\in ℝ\wedge 1+{c}=0\right)\to \left(\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{c}{x}=1\to \left({A}\in ℂ\to {A}+0={A}\right)\right)$
81 46 80 mpd ${⊢}\left({c}\in ℝ\wedge 1+{c}=0\right)\to \left({A}\in ℂ\to {A}+0={A}\right)$
82 81 rexlimiva ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}1+{c}=0\to \left({A}\in ℂ\to {A}+0={A}\right)$
83 1 2 82 mp2b ${⊢}{A}\in ℂ\to {A}+0={A}$