Theorem mul02d 11342

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 11322	. 2 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 · 𝐴) = 0)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  0cc0 11036   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  mulneg1  11584  mulge0  11666  mul0or  11788  prodgt0  12000  un0mulcl  12469  mul2lt0rgt0  13045  mul2lt0bi  13048  lincmb01cmp  13446  iccf1o  13447  discr1  14199  discr  14200  hashxplem  14393  cshweqrep  14781  remul2  15090  immul2  15097  indsum  15789  binomlem  15792  geomulcvg  15839  ntrivcvgfvn0  15862  fprodeq0  15938  fprodeq0g  15957  0fallfac  16000  binomfallfaclem2  16003  efne0d  16060  efne0OLD  16062  dvds0  16238  pwp1fsum  16358  smumullem  16459  mulgcd  16515  bezoutr1  16536  lcmgcd  16574  qnumgt0  16718  pcexp  16828  vdwapun  16943  vdwlem1  16950  mulgnn0ass  19084  odmulg  19529  torsubg  19827  isabvd  20791  nn0srg  21419  rge0srg  21420  prmirredlem  21454  pzriprnglem8  21470  nmo0  24725  nmoeq0  24726  blcvx  24788  reparphti  24989  pcorevlem  25018  ipcau2  25226  rrxcph  25384  itg1addlem4  25691  itg1addlem5  25692  itg1mulc  25696  itg2mulc  25739  dvcmul  25936  dvmptcmul  25956  dvexp3  25970  dvef  25972  dveq0  25992  dv11cn  25993  ply1termlem  26193  plyeq0lem  26200  plypf1  26202  plyaddlem1  26203  plymullem1  26204  coeeulem  26214  coeidlem  26227  coeid3  26230  coemullem  26240  coemulhi  26244  coemulc  26245  dgrco  26265  vieta1lem2  26302  elqaalem2  26311  aalioulem3  26325  taylthlem2  26364  abelthlem6  26426  pilem2  26442  sinhalfpip  26481  sinhalfpim  26482  coshalfpip  26483  coshalfpim  26484  logtayl  26649  mulcxp  26674  cxpmul2  26678  cxpeq  26746  chordthmlem5  26825  cubic  26838  atans2  26920  atantayl2  26927  leibpi  26931  efrlim  26958  scvxcvx  26974  amgm  26979  ftalem5  27065  basellem2  27070  mumul  27169  muinv  27181  dchrn0  27238  dchrinvcl  27241  lgsdirnn0  27332  lgsdinn0  27333  lgsquad2lem2  27373  rpvmasumlem  27475  dchrisum0flblem1  27496  rpvmasum2  27500  ostth2lem2  27622  brbtwn2  28999  axsegconlem1  29011  axpaschlem  29034  axcontlem7  29064  axcontlem8  29065  elntg2  29079  nvz0  30764  ipasslem1  30927  hi01  31192  fprodeq02  32923  sgnmul  32934  indsumin  32947  constrrtcc  33926  constrsslem  33932  constrremulcl  33958  2sqr3minply  33971  cos9thpiminplylem2  33974  xrge0iifhom  34128  eulerpartlemsv2  34549  eulerpartlems  34551  eulerpartlemsv3  34552  eulerpartlemgc  34553  eulerpartlemv  34555  eulerpartlemgs2  34571  plymul02  34737  plymulx0  34738  itgexpif  34797  breprexplemc  34823  breprexp  34824  logdivsqrle  34841  subfacp1lem6  35420  cvxpconn  35477  cvxsconn  35478  fwddifnp1  36400  lcmineqlem10  42530  deg1pow  42633  pell1234qrne0  43305  jm2.19lem3  43443  jm2.25  43451  flcidc  43622  relexpmulg  44161  radcnvrat  44765  dvconstbi  44785  binomcxplemnn0  44800  sineq0ALT  45387  fperiodmullem  45758  fprod0  46048  dvsinax  46363  dvasinbx  46370  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  dvnmul  46393  itgsinexplem1  46404  dirkertrigeqlem2  46549  fourierdlem42  46599  fourierdlem83  46639  sqwvfoura  46678  fouriersw  46681  elaa2lem  46683  etransclem15  46699  etransclem24  46708  etransclem35  46719  etransclem46  46730  sigarcol  47314  sharhght  47315  modlt0b  47839  fmtnofac2  48054  rrx2linest  49240  line2x  49252  line2y  49253  itschlc0yqe  49258  itschlc0xyqsol1  49264  itschlc0xyqsol  49265  2itscp  49279  aacllem  50298