Theorem mulridi 11243

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mulridi	⊢ (𝐴 · 1) = 𝐴

Proof of Theorem mulridi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mulrid 11237	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 1) = 𝐴

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7415  ℂcc 11131  1c1 11134   · cmul 11138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-mulcl 11195  ax-mulcom 11197  ax-mulass 11199  ax-distr 11200  ax-1rid 11203  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418

This theorem is referenced by:  addrid  11419  0lt1  11761  muleqadd  11883  1t1e1  12399  2t1e2  12400  3t1e3  12402  halfpm6th  12458  9p1e10  12704  numltc  12728  numsucc  12742  dec10p  12745  numadd  12749  numaddc  12750  11multnc  12770  4t3lem  12799  5t2e10  12802  9t11e99  12832  nn0opthlem1  14254  faclbnd4lem1  14279  rei  15130  imi  15131  cji  15133  sqrtm1  15249  0.999...  15854  efival  16123  ef01bndlem  16155  3lcm2e6  16698  decsplit0b  17043  2exp8  17052  37prm  17084  43prm  17085  83prm  17086  139prm  17087  163prm  17088  317prm  17089  1259lem1  17094  1259lem2  17095  1259lem3  17096  1259lem4  17097  1259lem5  17098  2503lem1  17100  2503lem2  17101  2503prm  17103  4001lem1  17104  4001lem2  17105  4001lem3  17106  cnmsgnsubg  21503  mdetralt  22504  dveflem  25905  dvsincos  25907  efhalfpi  26400  pige3ALT  26448  cosne0  26457  efif1olem4  26473  logf1o2  26578  asin1  26820  dvatan  26861  log2ublem3  26874  log2ub  26875  birthday  26880  basellem9  27015  ppiub  27131  chtub  27139  bposlem8  27218  lgsdir2  27257  mulog2sumlem2  27462  pntlemb  27524  avril1  30267  ipidsq  30514  nmopadjlem  31893  nmopcoadji  31905  unierri  31908  sgnmul  34157  signswch  34188  itgexpif  34233  reprlt  34246  breprexp  34260  hgt750lem  34278  hgt750lem2  34279  circum  35273  dvasin  37172  3lexlogpow5ineq1  41520  3lexlogpow5ineq5  41526  aks4d1p1  41542  235t711  41858  ex-decpmul  41859  it1ei  41868  sqrtcval2  43063  resqrtvalex  43066  imsqrtvalex  43067  inductionexd  43576  xralrple3  44747  wallispi  45449  wallispi2lem2  45451  stirlinglem1  45453  dirkertrigeqlem3  45479  257prm  46892  fmtno4prmfac193  46904  fmtno5fac  46913  139prmALT  46927  127prm  46930  2exp340mod341  47064

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »