Theorem addid2 11231

Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
addid2	⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnegex 11229	. 2 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)
2		cnegex 11229	. . . 4 ⊢ (𝑥 ∈ ℂ → ∃𝑦 ∈ ℂ (𝑥 + 𝑦) = 0)
3	2	ad2antrl 725	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → ∃𝑦 ∈ ℂ (𝑥 + 𝑦) = 0)
4		0cn 11040	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
5		addass 11031	. . . . . . . . . 10 ⊢ ((0 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦)))
6	4, 4, 5	mp3an12 1450	. . . . . . . . 9 ⊢ (𝑦 ∈ ℂ → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦)))
7	6	adantr 481	. . . . . . . 8 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦)))
8	7	3ad2ant3 1134	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦)))
9		00id 11223	. . . . . . . . 9 ⊢ (0 + 0) = 0
10	9	oveq1i 7325	. . . . . . . 8 ⊢ ((0 + 0) + 𝑦) = (0 + 𝑦)
11		simp1 1135	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝐴 ∈ ℂ)
12		simp2l 1198	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝑥 ∈ ℂ)
13		simp3l 1200	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝑦 ∈ ℂ)
14	11, 12, 13	addassd 11070	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((𝐴 + 𝑥) + 𝑦) = (𝐴 + (𝑥 + 𝑦)))
15		simp2r 1199	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 𝑥) = 0)
16	15	oveq1d 7330	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((𝐴 + 𝑥) + 𝑦) = (0 + 𝑦))
17		simp3r 1201	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝑥 + 𝑦) = 0)
18	17	oveq2d 7331	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + (𝑥 + 𝑦)) = (𝐴 + 0))
19	14, 16, 18	3eqtr3rd 2786	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 0) = (0 + 𝑦))
20		addid1 11228	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
21	20	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 0) = 𝐴)
22	19, 21	eqtr3d 2779	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + 𝑦) = 𝐴)
23	10, 22	eqtrid 2789	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((0 + 0) + 𝑦) = 𝐴)
24	22	oveq2d 7331	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + (0 + 𝑦)) = (0 + 𝐴))
25	8, 23, 24	3eqtr3rd 2786	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + 𝐴) = 𝐴)
26	25	3expia 1120	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → ((𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0) → (0 + 𝐴) = 𝐴))
27	26	expd 416	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (𝑦 ∈ ℂ → ((𝑥 + 𝑦) = 0 → (0 + 𝐴) = 𝐴)))
28	27	rexlimdv 3147	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (∃𝑦 ∈ ℂ (𝑥 + 𝑦) = 0 → (0 + 𝐴) = 𝐴))
29	3, 28	mpd 15	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (0 + 𝐴) = 𝐴)
30	1, 29	rexlimddv 3155	1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ∃wrex 3071  (class class class)co 7315  ℂcc 10942  0cc0 10944   + caddc 10947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-po 5521  df-so 5522  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7318  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-ltxr 11087

This theorem is referenced by:  addcan  11232  addid2i  11236  addid2d  11249  negneg  11344  fz0to4untppr  13432  fzo0addel  13514  fzoaddel2  13516  divfl0  13617  modid  13689  modsumfzodifsn  13737  swrdspsleq  14450  swrds1  14451  isercolllem3  15450  sumrblem  15495  summolem2a  15499  fsum0diag2  15567  eftlub  15890  gcdid  16306  cnaddablx  19537  cnaddabl  19538  cnaddid  19539  cncrng  20691  cnlmod  24375  ptolemy  25725  logtayl  25887  leibpilem2  26163  axcontlem2  27442  cnaddabloOLD  29052  cnidOLD  29053  dvcosax  43704  2zrngamnd  45751  aacllem  46757