MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid1 Structured version   Visualization version   GIF version

Theorem mulid1 10628
Description: The number 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.
StepHypRef Expression
1 cnre 10627 . 2 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2 recn 10616 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3 ax-icn 10585 . . . . . . 7 i ∈ ℂ
4 recn 10616 . . . . . . 7 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5 mulcl 10610 . . . . . . 7 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
63, 4, 5sylancr 590 . . . . . 6 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7 ax-1cn 10584 . . . . . . 7 1 ∈ ℂ
8 adddir 10621 . . . . . . 7 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
97, 8mp3an3 1447 . . . . . 6 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
102, 6, 9syl2an 598 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11 ax-1rid 10596 . . . . . 6 (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12 mulass 10614 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
133, 7, 12mp3an13 1449 . . . . . . . 8 (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
144, 13syl 17 . . . . . . 7 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15 ax-1rid 10596 . . . . . . . 8 (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
1615oveq2d 7156 . . . . . . 7 (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
1714, 16eqtrd 2857 . . . . . 6 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
1811, 17oveqan12d 7159 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
1910, 18eqtrd 2857 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20 oveq1 7147 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21 id 22 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
2220, 21eqeq12d 2838 . . . 4 (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
2319, 22syl5ibrcom 250 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
2423rexlimivv 3278 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
251, 24syl 17 1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2114  wrex 3131  (class class class)co 7140  cc 10524  cr 10525  1c1 10527  ici 10528   + caddc 10529   · cmul 10531
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-rex 3136  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143
This theorem is referenced by:  mulid2  10629  mulid1i  10634  mulid1d  10647  muleqadd  11273  divdiv1  11340  conjmul  11346  expmul  13470  binom21  13576  binom2sub1  13578  sq01  13582  bernneq  13586  hashiun  15168  fprodcvg  15275  prodmolem2a  15279  efexp  15445  cncrng  20110  cnfld1  20114  0dgr  24840  ecxp  25262  dvcxp1  25327  dvcncxp1  25330  efrlim  25553  lgsdilem2  25915  axcontlem7  26762  ipasslem2  28613  addltmulALT  30227  0dp2dp  30595  zrhnm  31284  2even  44496
  Copyright terms: Public domain W3C validator