MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul01i Unicode version

Theorem mul01i 8999
Description: Multiplication by  0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
Hypothesis
Ref Expression
mul.1  |-  A  e.  CC
Assertion
Ref Expression
mul01i  |-  ( A  x.  0 )  =  0

Proof of Theorem mul01i
StepHypRef Expression
1 mul.1 . 2  |-  A  e.  CC
2 mul01 8988 . 2  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
31, 2ax-mp 10 1  |-  ( A  x.  0 )  =  0
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1687  (class class class)co 5821   CCcc 8732   0cc0 8734    x. cmul 8739
This theorem is referenced by:  ine0  9212  msqge0  9292  recextlem2  9396  eqneg  9477  crne0  9736  num0h  10131  expmulnbnd  11229  discr  11234  reim0  11599  reim0b  11600  rereb  11601  abs1m  11815  iseraltlem2  12151  cos0  12426  sin4lt0  12471  demoivreALT  12477  gcdaddmlem  12703  bezout  12717  139prm  13121  317prm  13123  631prm  13124  1259lem4  13128  1259lem5  13129  2503lem1  13131  2503lem2  13132  4001lem1  13135  4001lem2  13136  4001lem3  13137  4001lem4  13138  odadd1  15136  htpycc  18474  pco0  18508  pcohtpylem  18513  pcopt2  18517  pcoass  18518  pcorevlem  18520  minveclem7  18795  itg1addlem4  19050  itgrevallem1  19145  aalioulem3  19710  pilem2  19824  cospi  19836  efipi  19837  sin2pi  19839  ef2pi  19841  pige3  19881  tanarg  19966  pythag  20111  dcubic  20138  atantayl2  20230  log2ublem3  20240  basellem7  20320  basellem9  20322  bclbnd  20515  bposlem1  20519  bposlem2  20520  lgsdir2  20563  lgsquadlem1  20589  lgsquadlem2  20590  log2sumbnd  20689  selberg2lem  20695  logdivbnd  20701  pntrsumo1  20710  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  ipidsq  21280  dip0r  21287  nmblolbii  21371  siilem1  21423  minvecolem7  21456  eigorthi  22411  lnopeq0i  22581  nmbdoplbi  22598  nmcoplbi  22602  nmbdfnlbi  22623  nmcfnlbi  22626  nmopcoi  22669  cdj3lem1  23008  subfacval2  23124  axpaschlem  23977  axlowdimlem6  23984  fsumcube  24204  m1expeven  27126
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-mpt 4082  df-id 4310  df-po 4315  df-so 4316  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-ov 5824  df-er 6657  df-en 6861  df-dom 6862  df-sdom 6863  df-pnf 8866  df-mnf 8867  df-ltxr 8869
  Copyright terms: Public domain W3C validator