# Metamath Proof Explorer

## 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↔1=0\right)$
19 16 17 17 18 mp3an ${⊢}0+1=0+0↔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$