Theorem mulid1 9916

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 9915	. 2 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2		recn 9905	. . . . . 6 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3		ax-icn 9874	. . . . . . 7 ⊢ i ∈ ℂ
4		recn 9905	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5		mulcl 9899	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
6	3, 4, 5	sylancr 694	. . . . . 6 ⊢ (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7		ax-1cn 9873	. . . . . . 7 ⊢ 1 ∈ ℂ
8		adddir 9910	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
9	7, 8	mp3an3 1405	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
10	2, 6, 9	syl2an 493	. . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11		ax-1rid 9885	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12		mulass 9903	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
13	3, 7, 12	mp3an13 1407	. . . . . . . 8 ⊢ (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
14	4, 13	syl 17	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15		ax-1rid 9885	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
16	15	oveq2d 6565	. . . . . . 7 ⊢ (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
17	14, 16	eqtrd 2644	. . . . . 6 ⊢ (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
18	11, 17	oveqan12d 6568	. . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
19	10, 18	eqtrd 2644	. . . 4 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20		oveq1 6556	. . . . 5 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21		id 22	. . . . 5 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
22	20, 21	eqeq12d 2625	. . . 4 ⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
23	19, 22	syl5ibrcom 236	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
24	23	rexlimivv 3018	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
25	1, 24	syl 17	1 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  (class class class)co 6549  ℂcc 9813  ℝcr 9814  1c1 9816  ici 9817   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  mulid2  9917  mulid1i  9921  mulid1d  9936  muleqadd  10550  divdiv1  10615  conjmul  10621  nnmulcl  10920  expmul  12767  binom21  12842  binom2sub1  12844  sq01  12848  bernneq  12852  hashiun  14395  fprodcvg  14499  prodmolem2a  14503  efexp  14670  cncrng  19586  cnfld1  19590  0dgr  23805  ecxp  24219  dvcxp1  24281  dvcncxp1  24284  efrlim  24496  lgsdilem2  24858  axcontlem7  25650  ipasslem2  27071  addltmulALT  28689  zrhnm  29341  2even  41723