Theorem 00id 11339

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 11166	. 2 ⊢ 0 ∈ ℝ
2		ax-rnegex 11131	. 2 ⊢ (0 ∈ ℝ → ∃𝑐 ∈ ℝ (0 + 𝑐) = 0)
3		oveq2 7370	. . . . . . 7 ⊢ (𝑐 = 0 → (0 + 𝑐) = (0 + 0))
4	3	eqeq1d 2733	. . . . . 6 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 ↔ (0 + 0) = 0))
5	4	biimpd 228	. . . . 5 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 → (0 + 0) = 0))
6	5	adantld 491	. . . 4 ⊢ (𝑐 = 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
7		ax-rrecex 11132	. . . . . . 7 ⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
8	7	adantlr 713	. . . . . 6 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
9		simplll 773	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℝ)
10	9	recnd 11192	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℂ)
11		simprl 769	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℝ)
12	11	recnd 11192	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℂ)
13		0cn 11156	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
14		mulass 11148	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
15	13, 14	mp3an3 1450	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
16	10, 12, 15	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
17		oveq1 7369	. . . . . . . . . . 11 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = (1 · 0))
18	13	mullidi 11169	. . . . . . . . . . 11 ⊢ (1 · 0) = 0
19	17, 18	eqtrdi 2787	. . . . . . . . . 10 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = 0)
20	19	ad2antll 727	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = 0)
21	16, 20	eqtr3d 2773	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) = 0)
22	21	oveq1d 7377	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = (0 + 0))
23		simpllr 774	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 𝑐) = 0)
24	23	oveq1d 7377	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = (0 · (𝑦 · 0)))
25		remulcl 11145	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑦 · 0) ∈ ℝ)
26	1, 25	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 · 0) ∈ ℝ)
27	26	ad2antrl 726	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℝ)
28	27	recnd 11192	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℂ)
29		adddir 11155	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ (𝑦 · 0) ∈ ℂ) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
30	13, 10, 28, 29	mp3an2i 1466	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
31	24, 30	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
32	31	oveq1d 7377	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + 0) = (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0))
33		remulcl 11145	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (0 · (𝑦 · 0)) ∈ ℝ)
34	1, 26, 33	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (0 · (𝑦 · 0)) ∈ ℝ)
35	34	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℝ)
36	35	recnd 11192	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℂ)
37		remulcl 11145	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
38	9, 27, 37	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
39	38	recnd 11192	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℂ)
40		addass 11147	. . . . . . . . . . 11 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ ∧ 0 ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
41	13, 40	mp3an3 1450	. . . . . . . . . 10 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
42	36, 39, 41	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
43	32, 42	eqtr2d 2772	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0))
44	26, 37	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
45		readdcl 11143	. . . . . . . . . . 11 ⊢ (((𝑐 · (𝑦 · 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
46	44, 1, 45	sylancl 586	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
47	9, 11, 46	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
48		readdcan 11338	. . . . . . . . . 10 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ 0 ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
49	1, 48	mp3an2 1449	. . . . . . . . 9 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
50	47, 35, 49	syl2anc 584	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
51	43, 50	mpbid 231	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = 0)
52	22, 51	eqtr3d 2773	. . . . . 6 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 0) = 0)
53	8, 52	rexlimddv 3154	. . . . 5 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → (0 + 0) = 0)
54	53	expcom 414	. . . 4 ⊢ (𝑐 ≠ 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
55	6, 54	pm2.61ine 3024	. . 3 ⊢ ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0)
56	55	rexlimiva 3140	. 2 ⊢ (∃𝑐 ∈ ℝ (0 + 𝑐) = 0 → (0 + 0) = 0)
57	1, 2, 56	mp2b 10	1 ⊢ (0 + 0) = 0

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∃wrex 3069  (class class class)co 7362  ℂcc 11058  ℝcr 11059  0cc0 11060  1c1 11061   + caddc 11063   · cmul 11065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-ltxr 11203

This theorem is referenced by:  mul02lem1  11340  mul02lem2  11341  addrid  11344  addlid  11347  addgt0  11650  addgegt0  11651  addgtge0  11652  addge0  11653  add20  11676  recextlem2  11795  crne0  12155  decaddm10  12686  10p10e20  12722  ser0  13970  faclbnd4lem3  14205  bcpasc  14231  relexpaddg  14950  fsumadd  15636  fsumrelem  15703  arisum  15756  fsumcube  15954  sadcaddlem  16348  sadcadd  16349  sadadd2  16351  bezout  16435  bezoutr1  16456  nnnn0modprm0  16689  pcaddlem  16771  4sqlem19  16846  139prm  17007  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem4  17017  2503lem1  17020  2503lem2  17021  2503lem3  17022  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  sylow1lem1  19394  cnfld0  20858  psrbagaddcl  21367  psrbagaddclOLD  21368  mplcoe3  21476  reparphti  24397  cphpyth  24617  itg1addlem4  25100  itg1addlem4OLD  25101  ibladdlem  25221  itgaddlem1  25224  iblabslem  25229  iblabs  25230  coeaddlem  25647  dcubic  26233  log2ublem3  26335  log2ub  26336  chtublem  26596  logfacrlim  26609  2sqnn  26824  dchrisumlem1  26874  vtxdg0e  28485  1kp2ke3k  29453  dip0r  29722  pythi  29855  normpythi  30147  ocsh  30288  0lnfn  30990  lnopeq0i  31012  nlelshi  31065  unierri  31109  probun  33108  hgt750lem2  33354  poimirlem3  36154  poimirlem4  36155  ismblfin  36192  itg2addnc  36205  ibladdnclem  36207  itgaddnclem1  36209  itgaddnclem2  36210  iblabsnclem  36214  iblabsnc  36215  iblmulc2nc  36216  ftc1anclem8  36231  ftc1anc  36232  3lexlogpow5ineq1  40584  dffltz  41030  relexpaddss  42112  stoweidlem44  44405  fourierdlem42  44510  fourierdlem103  44570  fourierdlem104  44571  sqwvfoura  44589  sqwvfourb  44590  fmtno5lem4  45868  139prmALT  45908  line2ylem  46957