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 A 0 A = 0

Proof

Step Hyp Ref Expression
1 cnre A x y A = x + i y
2 0cn 0
3 recn x x
4 ax-icn i
5 recn y y
6 mulcl i y i y
7 4 5 6 sylancr y i y
8 adddi 0 x i y 0 x + i y = 0 x + 0 i y
9 2 3 7 8 mp3an3an x y 0 x + i y = 0 x + 0 i y
10 mul02lem2 x 0 x = 0
11 mul12 0 i y 0 i y = i 0 y
12 2 4 5 11 mp3an12i y 0 i y = i 0 y
13 mul02lem2 y 0 y = 0
14 13 oveq2d y i 0 y = i 0
15 12 14 eqtrd y 0 i y = i 0
16 10 15 oveqan12d x y 0 x + 0 i y = 0 + i 0
17 9 16 eqtrd x y 0 x + i y = 0 + i 0
18 cnre 0 x y 0 = x + i y
19 2 18 ax-mp x y 0 = x + i y
20 oveq2 0 = x + i y 0 0 = 0 x + i y
21 20 eqeq1d 0 = x + i y 0 0 = 0 + i 0 0 x + i y = 0 + i 0
22 17 21 syl5ibrcom x y 0 = x + i y 0 0 = 0 + i 0
23 22 rexlimivv x y 0 = x + i y 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 x y 0 x + i y = 0
30 oveq2 A = x + i y 0 A = 0 x + i y
31 30 eqeq1d A = x + i y 0 A = 0 0 x + i y = 0
32 29 31 syl5ibrcom x y A = x + i y 0 A = 0
33 32 rexlimivv x y A = x + i y 0 A = 0
34 1 33 syl A 0 A = 0