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

Theorem mulid1 11160
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 11159 . 2 (๐ด โˆˆ โ„‚ โ†’ โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
2 recn 11148 . . . . . 6 (๐‘ฅ โˆˆ โ„ โ†’ ๐‘ฅ โˆˆ โ„‚)
3 ax-icn 11117 . . . . . . 7 i โˆˆ โ„‚
4 recn 11148 . . . . . . 7 (๐‘ฆ โˆˆ โ„ โ†’ ๐‘ฆ โˆˆ โ„‚)
5 mulcl 11142 . . . . . . 7 ((i โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (i ยท ๐‘ฆ) โˆˆ โ„‚)
63, 4, 5sylancr 588 . . . . . 6 (๐‘ฆ โˆˆ โ„ โ†’ (i ยท ๐‘ฆ) โˆˆ โ„‚)
7 ax-1cn 11116 . . . . . . 7 1 โˆˆ โ„‚
8 adddir 11153 . . . . . . 7 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1) = ((๐‘ฅ ยท 1) + ((i ยท ๐‘ฆ) ยท 1)))
97, 8mp3an3 1451 . . . . . 6 ((๐‘ฅ โˆˆ โ„‚ โˆง (i ยท ๐‘ฆ) โˆˆ โ„‚) โ†’ ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1) = ((๐‘ฅ ยท 1) + ((i ยท ๐‘ฆ) ยท 1)))
102, 6, 9syl2an 597 . . . . 5 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1) = ((๐‘ฅ ยท 1) + ((i ยท ๐‘ฆ) ยท 1)))
11 ax-1rid 11128 . . . . . 6 (๐‘ฅ โˆˆ โ„ โ†’ (๐‘ฅ ยท 1) = ๐‘ฅ)
12 mulass 11146 . . . . . . . . 9 ((i โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((i ยท ๐‘ฆ) ยท 1) = (i ยท (๐‘ฆ ยท 1)))
133, 7, 12mp3an13 1453 . . . . . . . 8 (๐‘ฆ โˆˆ โ„‚ โ†’ ((i ยท ๐‘ฆ) ยท 1) = (i ยท (๐‘ฆ ยท 1)))
144, 13syl 17 . . . . . . 7 (๐‘ฆ โˆˆ โ„ โ†’ ((i ยท ๐‘ฆ) ยท 1) = (i ยท (๐‘ฆ ยท 1)))
15 ax-1rid 11128 . . . . . . . 8 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ฆ ยท 1) = ๐‘ฆ)
1615oveq2d 7378 . . . . . . 7 (๐‘ฆ โˆˆ โ„ โ†’ (i ยท (๐‘ฆ ยท 1)) = (i ยท ๐‘ฆ))
1714, 16eqtrd 2777 . . . . . 6 (๐‘ฆ โˆˆ โ„ โ†’ ((i ยท ๐‘ฆ) ยท 1) = (i ยท ๐‘ฆ))
1811, 17oveqan12d 7381 . . . . 5 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ ((๐‘ฅ ยท 1) + ((i ยท ๐‘ฆ) ยท 1)) = (๐‘ฅ + (i ยท ๐‘ฆ)))
1910, 18eqtrd 2777 . . . 4 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1) = (๐‘ฅ + (i ยท ๐‘ฆ)))
20 oveq1 7369 . . . . 5 (๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (๐ด ยท 1) = ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1))
21 id 22 . . . . 5 (๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)))
2220, 21eqeq12d 2753 . . . 4 (๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ ((๐ด ยท 1) = ๐ด โ†” ((๐‘ฅ + (i ยท ๐‘ฆ)) ยท 1) = (๐‘ฅ + (i ยท ๐‘ฆ))))
2319, 22syl5ibrcom 247 . . 3 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (๐ด ยท 1) = ๐ด))
2423rexlimivv 3197 . 2 (โˆƒ๐‘ฅ โˆˆ โ„ โˆƒ๐‘ฆ โˆˆ โ„ ๐ด = (๐‘ฅ + (i ยท ๐‘ฆ)) โ†’ (๐ด ยท 1) = ๐ด)
251, 24syl 17 1 (๐ด โˆˆ โ„‚ โ†’ (๐ด ยท 1) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  โˆƒwrex 3074  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  1c1 11059  ici 11060   + caddc 11061   ยท cmul 11063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-mulcl 11120  ax-mulcom 11122  ax-mulass 11124  ax-distr 11125  ax-1rid 11128  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365
This theorem is referenced by:  mulid2  11161  mulid1i  11166  mulid1d  11179  muleqadd  11806  divdiv1  11873  conjmul  11879  expmul  14020  binom21  14129  binom2sub1  14131  sq01  14135  bernneq  14139  hashiun  15714  fprodcvg  15820  prodmolem2a  15824  efexp  15990  cncrng  20834  cnfld1  20838  0dgr  25622  ecxp  26044  dvcxp1  26109  dvcncxp1  26112  efrlim  26335  lgsdilem2  26697  axcontlem7  27961  ipasslem2  29816  addltmulALT  31430  0dp2dp  31807  zrhnm  32590  2even  46305
  Copyright terms: Public domain W3C validator