Theorem mul02d 11431

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  0cc0 11127   · cmul 11132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is referenced by:  mulneg1  11671  mulge0  11753  mul0or  11875  prodgt0  12086  un0mulcl  12533  mul2lt0rgt0  13110  mul2lt0bi  13113  lincmb01cmp  13510  iccf1o  13511  discr1  14255  discr  14256  hashxplem  14449  cshweqrep  14837  remul2  15147  immul2  15154  binomlem  15843  geomulcvg  15890  ntrivcvgfvn0  15913  fprodeq0  15989  fprodeq0g  16008  0fallfac  16051  binomfallfaclem2  16054  efne0d  16111  efne0OLD  16113  dvds0  16289  pwp1fsum  16408  smumullem  16509  mulgcd  16565  bezoutr1  16586  lcmgcd  16624  qnumgt0  16767  pcexp  16877  vdwapun  16992  vdwlem1  16999  mulgnn0ass  19091  odmulg  19535  torsubg  19833  isabvd  20770  nn0srg  21403  rge0srg  21404  prmirredlem  21431  pzriprnglem8  21447  nmo0  24672  nmoeq0  24673  blcvx  24735  reparphti  24945  reparphtiOLD  24946  pcorevlem  24975  ipcau2  25184  rrxcph  25342  itg1addlem4  25650  itg1addlem5  25651  itg1mulc  25655  itg2mulc  25698  dvcmul  25897  dvmptcmul  25918  dvexp3  25932  dvef  25934  dveq0  25955  dv11cn  25956  ply1termlem  26158  plyeq0lem  26165  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  coeid3  26195  coemullem  26205  coemulhi  26209  coemulc  26210  dgrco  26231  vieta1lem2  26269  elqaalem2  26278  aalioulem3  26292  taylthlem2  26332  taylthlem2OLD  26333  abelthlem6  26396  pilem2  26412  sinhalfpip  26451  sinhalfpim  26452  coshalfpip  26453  coshalfpim  26454  logtayl  26619  mulcxp  26644  cxpmul2  26648  cxpeq  26717  chordthmlem5  26796  cubic  26809  atans2  26891  atantayl2  26898  leibpi  26902  efrlim  26929  efrlimOLD  26930  scvxcvx  26946  amgm  26951  ftalem5  27037  basellem2  27042  mumul  27141  muinv  27153  dchrn0  27211  dchrinvcl  27214  lgsdirnn0  27305  lgsdinn0  27306  lgsquad2lem2  27346  rpvmasumlem  27448  dchrisum0flblem1  27469  rpvmasum2  27473  ostth2lem2  27595  brbtwn2  28830  axsegconlem1  28842  axpaschlem  28865  axcontlem7  28895  axcontlem8  28896  elntg2  28910  nvz0  30595  ipasslem1  30758  hi01  31023  fprodeq02  32748  sgnmul  32760  indsum  32784  indsumin  32785  constrrtcc  33715  constrsslem  33721  constrremulcl  33747  2sqr3minply  33760  cos9thpiminplylem2  33763  xrge0iifhom  33914  eulerpartlemsv2  34336  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemgc  34340  eulerpartlemv  34342  eulerpartlemgs2  34358  plymul02  34524  plymulx0  34525  itgexpif  34584  breprexplemc  34610  breprexp  34611  logdivsqrle  34628  subfacp1lem6  35153  cvxpconn  35210  cvxsconn  35211  fwddifnp1  36129  lcmineqlem10  41997  deg1pow  42100  pell1234qrne0  42823  jm2.19lem3  42962  jm2.25  42970  flcidc  43141  relexpmulg  43681  radcnvrat  44286  dvconstbi  44306  binomcxplemnn0  44321  sineq0ALT  44909  fperiodmullem  45280  fprod0  45573  dvsinax  45890  dvasinbx  45897  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnxpaek  45919  dvnmul  45920  itgsinexplem1  45931  dirkertrigeqlem2  46076  fourierdlem42  46126  fourierdlem83  46166  sqwvfoura  46205  fouriersw  46208  elaa2lem  46210  etransclem15  46226  etransclem24  46235  etransclem35  46246  etransclem46  46257  sigarcol  46841  sharhght  46842  fmtnofac2  47531  rrx2linest  48670  line2x  48682  line2y  48683  itschlc0yqe  48688  itschlc0xyqsol1  48694  itschlc0xyqsol  48695  2itscp  48709  aacllem  49613