Theorem mul01d 8507

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

Hypothesis

Ref	Expression
mul01d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mul01d	⊢ (𝜑 → (𝐴 · 0) = 0)

Proof of Theorem mul01d

Step	Hyp	Ref	Expression
1		mul01d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mul01 8503	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 0) = 0)

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   · cmul 7972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-setind 4606  ax-resscn 8059  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-mulcom 8068  ax-addass 8069  ax-distr 8071  ax-i2m1 8072  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-iota 5254  df-fun 5296  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-sub 8287

This theorem is referenced by:  mulap0r  8730  diveqap0  8797  div0ap  8817  mulle0r  9059  un0mulcl  9371  modqid  10538  addmodlteq  10587  expmul  10773  bcval5  10952  fsummulc2  11925  geolim  11988  fprodeq0  12094  0dvds  12288  gcdaddm  12471  bezoutlema  12486  bezoutlemb  12487  lcmgcd  12566  mulgcddvds  12582  cncongr2  12592  prmdiv  12723  pcaddlem  12828  qexpz  12841  mulgnn0ass  13661  dvcnp2cntop  15338  plymullem1  15387  dvply1  15404  sin0pilem1  15420  sin0pilem2  15421  sinmpi  15454  cosmpi  15455  sinppi  15456  cosppi  15457  lgsdilem  15671  lgsdir2  15677  lgsdirnn0  15691  lgsdinn0  15692  lgsquad3  15728  trilpolemclim  16315  trilpolemisumle  16317  trilpolemeq1  16319  nconstwlpolem0  16342