Theorem mul02lem2

Description: Lemma for mul02 . Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013)

	Ref	Expression
Assertion	mul02lem2	$$⊢A\in ℝ\to 0\cdot A=0$$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$$⊢1\ne 0$$
2		ax-1cn	$$⊢1\in ℂ$$
3		mul02lem1	$$⊢\left(\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\wedge 1\in ℂ\right)\to 1=1+1$$
4	2 3	mpan2	$$⊢\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\to 1=1+1$$
5	4	eqcomd	$$⊢\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\to 1+1=1$$
6	5	oveq2d	$$⊢\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\to \mathrm{i}\mathrm{i}+1+1=\mathrm{i}\mathrm{i}+1$$
7		ax-icn	$$⊢\mathrm{i}\in ℂ$$
8	7 7	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
9	8 2 2	addassi	$$⊢\mathrm{i}\mathrm{i}+1+1=\mathrm{i}\mathrm{i}+1+1$$
10		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
11	10	oveq1i	$$⊢\mathrm{i}\mathrm{i}+1+1=0+1$$
12	9 11	eqtr3i	$$⊢\mathrm{i}\mathrm{i}+1+1=0+1$$
13		00id	$$⊢0+0=0$$
14	10 13	eqtr4i	$$⊢\mathrm{i}\mathrm{i}+1=0+0$$
15	6 12 14	3eqtr3g	$$⊢\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\to 0+1=0+0$$
16		1re	$$⊢1\in ℝ$$
17		0re	$$⊢0\in ℝ$$
18		readdcan	$$⊢\left(1\in ℝ\wedge 0\in ℝ\wedge 0\in ℝ\right)\to \left(0+1=0+0\leftrightarrow 1=0\right)$$
19	16 17 17 18	mp3an	$$⊢0+1=0+0\leftrightarrow 1=0$$
20	15 19	sylib	$$⊢\left(A\in ℝ\wedge 0\cdot A\ne 0\right)\to 1=0$$
21	20	ex	$$⊢A\in ℝ\to \left(0\cdot A\ne 0\to 1=0\right)$$
22	21	necon1d	$$⊢A\in ℝ\to \left(1\ne 0\to 0\cdot A=0\right)$$
23	1 22	mpi	$$⊢A\in ℝ\to 0\cdot A=0$$