Theorem mul01d 10235

Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mul01d	|- ( ph -> ( A x. 0 ) = 0 )

Proof of Theorem mul01d

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		mul01 10215	. 2 |- ( A e. CC -> ( A x. 0 ) = 0 )
3	1, 2	syl 17	1 |- ( ph -> ( A x. 0 ) = 0 )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   0cc0 9936   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079

This theorem is referenced by:  mulge0  10546  mul0or  10667  diveq0  10695  div0  10715  lemul1a  10877  un0mulcl  11327  mul2lt0bi  11936  rexmul  12101  modid  12695  addmodlteq  12745  expmul  12905  sqlecan  12971  discr  13001  hashf1lem2  13240  hashf1  13241  fsummulc2  14516  geolim  14601  geomulcvg  14607  fprodeq0  14705  0risefac  14769  0dvds  15002  smumullem  15214  bezoutlem1  15256  lcmgcd  15320  mulgcddvds  15369  cncongr2  15382  prmdiv  15490  pcaddlem  15592  qexpz  15605  prmreclem4  15623  prmreclem5  15624  mulgnn0ass  17578  odadd2  18252  isabvd  18820  nn0srg  19816  rge0srg  19817  nmolb2d  22522  nmoleub  22535  reparphti  22797  pcorevlem  22826  itg1val2  23451  i1fmullem  23461  itg1addlem4  23466  itg10a  23477  itg1ge0a  23478  itg2const  23507  itg2monolem1  23517  itg0  23546  itgz  23547  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  dvcnp2  23683  dvcobr  23709  dvlip  23756  dvlipcn  23757  c1lip1  23760  dvlt0  23768  plymullem1  23970  coefv0  24004  coemullem  24006  coemulhi  24010  dgrmulc  24027  dgrcolem2  24030  dvply1  24039  plydivlem3  24050  elqaalem2  24075  elqaalem3  24076  tayl0  24116  dvtaylp  24124  radcnv0  24170  dvradcnv  24175  pserdvlem2  24182  abelthlem2  24186  pilem2  24206  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  tanregt0  24285  efsubm  24297  argregt0  24356  argrege0  24357  argimgt0  24358  logtayl  24406  mulcxplem  24430  mulcxp  24431  cxpmul2  24435  pythag  24547  quad2  24566  dcubic  24573  atans2  24658  zetacvg  24741  lgamgulmlem2  24756  mumul  24907  logexprlim  24950  dchrsum2  24993  sumdchr2  24995  lgsdilem  25049  lgsdirnn0  25069  lgsdinn0  25070  lgsquad3  25112  rpvmasumlem  25176  dchrisumlem1  25178  dchrvmasumiflem2  25191  rpvmasum2  25201  dchrisum0re  25202  pntrlog2bndlem4  25269  pntlemf  25294  pntleml  25300  ostth2lem2  25323  ostth3  25327  colinearalg  25790  nmlnoubi  27651  ipasslem2  27687  cdj3lem1  29293  2sqmod  29648  xrge0iifhom  29983  sgnmul  30604  signsplypnf  30627  signswch  30638  signlem0  30664  itgexpif  30684  circlemeth  30718  knoppndvlem6  32508  knoppndvlem8  32510  knoppndvlem13  32515  ovoliunnfl  33451  voliunnfl  33453  itg2addnclem  33461  iblmulc2nc  33475  itgmulc2nclem1  33476  areacirc  33505  geomcau  33555  bfp  33623  irrapxlem1  37386  pell1qr1  37435  pell1qrgaplem  37437  rmxy0  37488  jm2.18  37555  mpaaeu  37720  relexpmulg  38002  binomcxplemnotnn0  38555  xralrple2  39570  stoweidlem26  40243  stoweidlem37  40254  stirlinglem7  40297  dirkercncflem2  40321  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  sqwvfourb  40446  etransclem15  40466  etransclem24  40475  etransclem25  40476  etransclem32  40483  etransclem35  40486  etransclem48  40499  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  sharhght  41054  pwdif  41501  altgsumbcALT  42131  dig0  42400