Theorem addrid 11314

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
addrid	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Proof of Theorem addrid

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

Step	Hyp	Ref	Expression
1		1re 11133	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 11098	. 2 ⊢ (1 ∈ ℝ → ∃𝑐 ∈ ℝ (1 + 𝑐) = 0)
3		ax-1ne0 11096	. . . . . 6 ⊢ 1 ≠ 0
4		oveq2 7366	. . . . . . . . . 10 ⊢ (𝑐 = 0 → (1 + 𝑐) = (1 + 0))
5	4	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑐 = 0 → ((1 + 𝑐) = 0 ↔ (1 + 0) = 0))
6	5	biimpcd 249	. . . . . . . 8 ⊢ ((1 + 𝑐) = 0 → (𝑐 = 0 → (1 + 0) = 0))
7		oveq2 7366	. . . . . . . . 9 ⊢ ((1 + 0) = 0 → (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0))
8		ax-icn 11086	. . . . . . . . . . . . . . 15 ⊢ i ∈ ℂ
9	8, 8	mulcli 11140	. . . . . . . . . . . . . 14 ⊢ (i · i) ∈ ℂ
10	9, 9	mulcli 11140	. . . . . . . . . . . . 13 ⊢ ((i · i) · (i · i)) ∈ ℂ
11		ax-1cn 11085	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
12		0cn 11125	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℂ
13	10, 11, 12	adddii 11145	. . . . . . . . . . . 12 ⊢ (((i · i) · (i · i)) · (1 + 0)) = ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0))
14	10	mulridi 11137	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) · 1) = ((i · i) · (i · i))
15		mul01 11313	. . . . . . . . . . . . . . 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 11095	. . . . . . . . . . . . . 14 ⊢ ((i · i) + 1) = 0
18	16, 17	eqtr4i 2763	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) · 0) = ((i · i) + 1)
19	14, 18	oveq12i 7370	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
20	13, 19	eqtri 2760	. . . . . . . . . . 11 ⊢ (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
21	20, 16	eqeq12i 2755	. . . . . . . . . 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 11143	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) + (i · i)) + 1) = (((i · i) · (i · i)) + ((i · i) + 1))
23	9	mulridi 11137	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · 1) = (i · i)
24	23	oveq2i 7369	. . . . . . . . . . . . . 14 ⊢ (((i · i) · (i · i)) + ((i · i) · 1)) = (((i · i) · (i · i)) + (i · i))
25	9, 9, 11	adddii 11145	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · ((i · i) + 1)) = (((i · i) · (i · i)) + ((i · i) · 1))
26	17	oveq2i 7369	. . . . . . . . . . . . . . . 16 ⊢ ((i · i) · ((i · i) + 1)) = ((i · i) · 0)
27		mul01 11313	. . . . . . . . . . . . . . . . 17 ⊢ ((i · i) ∈ ℂ → ((i · i) · 0) = 0)
28	9, 27	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((i · i) · 0) = 0
29	26, 28	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · ((i · i) + 1)) = 0
30	25, 29	eqtr3i 2762	. . . . . . . . . . . . . 14 ⊢ (((i · i) · (i · i)) + ((i · i) · 1)) = 0
31	24, 30	eqtr3i 2762	. . . . . . . . . . . . 13 ⊢ (((i · i) · (i · i)) + (i · i)) = 0
32	31	oveq1i 7368	. . . . . . . . . . . 12 ⊢ ((((i · i) · (i · i)) + (i · i)) + 1) = (0 + 1)
33	22, 32	eqtr3i 2762	. . . . . . . . . . 11 ⊢ (((i · i) · (i · i)) + ((i · i) + 1)) = (0 + 1)
34		00id 11309	. . . . . . . . . . . 12 ⊢ (0 + 0) = 0
35	34	eqcomi 2746	. . . . . . . . . . 11 ⊢ 0 = (0 + 0)
36	33, 35	eqeq12i 2755	. . . . . . . . . 10 ⊢ ((((i · i) · (i · i)) + ((i · i) + 1)) = 0 ↔ (0 + 1) = (0 + 0))
37		0re 11135	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
38		readdcan 11308	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 + 1) = (0 + 0) ↔ 1 = 0))
39	1, 37, 37, 38	mp3an 1464	. . . . . . . . . 10 ⊢ ((0 + 1) = (0 + 0) ↔ 1 = 0)
40	21, 36, 39	3bitri 297	. . . . . . . . 9 ⊢ ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ 1 = 0)
41	7, 40	sylib 218	. . . . . . . 8 ⊢ ((1 + 0) = 0 → 1 = 0)
42	6, 41	syl6 35	. . . . . . 7 ⊢ ((1 + 𝑐) = 0 → (𝑐 = 0 → 1 = 0))
43	42	necon3d 2954	. . . . . 6 ⊢ ((1 + 𝑐) = 0 → (1 ≠ 0 → 𝑐 ≠ 0))
44	3, 43	mpi 20	. . . . 5 ⊢ ((1 + 𝑐) = 0 → 𝑐 ≠ 0)
45		ax-rrecex 11099	. . . . 5 ⊢ ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
46	44, 45	sylan2 594	. . . 4 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
47		simpr 484	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ)
48		simplrl 777	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℝ)
49	48	recnd 11161	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℂ)
50	47, 49	mulcld 11153	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ)
51		simplll 775	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℝ)
52	51	recnd 11161	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℂ)
53	12	a1i 11	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℂ)
54	50, 52, 53	adddid 11157	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)))
55	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℂ)
56	55, 52, 53	addassd 11155	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (1 + (𝑐 + 0)))
57		simpllr 776	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + 𝑐) = 0)
58	57	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (0 + 0))
59	56, 58	eqtr3d 2774	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (0 + 0))
60	34, 59, 57	3eqtr4a 2798	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (1 + 𝑐))
61	37	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℝ)
62	51, 61	readdcld 11162	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) ∈ ℝ)
63	1	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℝ)
64		readdcan 11308	. . . . . . . . . . 11 ⊢ (((𝑐 + 0) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈ ℝ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
65	62, 51, 63, 64	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
66	60, 65	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) = 𝑐)
67	66	oveq2d 7374	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = ((𝐴 · 𝑥) · 𝑐))
68	54, 67	eqtr3d 2774	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = ((𝐴 · 𝑥) · 𝑐))
69		mul31 11301	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
70	47, 49, 52, 69	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
71		simplrr 778	. . . . . . . . . 10 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 · 𝑥) = 1)
72	71	oveq1d 7373	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝑐 · 𝑥) · 𝐴) = (1 · 𝐴))
73	47	mullidd 11151	. . . . . . . . 9 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = 𝐴)
74	70, 72, 73	3eqtrd 2776	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = 𝐴)
75		mul01 11313	. . . . . . . . 9 ⊢ ((𝐴 · 𝑥) ∈ ℂ → ((𝐴 · 𝑥) · 0) = 0)
76	50, 75	syl 17	. . . . . . . 8 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 0) = 0)
77	74, 76	oveq12d 7376	. . . . . . 7 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = (𝐴 + 0))
78	68, 77, 74	3eqtr3d 2780	. . . . . 6 ⊢ ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 + 0) = 𝐴)
79	78	exp42 435	. . . . 5 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝑥 ∈ ℝ → ((𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))))
80	79	rexlimdv 3137	. . . 4 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)))
81	46, 80	mpd 15	. . 3 ⊢ ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
82	81	rexlimiva 3131	. 2 ⊢ (∃𝑐 ∈ ℝ (1 + 𝑐) = 0 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
83	1, 2, 82	mp2b 10	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∃wrex 3062  (class class class)co 7358  ℂcc 11025  ℝcr 11026  0cc0 11027  1c1 11028  ici 11029   + caddc 11030   · cmul 11032

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172

This theorem is referenced by:  cnegex  11315  addlid  11317  addcan2  11319  addridi  11321  addridd  11334  subid  11401  subid1  11402  addid0  11557  swrdccat3blem  14663  shftval3  15000  reim0  15042  isercolllem3  15591  fsumcvg  15636  summolem2a  15639  risefac1  15957  chnccat  18550  cnaddid  19803  ovolicc1  25461  addsqnreup  27394  brbtwn2  28962  axsegconlem1  28974  ax5seglem4  28989  axeuclid  29020  axcontlem2  29022  axcontlem4  29024  gsumzrsum  33131  stoweidlem26  46458  2zrngamnd  48681  aacllem  50234