**Description:** Multiplication by 0 . Theorem I.6 of Apostol p. 18. (Contributed by NM, 15-May-1999) (Revised by Scott Fenton, 3-Jan-2013)

Ref | Expression | ||
---|---|---|---|

Assertion | mul01 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 0cn | ⊢ 0 ∈ ℂ | |

2 | mulcom | ⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) ) | |

3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) ) |

4 | mul02 | ⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 ) | |

5 | 3 4 | eqtrd | ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 ) |