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

Theorem mulid1 10221
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.
StepHypRef Expression
1 cnre 10220 . 2 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2 recn 10210 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3 ax-icn 10179 . . . . . . 7 i ∈ ℂ
4 recn 10210 . . . . . . 7 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5 mulcl 10204 . . . . . . 7 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
63, 4, 5sylancr 698 . . . . . 6 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7 ax-1cn 10178 . . . . . . 7 1 ∈ ℂ
8 adddir 10215 . . . . . . 7 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
97, 8mp3an3 1554 . . . . . 6 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
102, 6, 9syl2an 495 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11 ax-1rid 10190 . . . . . 6 (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12 mulass 10208 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
133, 7, 12mp3an13 1556 . . . . . . . 8 (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
144, 13syl 17 . . . . . . 7 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15 ax-1rid 10190 . . . . . . . 8 (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
1615oveq2d 6821 . . . . . . 7 (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
1714, 16eqtrd 2786 . . . . . 6 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
1811, 17oveqan12d 6824 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
1910, 18eqtrd 2786 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20 oveq1 6812 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21 id 22 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
2220, 21eqeq12d 2767 . . . 4 (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
2319, 22syl5ibrcom 237 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
2423rexlimivv 3166 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
251, 24syl 17 1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wcel 2131  wrex 3043  (class class class)co 6805  cc 10118  cr 10119  1c1 10121  ici 10122   + caddc 10123   · cmul 10125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-mulcl 10182  ax-mulcom 10184  ax-mulass 10186  ax-distr 10187  ax-1rid 10190  ax-cnre 10193
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808
This theorem is referenced by:  mulid2  10222  mulid1i  10226  mulid1d  10241  muleqadd  10855  divdiv1  10920  conjmul  10926  nnmulcl  11227  expmul  13091  binom21  13166  binom2sub1  13168  sq01  13172  bernneq  13176  hashiun  14745  fprodcvg  14851  prodmolem2a  14855  efexp  15022  cncrng  19961  cnfld1  19965  0dgr  24192  ecxp  24610  dvcxp1  24672  dvcncxp1  24675  efrlim  24887  lgsdilem2  25249  axcontlem7  26041  ipasslem2  27988  addltmulALT  29606  0dp2dp  29918  zrhnm  30314  2even  42435
  Copyright terms: Public domain W3C validator