Theorem mul02d 11378

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072  0cc0 11074   · cmul 11079

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-ov 7392  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-ltxr 11219

This theorem is referenced by:  mulneg1  11620  mulge0  11702  mul0or  11824  prodgt0  12035  un0mulcl  12482  mul2lt0rgt0  13062  mul2lt0bi  13065  lincmb01cmp  13462  iccf1o  13463  discr1  14210  discr  14211  hashxplem  14404  cshweqrep  14792  remul2  15102  immul2  15109  binomlem  15801  geomulcvg  15848  ntrivcvgfvn0  15871  fprodeq0  15947  fprodeq0g  15966  0fallfac  16009  binomfallfaclem2  16012  efne0d  16069  efne0OLD  16071  dvds0  16247  pwp1fsum  16367  smumullem  16468  mulgcd  16524  bezoutr1  16545  lcmgcd  16583  qnumgt0  16726  pcexp  16836  vdwapun  16951  vdwlem1  16958  mulgnn0ass  19048  odmulg  19492  torsubg  19790  isabvd  20727  nn0srg  21360  rge0srg  21361  prmirredlem  21388  pzriprnglem8  21404  nmo0  24629  nmoeq0  24630  blcvx  24692  reparphti  24902  reparphtiOLD  24903  pcorevlem  24932  ipcau2  25140  rrxcph  25298  itg1addlem4  25606  itg1addlem5  25607  itg1mulc  25611  itg2mulc  25654  dvcmul  25853  dvmptcmul  25874  dvexp3  25888  dvef  25890  dveq0  25911  dv11cn  25912  ply1termlem  26114  plyeq0lem  26121  plypf1  26123  plyaddlem1  26124  plymullem1  26125  coeeulem  26135  coeidlem  26148  coeid3  26151  coemullem  26161  coemulhi  26165  coemulc  26166  dgrco  26187  vieta1lem2  26225  elqaalem2  26234  aalioulem3  26248  taylthlem2  26288  taylthlem2OLD  26289  abelthlem6  26352  pilem2  26368  sinhalfpip  26407  sinhalfpim  26408  coshalfpip  26409  coshalfpim  26410  logtayl  26575  mulcxp  26600  cxpmul2  26604  cxpeq  26673  chordthmlem5  26752  cubic  26765  atans2  26847  atantayl2  26854  leibpi  26858  efrlim  26885  efrlimOLD  26886  scvxcvx  26902  amgm  26907  ftalem5  26993  basellem2  26998  mumul  27097  muinv  27109  dchrn0  27167  dchrinvcl  27170  lgsdirnn0  27261  lgsdinn0  27262  lgsquad2lem2  27302  rpvmasumlem  27404  dchrisum0flblem1  27425  rpvmasum2  27429  ostth2lem2  27551  brbtwn2  28838  axsegconlem1  28850  axpaschlem  28873  axcontlem7  28903  axcontlem8  28904  elntg2  28918  nvz0  30603  ipasslem1  30766  hi01  31031  fprodeq02  32754  sgnmul  32766  indsum  32790  indsumin  32791  constrrtcc  33731  constrsslem  33737  constrremulcl  33763  2sqr3minply  33776  cos9thpiminplylem2  33779  xrge0iifhom  33933  eulerpartlemsv2  34355  eulerpartlems  34357  eulerpartlemsv3  34358  eulerpartlemgc  34359  eulerpartlemv  34361  eulerpartlemgs2  34377  plymul02  34543  plymulx0  34544  itgexpif  34603  breprexplemc  34629  breprexp  34630  logdivsqrle  34647  subfacp1lem6  35172  cvxpconn  35229  cvxsconn  35230  fwddifnp1  36148  lcmineqlem10  42021  deg1pow  42124  pell1234qrne0  42834  jm2.19lem3  42973  jm2.25  42981  flcidc  43152  relexpmulg  43692  radcnvrat  44296  dvconstbi  44316  binomcxplemnn0  44331  sineq0ALT  44919  fperiodmullem  45294  fprod0  45587  dvsinax  45904  dvasinbx  45911  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnxpaek  45933  dvnmul  45934  itgsinexplem1  45945  dirkertrigeqlem2  46090  fourierdlem42  46140  fourierdlem83  46180  sqwvfoura  46219  fouriersw  46222  elaa2lem  46224  etransclem15  46240  etransclem24  46249  etransclem35  46260  etransclem46  46271  sigarcol  46855  sharhght  46856  modlt0b  47354  fmtnofac2  47560  rrx2linest  48721  line2x  48733  line2y  48734  itschlc0yqe  48739  itschlc0xyqsol1  48745  itschlc0xyqsol  48746  2itscp  48760  aacllem  49780