This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )