Theorem 00id 11386

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 11211	. 2 ⊢ 0 ∈ ℝ
2		ax-rnegex 11172	. 2 ⊢ (0 ∈ ℝ → ∃𝑐 ∈ ℝ (0 + 𝑐) = 0)
3		oveq2 7420	. . . . . . 7 ⊢ (𝑐 = 0 → (0 + 𝑐) = (0 + 0))
4	3	eqeq1d 2765	. . . . . 6 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 ↔ (0 + 0) = 0))
5	4	biimpd 232	. . . . 5 ⊢ (𝑐 = 0 → ((0 + 𝑐) = 0 → (0 + 0) = 0))
6	5	adantld 495	. . . 4 ⊢ (𝑐 = 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
7		ax-rrecex 11173	. . . . . . 7 ⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
8	7	adantlr 727	. . . . . 6 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → ∃𝑦 ∈ ℝ (𝑐 · 𝑦) = 1)
9		simplll 786	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℝ)
10	9	recnd 11238	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑐 ∈ ℂ)
11		simprl 782	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℝ)
12	11	recnd 11238	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → 𝑦 ∈ ℂ)
13		0cn 11199	. . . . . . . . . . 11 ⊢ 0 ∈ ℂ
14		mulass 11189	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
15	13, 14	mp3an3 1479	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
16	10, 12, 15	syl2anc 595	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = (𝑐 · (𝑦 · 0)))
17		oveq1 7419	. . . . . . . . . . 11 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = (1 · 0))
18	13	mullidi 11215	. . . . . . . . . . 11 ⊢ (1 · 0) = 0
19	17, 18	eqtrdi 2814	. . . . . . . . . 10 ⊢ ((𝑐 · 𝑦) = 1 → ((𝑐 · 𝑦) · 0) = 0)
20	19	ad2antll 741	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · 𝑦) · 0) = 0)
21	16, 20	eqtr3d 2800	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) = 0)
22	21	oveq1d 7427	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = (0 + 0))
23		simpllr 787	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 𝑐) = 0)
24	23	oveq1d 7427	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = (0 · (𝑦 · 0)))
25		remulcl 11186	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → (𝑦 · 0) ∈ ℝ)
26	1, 25	mpan2 703	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (𝑦 · 0) ∈ ℝ)
27	26	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℝ)
28	27	recnd 11238	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑦 · 0) ∈ ℂ)
29		adddir 11198	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ (𝑦 · 0) ∈ ℂ) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
30	13, 10, 28, 29	mp3an2i 1495	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 + 𝑐) · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
31	24, 30	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) = ((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))))
32	31	oveq1d 7427	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + 0) = (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0))
33		remulcl 11186	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (0 · (𝑦 · 0)) ∈ ℝ)
34	1, 26, 33	sylancr 598	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (0 · (𝑦 · 0)) ∈ ℝ)
35	34	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℝ)
36	35	recnd 11238	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 · (𝑦 · 0)) ∈ ℂ)
37		remulcl 11186	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ ℝ ∧ (𝑦 · 0) ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
38	9, 27, 37	syl2anc 595	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
39	38	recnd 11238	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (𝑐 · (𝑦 · 0)) ∈ ℂ)
40		addass 11188	. . . . . . . . . . 11 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ ∧ 0 ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
41	13, 40	mp3an3 1479	. . . . . . . . . 10 ⊢ (((0 · (𝑦 · 0)) ∈ ℂ ∧ (𝑐 · (𝑦 · 0)) ∈ ℂ) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
42	36, 39, 41	syl2anc 595	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + (𝑐 · (𝑦 · 0))) + 0) = ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)))
43	32, 42	eqtr2d 2799	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0))
44	26, 37	sylan2 604	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑐 · (𝑦 · 0)) ∈ ℝ)
45		readdcl 11184	. . . . . . . . . . 11 ⊢ (((𝑐 · (𝑦 · 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
46	44, 1, 45	sylancl 597	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
47	9, 11, 46	syl2anc 595	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ)
48		readdcan 11385	. . . . . . . . . 10 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ 0 ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
49	1, 48	mp3an2 1478	. . . . . . . . 9 ⊢ ((((𝑐 · (𝑦 · 0)) + 0) ∈ ℝ ∧ (0 · (𝑦 · 0)) ∈ ℝ) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
50	47, 35, 49	syl2anc 595	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (((0 · (𝑦 · 0)) + ((𝑐 · (𝑦 · 0)) + 0)) = ((0 · (𝑦 · 0)) + 0) ↔ ((𝑐 · (𝑦 · 0)) + 0) = 0))
51	43, 50	mpbid 235	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → ((𝑐 · (𝑦 · 0)) + 0) = 0)
52	22, 51	eqtr3d 2800	. . . . . 6 ⊢ ((((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) ∧ (𝑦 ∈ ℝ ∧ (𝑐 · 𝑦) = 1)) → (0 + 0) = 0)
53	8, 52	rexlimddv 3172	. . . . 5 ⊢ (((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) ∧ 𝑐 ≠ 0) → (0 + 0) = 0)
54	53	expcom 418	. . . 4 ⊢ (𝑐 ≠ 0 → ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0))
55	6, 54	pm2.61ine 3041	. . 3 ⊢ ((𝑐 ∈ ℝ ∧ (0 + 𝑐) = 0) → (0 + 0) = 0)
56	55	rexlimiva 3158	. 2 ⊢ (∃𝑐 ∈ ℝ (0 + 𝑐) = 0 → (0 + 0) = 0)
57	1, 2, 56	mp2b 10	1 ⊢ (0 + 0) = 0

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3089  (class class class)co 7412  ℂcc 11099  ℝcr 11100  0cc0 11101  1c1 11102   + caddc 11104   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  mul02lem1  11387  mul02lem2  11388  addrid  11391  addlid  11394  addgt0  11701  addgegt0  11702  addgtge0  11703  addge0  11704  add20  11727  recextlem2  11846  crne0  12212  decaddm10  12776  10p10e20  12812  ser0  14092  faclbnd4lem3  14333  bcpasc  14359  relexpaddg  15092  fsumadd  15793  fsumrelem  15861  arisum  15916  fsumcube  16115  sadcaddlem  16516  sadcadd  16517  sadadd2  16519  bezout  16602  bezoutr1  16628  nnnn0modprm0  16867  pcaddlem  16949  4sqlem19  17024  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem4  17195  2503lem1  17198  2503lem2  17199  2503lem3  17200  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  sylow1lem1  19669  cnfld0  21527  pzriprnglem4  21615  psrbagaddcl  22055  mplcoe3  22170  reparphti  25137  cphpyth  25356  itg1addlem4  25839  ibladdlem  25960  itgaddlem1  25963  iblabslem  25968  iblabs  25969  coeaddlem  26387  dcubic  26989  log2ublem3  27091  log2ub  27092  chtublem  27353  logfacrlim  27366  2sqnn  27581  dchrisumlem1  27631  vtxdg0e  29802  1kp2ke3k  30775  dip0r  31047  pythi  31180  normpythi  31472  ocsh  31613  0lnfn  32315  lnopeq0i  32337  nlelshi  32390  unierri  32434  cos9thpiminply  34156  probun  34787  hgt750lem2  35017  poimirlem3  38252  poimirlem4  38253  ismblfin  38290  itg2addnc  38303  ibladdnclem  38305  itgaddnclem1  38307  itgaddnclem2  38308  iblabsnclem  38312  iblabsnc  38313  iblmulc2nc  38314  ftc1anclem8  38329  ftc1anc  38330  3lexlogpow5ineq1  42799  dffltz  43346  relexpaddss  44424  stoweidlem44  46738  fourierdlem42  46843  fourierdlem103  46903  fourierdlem104  46904  sqwvfoura  46922  sqwvfourb  46923  fmtno5lem4  48285  139prmALT  48325  line2ylem  49508