Theorem addid1 10616

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.)

Assertion

Ref	Expression
addid1	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1

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

Step	Hyp	Ref	Expression
1		1re 10435	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 10402	. 2 ⊢ (1 ∈ ℝ → ∃𝑐 ∈ ℝ (1 + 𝑐) = 0)
3		ax-1ne0 10400	. . . . . 6 ⊢ 1 ≠ 0
4		oveq2 6982	. . . . . . . . . 10 ⊢ (𝑐 = 0 → (1 + 𝑐) = (1 + 0))
5	4	eqeq1d 2777	. . . . . . . . 9 ⊢ (𝑐 = 0 → ((1 + 𝑐) = 0 ↔ (1 + 0) = 0))
6	5	biimpcd 241	. . . . . . . 8 ⊢ ((1 + 𝑐) = 0 → (𝑐 = 0 → (1 + 0) = 0))
7		oveq2 6982	. . . . . . . . 9 ⊢ ((1 + 0) = 0 → (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0))
8		ax-icn 10390	. . . . . . . . . . . . . . 15 ⊢ i ∈ ℂ
9	8, 8	mulcli 10443	. . . . . . . . . . . . . 14 ⊢ (i · i) ∈ ℂ
10	9, 9	mulcli 10443	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) ∈ ℂ
11		ax-1cn 10389	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
12		0cn 10427	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℂ
13	10, 11, 12	adddii 10448	. . . . . . . . . . . 12 ⊢ (((i · i) · (i · i)) · (1 + 0)) = ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0))
14	10	mulid1i 10440	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) · 1) = ((i · i) · (i · i))
15		mul01 10615	. . . . . . . . . . . . . . 15 ⊢ (((i · i) · (i · i)) ∈ ℂ → (((i · i) · (i · i)) · 0) = 0)
16	10, 15	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (((i · i) · (i · i)) · 0) = 0
17		ax-i2m1 10399	. . . . . . . . . . . . . 14 ⊢ ((i · i) + 1) = 0
18	16, 17	eqtr4i 2802	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) · 0) = ((i · i) + 1)
19	14, 18	oveq12i 6986	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
20	13, 19	eqtri 2799	. . . . . . . . . . 11 ⊢ (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
21	20, 16	eqeq12i 2789	. . . . . . . . . 10 ⊢ ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ (((i · i) · (i · i)) + ((i · i) + 1)) = 0)
22	10, 9, 11	addassi 10446	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) + (i · i)) + 1) = (((i · i) · (i · i)) + ((i · i) + 1))
23	9	mulid1i 10440	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · 1) = (i · i)
24	23	oveq2i 6985	. . . . . . . . . . . . . 14 ⊢ (((i · i) · (i · i)) + ((i · i) · 1)) = (((i · i) · (i · i)) + (i · i))
25	9, 9, 11	adddii 10448	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · ((i · i) + 1)) = (((i · i) · (i · i)) + ((i · i) · 1))
26	17	oveq2i 6985	. . . . . . . . . . . . . . . 16 ⊢ ((i · i) · ((i · i) + 1)) = ((i · i) · 0)
27		mul01 10615	. . . . . . . . . . . . . . . . 17 ⊢ ((i · i) ∈ ℂ → ((i · i) · 0) = 0)
28	9, 27	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((i · i) · 0) = 0
29	26, 28	eqtri 2799	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · ((i · i) + 1)) = 0
30	25, 29	eqtr3i 2801	. . . . . . . . . . . . . 14 ⊢ (((i · i) · (i · i)) + ((i · i) · 1)) = 0
31	24, 30	eqtr3i 2801	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) + (i · i)) = 0
32	31	oveq1i 6984	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) + (i · i)) + 1) = (0 + 1)
33	22, 32	eqtr3i 2801	. . . . . . . . . . 11 ⊢ (((i · i) · (i · i)) + ((i · i) + 1)) = (0 + 1)
34		00id 10611	. . . . . . . . . . . 12 ⊢ (0 + 0) = 0
35	34	eqcomi 2784	. . . . . . . . . . 11 ⊢ 0 = (0 + 0)
36	33, 35	eqeq12i 2789	. . . . . . . . . 10 ⊢ ((((i · i) · (i · i)) + ((i · i) + 1)) = 0 ↔ (0 + 1) = (0 + 0))
37		0re 10437	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
38		readdcan 10610	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 + 1) = (0 + 0) ↔ 1 = 0))
39	1, 37, 37, 38	mp3an 1440	. . . . . . . . . 10 ⊢ ((0 + 1) = (0 + 0) ↔ 1 = 0)
40	21, 36, 39	3bitri 289	. . . . . . . . 9 ⊢ ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ 1 = 0)
41	7, 40	sylib 210	. . . . . . . 8 ⊢ ((1 + 0) = 0 → 1 = 0)
42	6, 41	syl6 35	. . . . . . 7 ⊢ ((1 + 𝑐) = 0 → (𝑐 = 0 → 1 = 0))
43	42	necon3d 2985	. . . . . 6 ⊢ ((1 + 𝑐) = 0 → (1 ≠ 0 → 𝑐 ≠ 0))
44	3, 43	mpi 20	. . . . 5 ⊢ ((1 + 𝑐) = 0 → 𝑐 ≠ 0)
45		ax-rrecex 10403	. . . . 5 ⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
46	44, 45	sylan2 583	. . . 4 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
47		simpr 477	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ)
48		simplrl 764	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℝ)
49	48	recnd 10464	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℂ)
50	47, 49	mulcld 10456	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ)
51		simplll 762	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℝ)
52	51	recnd 10464	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℂ)
53	12	a1i 11	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℂ)
54	50, 52, 53	adddid 10460	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)))
55	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℂ)
56	55, 52, 53	addassd 10458	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (1 + (𝑐 + 0)))
57		simpllr 763	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + 𝑐) = 0)
58	57	oveq1d 6989	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (0 + 0))
59	56, 58	eqtr3d 2813	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (0 + 0))
60	34, 59, 57	3eqtr4a 2837	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (1 + 𝑐))
61	37	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℝ)
62	51, 61	readdcld 10465	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) ∈ ℝ)
63	1	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℝ)
64		readdcan 10610	. . . . . . . . . . 11 ⊢ (((𝑐 + 0) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈ ℝ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
65	62, 51, 63, 64	syl3anc 1351	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
66	60, 65	mpbid 224	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) = 𝑐)
67	66	oveq2d 6990	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = ((𝐴 · 𝑥) · 𝑐))
68	54, 67	eqtr3d 2813	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = ((𝐴 · 𝑥) · 𝑐))
69		mul31 10603	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
70	47, 49, 52, 69	syl3anc 1351	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
71		simplrr 765	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 · 𝑥) = 1)
72	71	oveq1d 6989	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝑐 · 𝑥) · 𝐴) = (1 · 𝐴))
73	47	mulid2d 10454	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = 𝐴)
74	70, 72, 73	3eqtrd 2815	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = 𝐴)
75		mul01 10615	. . . . . . . . 9 ⊢ ((𝐴 · 𝑥) ∈ ℂ → ((𝐴 · 𝑥) · 0) = 0)
76	50, 75	syl 17	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 0) = 0)
77	74, 76	oveq12d 6992	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = (𝐴 + 0))
78	68, 77, 74	3eqtr3d 2819	. . . . . 6 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 + 0) = 𝐴)
79	78	exp42 428	. . . . 5 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝑥 ∈ ℝ → ((𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))))
80	79	rexlimdv 3225	. . . 4 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)))
81	46, 80	mpd 15	. . 3 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
82	81	rexlimiva 3223	. 2 ⊢ (∃𝑐 ∈ ℝ (1 + 𝑐) = 0 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
83	1, 2, 82	mp2b 10	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2048   ≠ wne 2964  ∃wrex 3086  (class class class)co 6974  ℂcc 10329  ℝcr 10330  0cc0 10331  1c1 10332  ici 10333   + caddc 10334   · cmul 10336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-po 5323  df-so 5324  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-ov 6977  df-er 8085  df-en 8303  df-dom 8304  df-sdom 8305  df-pnf 10472  df-mnf 10473  df-ltxr 10475

This theorem is referenced by:  cnegex  10617  addid2  10619  addcan2  10621  addid1i  10623  addid1d  10636  subid  10702  subid1  10703  addid0  10856  swrdccat3blem  13938  shftval3  14290  reim0  14332  isercolllem3  14878  fsumcvg  14923  summolem2a  14926  risefac1  15241  cnaddid  18740  ovolicc1  23814  addsqnreup  25715  brbtwn2  26388  axsegconlem1  26400  ax5seglem4  26415  axeuclid  26446  axcontlem2  26448  axcontlem4  26450  stoweidlem26  41721  2zrngamnd  43550  aacllem  44243