Theorem mul02d 11547

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237  0cc0 11239   · cmul 11244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-ltxr 11387

This theorem is used by:  mulneg1  11791  mulge0  11874  mul0or  11996  prodgt0  12204  un0mulcl  12680  mul2lt0rgt0  13265  mul2lt0bi  13268  lincmb01cmp  13666  iccf1o  13667  discr1  14424  discr  14425  hashxplem  14619  cshweqrep  15014  sgnmul  15303  remul2  15340  immul2  15347  indsum  16039  binomlem  16042  geomulcvg  16089  ntrivcvgfvn0  16112  fprodeq0  16186  fprodeq0g  16205  0fallfac  16247  binomfallfaclem2  16250  efne0d  16307  efne0OLD  16309  dvds0  16485  pwp1fsum  16605  smumullem  16706  mulgcd  16765  bezoutr1  16788  lcmgcd  16826  qnumgt0  16970  pcexp  17081  vdwapun  17196  vdwlem1  17203  mulgnn0ass  19370  odmulg  19821  torsubg  20119  isabvd  21120  nn0srg  21797  rge0srg  21798  prmirredlem  21833  pzriprnglem8  21849  nmo0  25109  nmoeq0  25110  blcvx  25172  reparphti  25373  pcorevlem  25402  ipcau2  25610  rrxcph  25768  itg1addlem4  26075  itg1addlem5  26076  itg1mulc  26080  itg2mulc  26123  dvcmul  26319  dvmptcmul  26339  dvexp3  26353  dvef  26355  dveq0  26375  dv11cn  26376  ply1termlem  26576  plyeq0lem  26584  plypf1  26586  plyaddlem1  26587  plymullem1  26588  coeeulem  26598  coeidlem  26611  coeid3  26614  coemullem  26624  coemulhi  26628  coemulc  26629  dgrco  26649  plymul02  26656  plyn0mulidp  26657  vieta1lem2  26689  elqaalem2  26700  aalioulem3  26718  taylthlem2  26758  abelthlem6  26820  pilem2  26836  sinhalfpip  26878  sinhalfpim  26879  coshalfpip  26880  coshalfpim  26881  logtayl  27045  mulcxp  27070  cxpmul2  27074  cxpeq  27142  chordthmlem5  27221  cubic  27234  atans2  27316  atantayl2  27323  leibpi  27327  efrlim  27354  scvxcvx  27370  amgm  27375  ftalem5  27461  basellem2  27466  mumul  27565  muinv  27577  dchrn0  27634  dchrinvcl  27637  lgsdirnn0  27728  lgsdinn0  27729  lgsquad2lem2  27769  rpvmasumlem  27871  dchrisum0flblem1  27892  rpvmasum2  27896  ostth2lem2  28018  brbtwn2  29540  axsegconlem1  29552  axpaschlem  29575  axcontlem7  29605  axcontlem8  29606  elntg2  29620  nvz0  31327  ipasslem1  31490  hi01  31755  fprodeq02  33511  indsumin  33524  constrrtcc  34478  constrsslem  34484  constrremulcl  34510  2sqr3minply  34523  cos9thpiminplylem2  34526  xrge0iifhom  34680  eulerpartlemsv2  35101  eulerpartlems  35103  eulerpartlemsv3  35104  eulerpartlemgc  35105  eulerpartlemv  35107  eulerpartlemgs2  35123  itgexpif  35346  breprexplemc  35372  breprexp  35373  logdivsqrle  35390  subfacp1lem6  36158  cvxpconn  36215  cvxsconn  36216  fwddifnp1  37145  lcmineqlem10  43354  deg1pow  43457  pell1234qrne0  44126  jm2.19lem3  44264  jm2.25  44272  flcidc  44433  relexpmulg  44971  radcnvrat  45559  dvconstbi  45579  binomcxplemnn0  45594  sineq0ALT  46179  fperiodmullem  46592  fprod0  46881  dvsinax  47196  dvasinbx  47203  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  dvnmul  47226  itgsinexplem1  47237  dirkertrigeqlem2  47382  fourierdlem42  47432  fourierdlem83  47472  sqwvfoura  47511  fouriersw  47514  elaa2lem  47516  etransclem15  47532  etransclem24  47541  etransclem35  47552  etransclem46  47563  sigarcol  48147  sharhght  48148  modlt0b  48712  fmtnofac2  48927  zellaz  49729  rrx2linest  50185  line2x  50197  line2y  50198  itschlc0yqe  50203  itschlc0xyqsol1  50209  itschlc0xyqsol  50210  2itscp  50224  aacllem  51367