This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 ax-1ne0 ⊢ 1 ≠ 0
2 ax-1cn ⊢ 1 ∈ ℂ
3 mul02lem1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 1 ∈ ℂ ) → 1 = ( 1 + 1 ) )
4 2 3 mpan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → 1 = ( 1 + 1 ) )
5 4 eqcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ( 1 + 1 ) = 1 )
6 5 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ( ( i · i ) + ( 1 + 1 ) ) = ( ( i · i ) + 1 ) )
7 ax-icn ⊢ i ∈ ℂ
8 7 7 mulcli ⊢ ( i · i ) ∈ ℂ
9 8 2 2 addassi ⊢ ( ( ( i · i ) + 1 ) + 1 ) = ( ( i · i ) + ( 1 + 1 ) )
10 ax-i2m1 ⊢ ( ( i · i ) + 1 ) = 0
11 10 oveq1i ⊢ ( ( ( i · i ) + 1 ) + 1 ) = ( 0 + 1 )
12 9 11 eqtr3i ⊢ ( ( i · i ) + ( 1 + 1 ) ) = ( 0 + 1 )
13 00id ⊢ ( 0 + 0 ) = 0
14 10 13 eqtr4i ⊢ ( ( i · i ) + 1 ) = ( 0 + 0 )
15 6 12 14 3eqtr3g ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ( 0 + 1 ) = ( 0 + 0 ) )
16 1re ⊢ 1 ∈ ℝ
17 0re ⊢ 0 ∈ ℝ
18 readdcan ⊢ ( ( 1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 + 1 ) = ( 0 + 0 ) ↔ 1 = 0 ) )
19 16 17 17 18 mp3an ⊢ ( ( 0 + 1 ) = ( 0 + 0 ) ↔ 1 = 0 )
20 15 19 sylib ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → 1 = 0 )
21 20 ex ⊢ ( 𝐴 ∈ ℝ → ( ( 0 · 𝐴 ) ≠ 0 → 1 = 0 ) )
22 21 necon1d ⊢ ( 𝐴 ∈ ℝ → ( 1 ≠ 0 → ( 0 · 𝐴 ) = 0 ) )
23 1 22 mpi ⊢ ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )