Theorem mulid1 7116

Description: 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
mulid1	⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)

Proof of Theorem mulid1

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

Step	Hyp	Ref	Expression
1		cnre 7115	. 2 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2		recn 7106	. . . . . 6 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3		ax-icn 7071	. . . . . . 7 ⊢ i ∈ ℂ
4		recn 7106	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5		mulcl 7100	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
6	3, 4, 5	sylancr 405	. . . . . 6 ⊢ (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7		ax-1cn 7069	. . . . . . 7 ⊢ 1 ∈ ℂ
8		adddir 7110	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
9	7, 8	mp3an3 1257	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
10	2, 6, 9	syl2an 283	. . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11		ax-1rid 7083	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12		mulass 7104	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
13	3, 7, 12	mp3an13 1259	. . . . . . . 8 ⊢ (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
14	4, 13	syl 14	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15		ax-1rid 7083	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
16	15	oveq2d 5548	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
17	14, 16	eqtrd 2113	. . . . . 6 ⊢ (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
18	11, 17	oveqan12d 5551	. . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
19	10, 18	eqtrd 2113	. . . 4 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20		oveq1 5539	. . . . 5 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21		id 19	. . . . 5 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
22	20, 21	eqeq12d 2095	. . . 4 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
23	19, 22	syl5ibrcom 155	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
24	23	rexlimivv 2482	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
25	1, 24	syl 14	1 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1284   ∈ wcel 1433  ∃wrex 2349  (class class class)co 5532  ℂcc 6979  ℝcr 6980  1c1 6982  ici 6983   + caddc 6984   · cmul 6986

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-mulcl 7074  ax-mulcom 7077  ax-mulass 7079  ax-distr 7080  ax-1rid 7083  ax-cnre 7087

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  mulid2  7117  mulid1i  7121  mulid1d  7136  muleqadd  7758  divdivap1  7811  conjmulap  7817  nnmulcl  8060  expmul  9521  binom21  9586  bernneq  9593