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 )