00id

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

		Ref	Expression
	Assertion	00id	$⊢ 0 + 0 = 0$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		ax-rnegex	$⊢ 0 \in ℝ \to \exists c \in ℝ 0 + c = 0$
3		oveq2	$⊢ c = 0 \to 0 + c = 0 + 0$
4	3	eqeq1d	$⊢ c = 0 \to (0 + c = 0 \leftrightarrow 0 + 0 = 0)$
5	4	biimpd	$⊢ c = 0 \to (0 + c = 0 \to 0 + 0 = 0)$
6	5	adantld	$⊢ c = 0 \to ((c \in ℝ \land 0 + c = 0) \to 0 + 0 = 0)$
7		ax-rrecex	$⊢ (c \in ℝ \land c \neq 0) \to \exists y \in ℝ c y = 1$
8	7	adantlr	$⊢ ((c \in ℝ \land 0 + c = 0) \land c \neq 0) \to \exists y \in ℝ c y = 1$
9		simplll	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c \in ℝ$
10	9	recnd	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c \in ℂ$
11		simprl	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to y \in ℝ$
12	11	recnd	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to y \in ℂ$
13		0cn	$⊢ 0 \in ℂ$
14		mulass	$⊢ (c \in ℂ \land y \in ℂ \land 0 \in ℂ) \to c y \cdot 0 = c y \cdot 0$
15	13 14	mp3an3	$⊢ (c \in ℂ \land y \in ℂ) \to c y \cdot 0 = c y \cdot 0$
16	10 12 15	syl2anc	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 = c y \cdot 0$
17		oveq1	$⊢ c y = 1 \to c y \cdot 0 = 1 \cdot 0$
18	13	mulid2i	$⊢ 1 \cdot 0 = 0$
19	17 18	eqtrdi	$⊢ c y = 1 \to c y \cdot 0 = 0$
20	19	ad2antll	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 = 0$
21	16 20	eqtr3d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 = 0$
22	21	oveq1d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 + 0 = 0 + 0$
23		simpllr	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 + c = 0$
24	23	oveq1d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to (0 + c) y \cdot 0 = 0 \cdot y \cdot 0$
25		remulcl	$⊢ (y \in ℝ \land 0 \in ℝ) \to y \cdot 0 \in ℝ$
26	1 25	mpan2	$⊢ y \in ℝ \to y \cdot 0 \in ℝ$
27	26	ad2antrl	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to y \cdot 0 \in ℝ$
28	27	recnd	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to y \cdot 0 \in ℂ$
29		adddir	$⊢ (0 \in ℂ \land c \in ℂ \land y \cdot 0 \in ℂ) \to (0 + c) y \cdot 0 = 0 \cdot y \cdot 0 + c y \cdot 0$
30	13 10 28 29	mp3an2i	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to (0 + c) y \cdot 0 = 0 \cdot y \cdot 0 + c y \cdot 0$
31	24 30	eqtr3d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 = 0 \cdot y \cdot 0 + c y \cdot 0$
32	31	oveq1d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 + 0 = 0 \cdot y \cdot 0 + c y \cdot 0 + 0$
33		remulcl	$⊢ (0 \in ℝ \land y \cdot 0 \in ℝ) \to 0 \cdot y \cdot 0 \in ℝ$
34	1 26 33	sylancr	$⊢ y \in ℝ \to 0 \cdot y \cdot 0 \in ℝ$
35	34	ad2antrl	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 \in ℝ$
36	35	recnd	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 \in ℂ$
37		remulcl	$⊢ (c \in ℝ \land y \cdot 0 \in ℝ) \to c y \cdot 0 \in ℝ$
38	9 27 37	syl2anc	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 \in ℝ$
39	38	recnd	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 \in ℂ$
40		addass	$⊢ (0 \cdot y \cdot 0 \in ℂ \land c y \cdot 0 \in ℂ \land 0 \in ℂ) \to 0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + c y \cdot 0 + 0$
41	13 40	mp3an3	$⊢ (0 \cdot y \cdot 0 \in ℂ \land c y \cdot 0 \in ℂ) \to 0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + c y \cdot 0 + 0$
42	36 39 41	syl2anc	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + c y \cdot 0 + 0$
43	32 42	eqtr2d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + 0$
44	26 37	sylan2	$⊢ (c \in ℝ \land y \in ℝ) \to c y \cdot 0 \in ℝ$
45		readdcl	$⊢ (c y \cdot 0 \in ℝ \land 0 \in ℝ) \to c y \cdot 0 + 0 \in ℝ$
46	44 1 45	sylancl	$⊢ (c \in ℝ \land y \in ℝ) \to c y \cdot 0 + 0 \in ℝ$
47	9 11 46	syl2anc	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 + 0 \in ℝ$
48		readdcan	$⊢ (c y \cdot 0 + 0 \in ℝ \land 0 \in ℝ \land 0 \cdot y \cdot 0 \in ℝ) \to (0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + 0 \leftrightarrow c y \cdot 0 + 0 = 0)$
49	1 48	mp3an2	$⊢ (c y \cdot 0 + 0 \in ℝ \land 0 \cdot y \cdot 0 \in ℝ) \to (0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + 0 \leftrightarrow c y \cdot 0 + 0 = 0)$
50	47 35 49	syl2anc	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to (0 \cdot y \cdot 0 + c y \cdot 0 + 0 = 0 \cdot y \cdot 0 + 0 \leftrightarrow c y \cdot 0 + 0 = 0)$
51	43 50	mpbid	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to c y \cdot 0 + 0 = 0$
52	22 51	eqtr3d	$⊢ (((c \in ℝ \land 0 + c = 0) \land c \neq 0) \land (y \in ℝ \land c y = 1)) \to 0 + 0 = 0$
53	8 52	rexlimddv	$⊢ ((c \in ℝ \land 0 + c = 0) \land c \neq 0) \to 0 + 0 = 0$
54	53	expcom	$⊢ c \neq 0 \to ((c \in ℝ \land 0 + c = 0) \to 0 + 0 = 0)$
55	6 54	pm2.61ine	$⊢ (c \in ℝ \land 0 + c = 0) \to 0 + 0 = 0$
56	55	rexlimiva	$⊢ \exists c \in ℝ 0 + c = 0 \to 0 + 0 = 0$
57	1 2 56	mp2b	$⊢ 0 + 0 = 0$

Metamath Proof Explorer

Theorem 00id

Proof