Metamath Proof Explorer


Theorem cxpeq0

Description: Complex exponentiation is zero iff the base is zero and the exponent is nonzero. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion cxpeq0 A B A B = 0 A = 0 B 0

Proof

Step Hyp Ref Expression
1 cxpne0 A A 0 B A B 0
2 1 3com23 A B A 0 A B 0
3 2 3expia A B A 0 A B 0
4 3 necon4d A B A B = 0 A = 0
5 ax-1ne0 1 0
6 cxp0 A A 0 = 1
7 6 neeq1d A A 0 0 1 0
8 5 7 mpbiri A A 0 0
9 8 adantr A B A 0 0
10 oveq2 B = 0 A B = A 0
11 10 neeq1d B = 0 A B 0 A 0 0
12 9 11 syl5ibrcom A B B = 0 A B 0
13 12 necon2d A B A B = 0 B 0
14 4 13 jcad A B A B = 0 A = 0 B 0
15 0cxp B B 0 0 B = 0
16 oveq1 A = 0 A B = 0 B
17 16 eqeq1d A = 0 A B = 0 0 B = 0
18 15 17 syl5ibrcom B B 0 A = 0 A B = 0
19 18 expimpd B B 0 A = 0 A B = 0
20 19 ancomsd B A = 0 B 0 A B = 0
21 20 adantl A B A = 0 B 0 A B = 0
22 14 21 impbid A B A B = 0 A = 0 B 0