Metamath Proof Explorer

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 )