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 ℝ\exists y\in ℝ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 ℝ\exists y\in ℝ0=x+\mathrm{i}y$$
19	2 18	ax-mp	$$⊢\exists x\in ℝ\exists y\in ℝ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\leftrightarrow 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 ℝ\exists y\in ℝ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	eqtrdi	$$⊢\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\leftrightarrow 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 ℝ\exists y\in ℝA=x+\mathrm{i}y\to 0\cdot A=0$$
34	1 33	syl	$$⊢A\in ℂ\to 0\cdot A=0$$