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 e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 <-> ( A = 0 /\ B =/= 0 ) ) )

Proof

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