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

Theorem mulid1 10627
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 10626 . 2 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2 recn 10615 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3 ax-icn 10584 . . . . . . 7 i ∈ ℂ
4 recn 10615 . . . . . . 7 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5 mulcl 10609 . . . . . . 7 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
63, 4, 5sylancr 587 . . . . . 6 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7 ax-1cn 10583 . . . . . . 7 1 ∈ ℂ
8 adddir 10620 . . . . . . 7 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
97, 8mp3an3 1441 . . . . . 6 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
102, 6, 9syl2an 595 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11 ax-1rid 10595 . . . . . 6 (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12 mulass 10613 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
133, 7, 12mp3an13 1443 . . . . . . . 8 (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
144, 13syl 17 . . . . . . 7 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15 ax-1rid 10595 . . . . . . . 8 (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
1615oveq2d 7161 . . . . . . 7 (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
1714, 16eqtrd 2853 . . . . . 6 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
1811, 17oveqan12d 7164 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
1910, 18eqtrd 2853 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20 oveq1 7152 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21 id 22 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
2220, 21eqeq12d 2834 . . . 4 (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
2319, 22syl5ibrcom 248 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
2423rexlimivv 3289 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
251, 24syl 17 1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wrex 3136  (class class class)co 7145  cc 10523  cr 10524  1c1 10526  ici 10527   + caddc 10528   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulcom 10589  ax-mulass 10591  ax-distr 10592  ax-1rid 10595  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  mulid2  10628  mulid1i  10633  mulid1d  10646  muleqadd  11272  divdiv1  11339  conjmul  11345  expmul  13462  binom21  13568  binom2sub1  13570  sq01  13574  bernneq  13578  hashiun  15165  fprodcvg  15272  prodmolem2a  15276  efexp  15442  cncrng  20494  cnfld1  20498  0dgr  24762  ecxp  25183  dvcxp1  25248  dvcncxp1  25251  efrlim  25474  lgsdilem2  25836  axcontlem7  26683  ipasslem2  28536  addltmulALT  30150  0dp2dp  30512  zrhnm  31109  2even  44132
  Copyright terms: Public domain W3C validator