# Metamath Proof Explorer

## Theorem mul02

Description: Multiplication by 0 . Theorem I.6 of Apostol p. 18. Based on ideas by Eric Schmidt. (Contributed by NM, 10-Aug-1999) (Revised by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul02 ${⊢}{A}\in ℂ\to 0\cdot {A}=0$

### Proof

Step Hyp Ref Expression
1 cnre ${⊢}{A}\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}$
2 0cn ${⊢}0\in ℂ$
3 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
4 ax-icn ${⊢}\mathrm{i}\in ℂ$
5 recn ${⊢}{y}\in ℝ\to {y}\in ℂ$
6 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge {y}\in ℂ\right)\to \mathrm{i}{y}\in ℂ$
7 4 5 6 sylancr ${⊢}{y}\in ℝ\to \mathrm{i}{y}\in ℂ$
8 adddi ${⊢}\left(0\in ℂ\wedge {x}\in ℂ\wedge \mathrm{i}{y}\in ℂ\right)\to 0\cdot \left({x}+\mathrm{i}{y}\right)=0\cdot {x}+0\cdot \mathrm{i}{y}$
9 2 3 7 8 mp3an3an ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to 0\cdot \left({x}+\mathrm{i}{y}\right)=0\cdot {x}+0\cdot \mathrm{i}{y}$
10 mul02lem2 ${⊢}{x}\in ℝ\to 0\cdot {x}=0$
11 mul12 ${⊢}\left(0\in ℂ\wedge \mathrm{i}\in ℂ\wedge {y}\in ℂ\right)\to 0\cdot \mathrm{i}{y}=\mathrm{i}0\cdot {y}$
12 2 4 5 11 mp3an12i ${⊢}{y}\in ℝ\to 0\cdot \mathrm{i}{y}=\mathrm{i}0\cdot {y}$
13 mul02lem2 ${⊢}{y}\in ℝ\to 0\cdot {y}=0$
14 13 oveq2d ${⊢}{y}\in ℝ\to \mathrm{i}0\cdot {y}=\mathrm{i}\cdot 0$
15 12 14 eqtrd ${⊢}{y}\in ℝ\to 0\cdot \mathrm{i}{y}=\mathrm{i}\cdot 0$
16 10 15 oveqan12d ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to 0\cdot {x}+0\cdot \mathrm{i}{y}=0+\mathrm{i}\cdot 0$
17 9 16 eqtrd ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to 0\cdot \left({x}+\mathrm{i}{y}\right)=0+\mathrm{i}\cdot 0$
18 cnre ${⊢}0\in ℂ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}0={x}+\mathrm{i}{y}$
19 2 18 ax-mp ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}0={x}+\mathrm{i}{y}$
20 oveq2 ${⊢}0={x}+\mathrm{i}{y}\to 0\cdot 0=0\cdot \left({x}+\mathrm{i}{y}\right)$
21 20 eqeq1d ${⊢}0={x}+\mathrm{i}{y}\to \left(0\cdot 0=0+\mathrm{i}\cdot 0↔0\cdot \left({x}+\mathrm{i}{y}\right)=0+\mathrm{i}\cdot 0\right)$
22 17 21 syl5ibrcom ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left(0={x}+\mathrm{i}{y}\to 0\cdot 0=0+\mathrm{i}\cdot 0\right)$
23 22 rexlimivv ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}0={x}+\mathrm{i}{y}\to 0\cdot 0=0+\mathrm{i}\cdot 0$
24 19 23 ax-mp ${⊢}0\cdot 0=0+\mathrm{i}\cdot 0$
25 0re ${⊢}0\in ℝ$
26 mul02lem2 ${⊢}0\in ℝ\to 0\cdot 0=0$
27 25 26 ax-mp ${⊢}0\cdot 0=0$
28 24 27 eqtr3i ${⊢}0+\mathrm{i}\cdot 0=0$
29 17 28 syl6eq ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to 0\cdot \left({x}+\mathrm{i}{y}\right)=0$
30 oveq2 ${⊢}{A}={x}+\mathrm{i}{y}\to 0\cdot {A}=0\cdot \left({x}+\mathrm{i}{y}\right)$
31 30 eqeq1d ${⊢}{A}={x}+\mathrm{i}{y}\to \left(0\cdot {A}=0↔0\cdot \left({x}+\mathrm{i}{y}\right)=0\right)$
32 29 31 syl5ibrcom ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to \left({A}={x}+\mathrm{i}{y}\to 0\cdot {A}=0\right)$
33 32 rexlimivv ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{A}={x}+\mathrm{i}{y}\to 0\cdot {A}=0$
34 1 33 syl ${⊢}{A}\in ℂ\to 0\cdot {A}=0$