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

Proof

Step	Hyp	Ref	Expression
1		cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2		0cn	⊢ 0 ∈ ℂ
3		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
4		ax-icn	⊢ i ∈ ℂ
5		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
6		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
7	4 5 6	sylancr	⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∈ ℂ )
8		adddi	⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) )
9	2 3 7 8	mp3an3an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) )
10		mul02lem2	⊢ ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
11		mul12	⊢ ( ( 0 ∈ ℂ ∧ i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 · ( i · 𝑦 ) ) = ( i · ( 0 · 𝑦 ) ) )
12	2 4 5 11	mp3an12i	⊢ ( 𝑦 ∈ ℝ → ( 0 · ( i · 𝑦 ) ) = ( i · ( 0 · 𝑦 ) ) )
13		mul02lem2	⊢ ( 𝑦 ∈ ℝ → ( 0 · 𝑦 ) = 0 )
14	13	oveq2d	⊢ ( 𝑦 ∈ ℝ → ( i · ( 0 · 𝑦 ) ) = ( i · 0 ) )
15	12 14	eqtrd	⊢ ( 𝑦 ∈ ℝ → ( 0 · ( i · 𝑦 ) ) = ( i · 0 ) )
16	10 15	oveqan12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) = ( 0 + ( i · 0 ) ) )
17	9 16	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( 0 + ( i · 0 ) ) )
18		cnre	⊢ ( 0 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 0 = ( 𝑥 + ( i · 𝑦 ) ) )
19	2 18	ax-mp	⊢ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 0 = ( 𝑥 + ( i · 𝑦 ) )
20		oveq2	⊢ ( 0 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 0 ) = ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) )
21	20	eqeq1d	⊢ ( 0 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 0 · 0 ) = ( 0 + ( i · 0 ) ) ↔ ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( 0 + ( i · 0 ) ) ) )
22	17 21	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 0 ) = ( 0 + ( i · 0 ) ) ) )
23	22	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 0 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 0 ) = ( 0 + ( i · 0 ) ) )
24	19 23	ax-mp	⊢ ( 0 · 0 ) = ( 0 + ( i · 0 ) )
25		0re	⊢ 0 ∈ ℝ
26		mul02lem2	⊢ ( 0 ∈ ℝ → ( 0 · 0 ) = 0 )
27	25 26	ax-mp	⊢ ( 0 · 0 ) = 0
28	24 27	eqtr3i	⊢ ( 0 + ( i · 0 ) ) = 0
29	17 28	eqtrdi	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = 0 )
30		oveq2	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) )
31	30	eqeq1d	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 0 · 𝐴 ) = 0 ↔ ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
32	29 31	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = 0 ) )
33	32	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = 0 )
34	1 33	syl	⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )