Theorem mul01i 11267

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 11256	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 · 0) = 0

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7338  ℂcc 10971  0cc0 10973   · cmul 10978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-po 5533  df-so 5534  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-ov 7341  df-er 8570  df-en 8806  df-dom 8807  df-sdom 8808  df-pnf 11113  df-mnf 11114  df-ltxr 11116

This theorem is referenced by:  ine0  11512  msqge0  11598  recextlem2  11708  eqneg  11797  crne0  12068  2t0e0  12244  it0e0  12297  num0h  12551  discr  14057  sin4lt0  16004  demoivreALT  16010  gcdaddmlem  16331  bezout  16351  139prm  16923  317prm  16925  631prm  16926  1259lem4  16933  2503lem1  16936  2503lem2  16937  4001lem1  16940  4001lem2  16941  4001lem3  16942  4001lem4  16943  odadd1  19545  minveclem7  24706  itg1addlem4  24970  itg1addlem4OLD  24971  aalioulem3  25601  dcubic  26103  log2ublem3  26205  basellem7  26343  basellem9  26345  lgsdir2  26585  selberg2lem  26805  logdivbnd  26811  pntrsumo1  26820  pntrlog2bndlem5  26836  axpaschlem  27598  axlowdimlem6  27605  nmblolbii  29450  siilem1  29502  minvecolem7  29534  eigorthi  30488  nmbdoplbi  30675  nmcoplbi  30679  nmbdfnlbi  30700  nmcfnlbi  30703  nmopcoi  30746  itgexpif  32886  hgt750lem2  32932  subfacval2  33448  areacirc  36026  60lcm7e420  40323  3lexlogpow5ineq1  40367  sqn5i  40624  139prmALT  45466