Theorem mul01i 11366

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	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
mul01i	⊢ (𝐴 · 0) = 0

Proof of Theorem mul01i

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		mul01 11355	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 0) = 0

Syntax hints:   = wceq 1559   ∈ wcel 2141  (class class class)co 7390  ℂcc 11064  0cc0 11066   · cmul 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-ltxr 11214

This theorem is referenced by:  ine0  11615  msqge0  11701  recextlem2  11811  eqneg  11904  crne0  12181  2t0e0  12381  it0e0  12437  num0h  12693  discr  14246  sin4lt0  16217  demoivreALT  16223  5ndvds3  16437  gcdaddmlem  16548  bezout  16567  139prm  17150  317prm  17152  631prm  17153  1259lem4  17160  2503lem1  17163  2503lem2  17164  4001lem1  17167  4001lem2  17168  4001lem3  17169  4001lem4  17170  odadd1  19878  minveclem7  25484  itg1addlem4  25748  aalioulem3  26385  dcubic  26898  log2ublem3  27000  basellem7  27138  basellem9  27140  lgsdir2  27381  selberg2lem  27601  logdivbnd  27607  pntrsumo1  27616  pntrlog2bndlem5  27632  axpaschlem  29097  axlowdimlem6  29104  nmblolbii  30958  siilem1  31010  minvecolem7  31042  eigorthi  31996  nmbdoplbi  32183  nmcoplbi  32187  nmbdfnlbi  32208  nmcfnlbi  32211  nmopcoi  32254  itgexpif  34860  hgt750lem2  34906  subfacval2  35497  areacirc  38172  60lcm7e420  42587  3lexlogpow5ineq1  42631  sqn5i  42854  139prmALT  48165