Theorem mul02d 11432

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122  0cc0 11124   · cmul 11129

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272

This theorem is used by:  mulneg1  11674  mulge0  11756  mul0or  11878  prodgt0  12086  un0mulcl  12562  mul2lt0rgt0  13147  mul2lt0bi  13150  lincmb01cmp  13548  iccf1o  13549  discr1  14303  discr  14304  hashxplem  14498  cshweqrep  14892  sgnmul  15180  remul2  15217  immul2  15224  indsum  15915  binomlem  15918  geomulcvg  15965  ntrivcvgfvn0  15988  fprodeq0  16062  fprodeq0g  16081  0fallfac  16123  binomfallfaclem2  16126  efne0d  16183  efne0OLD  16185  dvds0  16361  pwp1fsum  16481  smumullem  16582  mulgcd  16638  bezoutr1  16659  lcmgcd  16697  qnumgt0  16841  pcexp  16951  vdwapun  17066  vdwlem1  17073  mulgnn0ass  19233  odmulg  19683  torsubg  19981  isabvd  20978  nn0srg  21650  rge0srg  21651  prmirredlem  21685  pzriprnglem8  21701  nmo0  24961  nmoeq0  24962  blcvx  25024  reparphti  25225  pcorevlem  25254  ipcau2  25462  rrxcph  25620  itg1addlem4  25927  itg1addlem5  25928  itg1mulc  25932  itg2mulc  25975  dvcmul  26171  dvmptcmul  26191  dvexp3  26205  dvef  26207  dveq0  26227  dv11cn  26228  ply1termlem  26428  plyeq0lem  26436  plypf1  26438  plyaddlem1  26439  plymullem1  26440  coeeulem  26450  coeidlem  26463  coeid3  26466  coemullem  26476  coemulhi  26480  coemulc  26481  dgrco  26501  plymul02  26510  plyn0mulidp  26511  vieta1lem2  26543  elqaalem2  26552  aalioulem3  26570  taylthlem2  26610  abelthlem6  26672  pilem2  26688  sinhalfpip  26730  sinhalfpim  26731  coshalfpip  26732  coshalfpim  26733  logtayl  26897  mulcxp  26922  cxpmul2  26926  cxpeq  26994  chordthmlem5  27073  cubic  27086  atans2  27168  atantayl2  27175  leibpi  27179  efrlim  27206  scvxcvx  27222  amgm  27227  ftalem5  27313  basellem2  27318  mumul  27417  muinv  27429  dchrn0  27486  dchrinvcl  27489  lgsdirnn0  27580  lgsdinn0  27581  lgsquad2lem2  27621  rpvmasumlem  27723  dchrisum0flblem1  27744  rpvmasum2  27748  ostth2lem2  27870  brbtwn2  29362  axsegconlem1  29374  axpaschlem  29397  axcontlem7  29427  axcontlem8  29428  elntg2  29442  nvz0  31149  ipasslem1  31312  hi01  31577  fprodeq02  33294  indsumin  33307  constrrtcc  34245  constrsslem  34251  constrremulcl  34277  2sqr3minply  34290  cos9thpiminplylem2  34293  xrge0iifhom  34447  eulerpartlemsv2  34869  eulerpartlems  34871  eulerpartlemsv3  34872  eulerpartlemgc  34873  eulerpartlemv  34875  eulerpartlemgs2  34891  itgexpif  35114  breprexplemc  35140  breprexp  35141  logdivsqrle  35158  subfacp1lem6  35764  cvxpconn  35821  cvxsconn  35822  fwddifnp1  36745  lcmineqlem10  42904  deg1pow  43007  pell1234qrne0  43694  jm2.19lem3  43832  jm2.25  43840  flcidc  44011  relexpmulg  44550  radcnvrat  45138  dvconstbi  45158  binomcxplemnn0  45173  sineq0ALT  45759  fperiodmullem  46136  fprod0  46426  dvsinax  46741  dvasinbx  46748  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnmul  46771  itgsinexplem1  46782  dirkertrigeqlem2  46927  fourierdlem42  46977  fourierdlem83  47017  sqwvfoura  47056  fouriersw  47059  elaa2lem  47061  etransclem15  47077  etransclem24  47086  etransclem35  47097  etransclem46  47108  sigarcol  47692  sharhght  47693  modlt0b  48257  fmtnofac2  48472  rrx2linest  49672  line2x  49684  line2y  49685  itschlc0yqe  49690  itschlc0xyqsol1  49696  itschlc0xyqsol  49697  2itscp  49711  aacllem  50772