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

Theorem mul01d 11353
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mul01d (𝜑 → (𝐴 · 0) = 0)

Proof of Theorem mul01d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mul01 11333 . 2 (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
31, 2syl 17 1 (𝜑 → (𝐴 · 0) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  (class class class)co 7356  cc 11048  0cc0 11050   · cmul 11055
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7359  df-er 8647  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11190  df-mnf 11191  df-ltxr 11193
This theorem is referenced by:  mulge0  11672  mul0or  11794  diveq0  11822  div0  11842  lemul1a  12008  un0mulcl  12446  mul2lt0bi  13020  rexmul  13189  modid  13800  addmodlteq  13850  expmul  14012  sqlecan  14112  discr  14142  hashf1lem2  14354  hashf1  14355  fsummulc2  15668  pwdif  15752  geolim  15754  geomulcvg  15760  fprodeq0  15857  0risefac  15920  0dvds  16158  smumullem  16371  bezoutlem1  16419  lcmgcd  16482  mulgcddvds  16530  cncongr2  16543  prmdiv  16656  pcaddlem  16759  qexpz  16772  prmreclem4  16790  prmreclem5  16791  mulgnn0ass  18910  odadd2  19625  isabvd  20277  nn0srg  20865  rge0srg  20866  mhppwdeg  21538  nmolb2d  24080  nmoleub  24093  reparphti  24358  pcorevlem  24387  itg1val2  25046  i1fmullem  25056  itg1addlem4  25061  itg1addlem4OLD  25062  itg10a  25073  itg1ge0a  25074  itg2const  25103  itg2monolem1  25113  itg0  25142  itgz  25143  iblmulc2  25193  itgmulc2lem1  25194  bddmulibl  25201  dvcnp2  25282  dvcobr  25308  dvlip  25355  dvlipcn  25356  c1lip1  25359  dvlt0  25367  plymullem1  25573  coefv0  25607  coemullem  25609  coemulhi  25613  dgrmulc  25630  dgrcolem2  25633  dvply1  25642  plydivlem3  25653  elqaalem2  25678  elqaalem3  25679  tayl0  25719  dvtaylp  25727  radcnv0  25773  dvradcnv  25778  pserdvlem2  25785  abelthlem2  25789  pilem2  25809  sinmpi  25842  cosmpi  25843  sinppi  25844  cosppi  25845  tanregt0  25893  efsubm  25905  argregt0  25963  argrege0  25964  argimgt0  25965  logtayl  26013  mulcxplem  26037  mulcxp  26038  cxpmul2  26042  pythag  26165  quad2  26187  dcubic  26194  atans2  26279  zetacvg  26362  lgamgulmlem2  26377  mumul  26528  logexprlim  26571  dchrsum2  26614  sumdchr2  26616  lgsdilem  26670  lgsdirnn0  26690  lgsdinn0  26691  lgsquad3  26733  2sqmod  26782  rpvmasumlem  26833  dchrisumlem1  26835  dchrvmasumiflem2  26848  rpvmasum2  26858  dchrisum0re  26859  pntrlog2bndlem4  26926  pntlemf  26951  pntleml  26957  ostth2lem2  26980  ostth3  26984  colinearalg  27806  nmlnoubi  29685  ipasslem2  29721  cdj3lem1  31323  xrge0iifhom  32458  sgnmul  33082  signsplypnf  33102  signswch  33113  signlem0  33139  itgexpif  33159  circlemeth  33193  knoppndvlem6  34970  knoppndvlem8  34972  knoppndvlem13  34977  ovoliunnfl  36110  voliunnfl  36112  itg2addnclem  36119  iblmulc2nc  36133  itgmulc2nclem1  36134  areacirc  36161  geomcau  36208  bfp  36273  lcmineqlem10  40485  lcmineqlem12  40487  irrapxlem1  41122  pell1qr1  41171  pell1qrgaplem  41173  rmxy0  41224  jm2.18  41289  mpaaeu  41454  relexpmulg  41963  binomcxplemnotnn0  42617  xralrple2  43563  stoweidlem26  44238  stoweidlem37  44249  stirlinglem7  44292  dirkercncflem2  44316  fourierdlem103  44421  fourierdlem104  44422  sqwvfoura  44440  sqwvfourb  44441  etransclem15  44461  etransclem24  44470  etransclem25  44471  etransclem32  44478  etransclem35  44481  etransclem48  44494  hoidmvlelem1  44807  hoidmvlelem2  44808  hoidmvlelem3  44809  sharhght  45077  altgsumbcALT  46400  dig0  46663  itcovalpclem1  46727  line2ylem  46808  line2xlem  46810  2itscp  46838
  Copyright terms: Public domain W3C validator