Theorem mul02d 11408

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
mul02d	⊢ (𝜑 → (0 · 𝐴) = 0)

Proof of Theorem mul02d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mul02 11388	. 2 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 · 𝐴) = 0)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  0cc0 11106   · cmul 11111

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 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  mulneg1  11646  mulge0  11728  mul0or  11850  prodgt0  12057  un0mulcl  12502  mul2lt0rgt0  13073  mul2lt0bi  13076  lincmb01cmp  13468  iccf1o  13469  discr1  14198  discr  14199  hashxplem  14389  cshweqrep  14767  remul2  15073  immul2  15080  binomlem  15771  geomulcvg  15818  ntrivcvgfvn0  15841  fprodeq0  15915  fprodeq0g  15934  0fallfac  15977  binomfallfaclem2  15980  efne0  16036  dvds0  16211  pwp1fsum  16330  smumullem  16429  mulgcd  16486  bezoutr1  16502  lcmgcd  16540  qnumgt0  16682  pcexp  16788  vdwapun  16903  vdwlem1  16910  mulgnn0ass  18984  odmulg  19418  torsubg  19716  isabvd  20420  nn0srg  21007  rge0srg  21008  prmirredlem  21033  nmo0  24243  nmoeq0  24244  blcvx  24305  reparphti  24504  pcorevlem  24533  ipcau2  24742  rrxcph  24900  itg1addlem4  25207  itg1addlem4OLD  25208  itg1addlem5  25209  itg1mulc  25213  itg2mulc  25256  dvcmul  25452  dvmptcmul  25472  dvexp3  25486  dvef  25488  dveq0  25508  dv11cn  25509  ply1termlem  25708  plyeq0lem  25715  plypf1  25717  plyaddlem1  25718  plymullem1  25719  coeeulem  25729  coeidlem  25742  coeid3  25745  coemullem  25755  coemulhi  25759  coemulc  25760  dgrco  25780  vieta1lem2  25815  elqaalem2  25824  aalioulem3  25838  taylthlem2  25877  abelthlem6  25939  pilem2  25955  sinhalfpip  25993  sinhalfpim  25994  coshalfpip  25995  coshalfpim  25996  logtayl  26159  mulcxp  26184  cxpmul2  26188  cxpeq  26254  chordthmlem5  26330  cubic  26343  atans2  26425  atantayl2  26432  leibpi  26436  efrlim  26463  scvxcvx  26479  amgm  26484  ftalem5  26570  basellem2  26575  mumul  26674  muinv  26686  dchrn0  26742  dchrinvcl  26745  lgsdirnn0  26836  lgsdinn0  26837  lgsquad2lem2  26877  rpvmasumlem  26979  dchrisum0flblem1  27000  rpvmasum2  27004  ostth2lem2  27126  brbtwn2  28152  axsegconlem1  28164  axpaschlem  28187  axcontlem7  28217  axcontlem8  28218  elntg2  28232  nvz0  29908  ipasslem1  30071  hi01  30336  fprodeq02  32016  xrge0iifhom  32905  indsum  33007  indsumin  33008  eulerpartlemsv2  33345  eulerpartlems  33347  eulerpartlemsv3  33348  eulerpartlemgc  33349  eulerpartlemv  33351  eulerpartlemgs2  33367  sgnmul  33529  plymul02  33545  plymulx0  33546  itgexpif  33606  breprexplemc  33632  breprexp  33633  logdivsqrle  33650  subfacp1lem6  34164  cvxpconn  34221  cvxsconn  34222  fwddifnp1  35125  gg-reparphti  35160  lcmineqlem10  40891  pell1234qrne0  41576  jm2.19lem3  41715  jm2.25  41723  flcidc  41901  relexpmulg  42446  radcnvrat  43058  dvconstbi  43078  binomcxplemnn0  43093  sineq0ALT  43683  fperiodmullem  43999  fprod0  44298  dvsinax  44615  dvasinbx  44622  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnxpaek  44644  dvnmul  44645  itgsinexplem1  44656  dirkertrigeqlem2  44801  fourierdlem42  44851  fourierdlem83  44891  sqwvfoura  44930  fouriersw  44933  elaa2lem  44935  etransclem15  44951  etransclem24  44960  etransclem35  44971  etransclem46  44982  sigarcol  45566  sharhght  45567  fmtnofac2  46223  rrx2linest  47381  line2x  47393  line2y  47394  itschlc0yqe  47399  itschlc0xyqsol1  47405  itschlc0xyqsol  47406  2itscp  47420  aacllem  47801