Theorem 00id 10809

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
00id	⊢ (0 + 0) = 0

Proof of Theorem 00id

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

Step	Hyp	Ref	Expression
1		0re 10637	. 2 ⊢ 0 ∈ ℝ
2		ax-rnegex 10602	. 2 ⊢ (0 ∈ ℝ → ∃𝑐 ∈ ℝ (0 + 𝑐) = 0)
3		oveq2 7158	. . . . . . 7 ⊢ (𝑐 = 0 → (0 + 𝑐) = (0 + 0))
4	3	eqeq1d 2823	. . . . . 6 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 ↔ (0 + 0) = 0))
5	4	biimpd 231	. . . . 5 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 → (0 + 0) = 0))
6	5	adantld 493	. . . 4 ⊢ (𝑐 = 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
7		ax-rrecex 10603	. . . . . . 7 ⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
8	7	adantlr 713	. . . . . 6 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
9		simplll 773	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℝ)
10	9	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℂ)
11		simprl 769	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℝ)
12	11	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℂ)
13		0cn 10627	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
14		mulass 10619	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
15	13, 14	mp3an3 1446	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
16	10, 12, 15	syl2anc 586	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
17		oveq1 7157	. . . . . . . . . . 11 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = (1 · 0))
18	13	mulid2i 10640	. . . . . . . . . . 11 ⊢ (1 · 0) = 0
19	17, 18	syl6eq 2872	. . . . . . . . . 10 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = 0)
20	19	ad2antll 727	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = 0)
21	16, 20	eqtr3d 2858	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) = 0)
22	21	oveq1d 7165	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = (0 + 0))
23		simpllr 774	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 𝑐) = 0)
24	23	oveq1d 7165	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = (0 · (𝑦 · 0)))
25		remulcl 10616	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑦 · 0) ∈ ℝ)
26	1, 25	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 · 0) ∈ ℝ)
27	26	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℝ)
28	27	recnd 10663	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℂ)
29		adddir 10626	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ (𝑦 · 0) ∈ ℂ) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
30	13, 10, 28, 29	mp3an2i 1462	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
31	24, 30	eqtr3d 2858	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
32	31	oveq1d 7165	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + 0) = (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0))
33		remulcl 10616	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (0 · (𝑦 · 0)) ∈ ℝ)
34	1, 26, 33	sylancr 589	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (0 · (𝑦 · 0)) ∈ ℝ)
35	34	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℝ)
36	35	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℂ)
37		remulcl 10616	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
38	9, 27, 37	syl2anc 586	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
39	38	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℂ)
40		addass 10618	. . . . . . . . . . 11 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ ∧ 0 ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
41	13, 40	mp3an3 1446	. . . . . . . . . 10 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
42	36, 39, 41	syl2anc 586	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
43	32, 42	eqtr2d 2857	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0))
44	26, 37	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
45		readdcl 10614	. . . . . . . . . . 11 ⊢ (((𝑐 · (𝑦 · 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
46	44, 1, 45	sylancl 588	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
47	9, 11, 46	syl2anc 586	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
48		readdcan 10808	. . . . . . . . . 10 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ 0 ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
49	1, 48	mp3an2 1445	. . . . . . . . 9 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
50	47, 35, 49	syl2anc 586	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
51	43, 50	mpbid 234	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = 0)
52	22, 51	eqtr3d 2858	. . . . . 6 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 0) = 0)
53	8, 52	rexlimddv 3291	. . . . 5 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → (0 + 0) = 0)
54	53	expcom 416	. . . 4 ⊢ (𝑐 ≠ 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
55	6, 54	pm2.61ine 3100	. . 3 ⊢ ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0)
56	55	rexlimiva 3281	. 2 ⊢ (∃𝑐 ∈ ℝ (0 + 𝑐) = 0 → (0 + 0) = 0)
57	1, 2, 56	mp2b 10	1 ⊢ (0 + 0) = 0

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∃wrex 3139  (class class class)co 7150  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-ltxr 10674

This theorem is referenced by:  mul02lem1  10810  mul02lem2  10811  addid1  10814  addid2  10817  addgt0  11120  addgegt0  11121  addgtge0  11122  addge0  11123  add20  11146  recextlem2  11265  crne0  11625  decaddm10  12151  10p10e20  12187  ser0  13416  faclbnd4lem3  13649  bcpasc  13675  relexpaddg  14406  fsumadd  15090  fsumrelem  15156  arisum  15209  fsumcube  15408  sadcaddlem  15800  sadcadd  15801  sadadd2  15803  bezout  15885  bezoutr1  15907  nnnn0modprm0  16137  pcaddlem  16218  4sqlem19  16293  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem4  16461  2503lem1  16464  2503lem2  16465  2503lem3  16466  4001lem1  16468  4001lem2  16469  4001lem3  16470  4001lem4  16471  sylow1lem1  18717  psrbagaddcl  20144  mplcoe3  20241  cnfld0  20563  reparphti  23595  itg1addlem4  24294  ibladdlem  24414  itgaddlem1  24417  iblabslem  24422  iblabs  24423  coeaddlem  24833  dcubic  25418  log2ublem3  25520  log2ub  25521  chtublem  25781  logfacrlim  25794  2sqnn  26009  dchrisumlem1  26059  vtxdg0e  27250  1kp2ke3k  28219  dip0r  28488  pythi  28621  normpythi  28913  ocsh  29054  0lnfn  29756  lnopeq0i  29778  nlelshi  29831  unierri  29875  probun  31672  hgt750lem2  31918  poimirlem3  34889  poimirlem4  34890  ismblfin  34927  itg2addnc  34940  ibladdnclem  34942  itgaddnclem1  34944  itgaddnclem2  34945  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  ftc1anclem8  34968  ftc1anc  34969  dffltz  39264  relexpaddss  40056  stoweidlem44  42323  fourierdlem42  42428  fourierdlem103  42488  fourierdlem104  42489  sqwvfoura  42507  sqwvfourb  42508  fmtno5lem4  43712  139prmALT  43753  line2ylem  44732