addid1

Description: 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	addid1	$⊢ A \in ℂ \to A + 0 = A$

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		ax-rnegex	$⊢ 1 \in ℝ \to \exists c \in ℝ 1 + c = 0$
3		ax-1ne0	$⊢ 1 \neq 0$
4		oveq2	$⊢ c = 0 \to 1 + c = 1 + 0$
5	4	eqeq1d	$⊢ c = 0 \to (1 + c = 0 \leftrightarrow 1 + 0 = 0)$
6	5	biimpcd	$⊢ 1 + c = 0 \to (c = 0 \to 1 + 0 = 0)$
7		oveq2	$⊢ 1 + 0 = 0 \to i i i i (1 + 0) = i i i i \cdot 0$
8		ax-icn	$⊢ i \in ℂ$
9	8 8	mulcli	$⊢ i i \in ℂ$
10	9 9	mulcli	$⊢ i i i i \in ℂ$
11		ax-1cn	$⊢ 1 \in ℂ$
12		0cn	$⊢ 0 \in ℂ$
13	10 11 12	adddii	$⊢ i i i i (1 + 0) = i i i i \cdot 1 + i i i i \cdot 0$
14	10	mulid1i	$⊢ i i i i \cdot 1 = i i i i$
15		mul01	$⊢ i i i i \in ℂ \to i i i i \cdot 0 = 0$
16	10 15	ax-mp	$⊢ i i i i \cdot 0 = 0$
17		ax-i2m1	$⊢ i i + 1 = 0$
18	16 17	eqtr4i	$⊢ i i i i \cdot 0 = i i + 1$
19	14 18	oveq12i	$⊢ i i i i \cdot 1 + i i i i \cdot 0 = i i i i + i i + 1$
20	13 19	eqtri	$⊢ i i i i (1 + 0) = i i i i + i i + 1$
21	20 16	eqeq12i	$⊢ i i i i (1 + 0) = i i i i \cdot 0 \leftrightarrow i i i i + i i + 1 = 0$
22	10 9 11	addassi	$⊢ i i i i + i i + 1 = i i i i + i i + 1$
23	9	mulid1i	$⊢ i i \cdot 1 = i i$
24	23	oveq2i	$⊢ i i i i + i i \cdot 1 = i i i i + i i$
25	9 9 11	adddii	$⊢ i i (i i + 1) = i i i i + i i \cdot 1$
26	17	oveq2i	$⊢ i i (i i + 1) = i i \cdot 0$
27		mul01	$⊢ i i \in ℂ \to i i \cdot 0 = 0$
28	9 27	ax-mp	$⊢ i i \cdot 0 = 0$
29	26 28	eqtri	$⊢ i i (i i + 1) = 0$
30	25 29	eqtr3i	$⊢ i i i i + i i \cdot 1 = 0$
31	24 30	eqtr3i	$⊢ i i i i + i i = 0$
32	31	oveq1i	$⊢ i i i i + i i + 1 = 0 + 1$
33	22 32	eqtr3i	$⊢ i i i i + i i + 1 = 0 + 1$
34		00id	$⊢ 0 + 0 = 0$
35	34	eqcomi	$⊢ 0 = 0 + 0$
36	33 35	eqeq12i	$⊢ i i i i + i i + 1 = 0 \leftrightarrow 0 + 1 = 0 + 0$
37		0re	$⊢ 0 \in ℝ$
38		readdcan	$⊢ (1 \in ℝ \land 0 \in ℝ \land 0 \in ℝ) \to (0 + 1 = 0 + 0 \leftrightarrow 1 = 0)$
39	1 37 37 38	mp3an	$⊢ 0 + 1 = 0 + 0 \leftrightarrow 1 = 0$
40	21 36 39	3bitri	$⊢ i i i i (1 + 0) = i i i i \cdot 0 \leftrightarrow 1 = 0$
41	7 40	sylib	$⊢ 1 + 0 = 0 \to 1 = 0$
42	6 41	syl6	$⊢ 1 + c = 0 \to (c = 0 \to 1 = 0)$
43	42	necon3d	$⊢ 1 + c = 0 \to (1 \neq 0 \to c \neq 0)$
44	3 43	mpi	$⊢ 1 + c = 0 \to c \neq 0$
45		ax-rrecex	$⊢ (c \in ℝ \land c \neq 0) \to \exists x \in ℝ c x = 1$
46	44 45	sylan2	$⊢ (c \in ℝ \land 1 + c = 0) \to \exists x \in ℝ c x = 1$
47		simpr	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A \in ℂ$
48		simplrl	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to x \in ℝ$
49	48	recnd	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to x \in ℂ$
50	47 49	mulcld	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x \in ℂ$
51		simplll	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c \in ℝ$
52	51	recnd	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c \in ℂ$
53	12	a1i	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 0 \in ℂ$
54	50 52 53	adddid	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x (c + 0) = A x c + A x \cdot 0$
55	11	a1i	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 \in ℂ$
56	55 52 53	addassd	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 + c + 0 = 1 + c + 0$
57		simpllr	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 + c = 0$
58	57	oveq1d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 + c + 0 = 0 + 0$
59	56 58	eqtr3d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 + c + 0 = 0 + 0$
60	34 59 57	3eqtr4a	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 + c + 0 = 1 + c$
61	37	a1i	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 0 \in ℝ$
62	51 61	readdcld	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c + 0 \in ℝ$
63	1	a1i	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 \in ℝ$
64		readdcan	$⊢ (c + 0 \in ℝ \land c \in ℝ \land 1 \in ℝ) \to (1 + c + 0 = 1 + c \leftrightarrow c + 0 = c)$
65	62 51 63 64	syl3anc	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to (1 + c + 0 = 1 + c \leftrightarrow c + 0 = c)$
66	60 65	mpbid	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c + 0 = c$
67	66	oveq2d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x (c + 0) = A x c$
68	54 67	eqtr3d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x c + A x \cdot 0 = A x c$
69		mul31	$⊢ (A \in ℂ \land x \in ℂ \land c \in ℂ) \to A x c = c x A$
70	47 49 52 69	syl3anc	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x c = c x A$
71		simplrr	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c x = 1$
72	71	oveq1d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to c x A = 1 A$
73	47	mulid2d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to 1 A = A$
74	70 72 73	3eqtrd	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x c = A$
75		mul01	$⊢ A x \in ℂ \to A x \cdot 0 = 0$
76	50 75	syl	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x \cdot 0 = 0$
77	74 76	oveq12d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A x c + A x \cdot 0 = A + 0$
78	68 77 74	3eqtr3d	$⊢ (((c \in ℝ \land 1 + c = 0) \land (x \in ℝ \land c x = 1)) \land A \in ℂ) \to A + 0 = A$
79	78	exp42	$⊢ (c \in ℝ \land 1 + c = 0) \to (x \in ℝ \to (c x = 1 \to (A \in ℂ \to A + 0 = A)))$
80	79	rexlimdv	$⊢ (c \in ℝ \land 1 + c = 0) \to (\exists x \in ℝ c x = 1 \to (A \in ℂ \to A + 0 = A))$
81	46 80	mpd	$⊢ (c \in ℝ \land 1 + c = 0) \to (A \in ℂ \to A + 0 = A)$
82	81	rexlimiva	$⊢ \exists c \in ℝ 1 + c = 0 \to (A \in ℂ \to A + 0 = A)$
83	1 2 82	mp2b	$⊢ A \in ℂ \to A + 0 = A$

Metamath Proof Explorer

Theorem addid1

Proof