Theorem mul02d 11173

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  0cc0 10871   · cmul 10876

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-ltxr 11014

This theorem is referenced by:  mulneg1  11411  mulge0  11493  mul0or  11615  prodgt0  11822  un0mulcl  12267  mul2lt0rgt0  12833  mul2lt0bi  12836  lincmb01cmp  13227  iccf1o  13228  discr1  13954  discr  13955  hashxplem  14148  cshweqrep  14534  remul2  14841  immul2  14848  binomlem  15541  geomulcvg  15588  ntrivcvgfvn0  15611  fprodeq0  15685  fprodeq0g  15704  0fallfac  15747  binomfallfaclem2  15750  efne0  15806  dvds0  15981  pwp1fsum  16100  smumullem  16199  mulgcd  16256  bezoutr1  16274  lcmgcd  16312  qnumgt0  16454  pcexp  16560  vdwapun  16675  vdwlem1  16682  mulgnn0ass  18739  odmulg  19163  torsubg  19455  isabvd  20080  nn0srg  20668  rge0srg  20669  prmirredlem  20694  nmo0  23899  nmoeq0  23900  blcvx  23961  reparphti  24160  pcorevlem  24189  ipcau2  24398  rrxcph  24556  itg1addlem4  24863  itg1addlem4OLD  24864  itg1addlem5  24865  itg1mulc  24869  itg2mulc  24912  dvcmul  25108  dvmptcmul  25128  dvexp3  25142  dvef  25144  dveq0  25164  dv11cn  25165  ply1termlem  25364  plyeq0lem  25371  plypf1  25373  plyaddlem1  25374  plymullem1  25375  coeeulem  25385  coeidlem  25398  coeid3  25401  coemullem  25411  coemulhi  25415  coemulc  25416  dgrco  25436  vieta1lem2  25471  elqaalem2  25480  aalioulem3  25494  taylthlem2  25533  abelthlem6  25595  pilem2  25611  sinhalfpip  25649  sinhalfpim  25650  coshalfpip  25651  coshalfpim  25652  logtayl  25815  mulcxp  25840  cxpmul2  25844  cxpeq  25910  chordthmlem5  25986  cubic  25999  atans2  26081  atantayl2  26088  leibpi  26092  efrlim  26119  scvxcvx  26135  amgm  26140  ftalem5  26226  basellem2  26231  mumul  26330  muinv  26342  dchrn0  26398  dchrinvcl  26401  lgsdirnn0  26492  lgsdinn0  26493  lgsquad2lem2  26533  rpvmasumlem  26635  dchrisum0flblem1  26656  rpvmasum2  26660  ostth2lem2  26782  brbtwn2  27273  axsegconlem1  27285  axpaschlem  27308  axcontlem7  27338  axcontlem8  27339  elntg2  27353  nvz0  29030  ipasslem1  29193  hi01  29458  fprodeq02  31137  xrge0iifhom  31887  indsum  31989  indsumin  31990  eulerpartlemsv2  32325  eulerpartlems  32327  eulerpartlemsv3  32328  eulerpartlemgc  32329  eulerpartlemv  32331  eulerpartlemgs2  32347  sgnmul  32509  plymul02  32525  plymulx0  32526  itgexpif  32586  breprexplemc  32612  breprexp  32613  logdivsqrle  32630  subfacp1lem6  33147  cvxpconn  33204  cvxsconn  33205  fwddifnp1  34467  lcmineqlem10  40046  pell1234qrne0  40675  jm2.19lem3  40813  jm2.25  40821  flcidc  40999  relexpmulg  41318  radcnvrat  41932  dvconstbi  41952  binomcxplemnn0  41967  sineq0ALT  42557  fperiodmullem  42842  fprod0  43137  dvsinax  43454  dvasinbx  43461  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  dvnxpaek  43483  dvnmul  43484  itgsinexplem1  43495  dirkertrigeqlem2  43640  fourierdlem42  43690  fourierdlem83  43730  sqwvfoura  43769  fouriersw  43772  elaa2lem  43774  etransclem15  43790  etransclem24  43799  etransclem35  43810  etransclem46  43821  sigarcol  44380  sharhght  44381  fmtnofac2  45021  rrx2linest  46088  line2x  46100  line2y  46101  itschlc0yqe  46106  itschlc0xyqsol1  46112  itschlc0xyqsol  46113  2itscp  46127  aacllem  46505