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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) )

Proof

Step Hyp Ref Expression
1 cxpne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )
2 1 3com23 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )
3 2 3expia ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ≠ 0 → ( 𝐴𝑐 𝐵 ) ≠ 0 ) )
4 3 necon4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) = 0 → 𝐴 = 0 ) )
5 ax-1ne0 1 ≠ 0
6 cxp0 ( 𝐴 ∈ ℂ → ( 𝐴𝑐 0 ) = 1 )
7 6 neeq1d ( 𝐴 ∈ ℂ → ( ( 𝐴𝑐 0 ) ≠ 0 ↔ 1 ≠ 0 ) )
8 5 7 mpbiri ( 𝐴 ∈ ℂ → ( 𝐴𝑐 0 ) ≠ 0 )
9 8 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 0 ) ≠ 0 )
10 oveq2 ( 𝐵 = 0 → ( 𝐴𝑐 𝐵 ) = ( 𝐴𝑐 0 ) )
11 10 neeq1d ( 𝐵 = 0 → ( ( 𝐴𝑐 𝐵 ) ≠ 0 ↔ ( 𝐴𝑐 0 ) ≠ 0 ) )
12 9 11 syl5ibrcom ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 = 0 → ( 𝐴𝑐 𝐵 ) ≠ 0 ) )
13 12 necon2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) = 0 → 𝐵 ≠ 0 ) )
14 4 13 jcad ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) = 0 → ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) )
15 0cxp ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
16 oveq1 ( 𝐴 = 0 → ( 𝐴𝑐 𝐵 ) = ( 0 ↑𝑐 𝐵 ) )
17 16 eqeq1d ( 𝐴 = 0 → ( ( 𝐴𝑐 𝐵 ) = 0 ↔ ( 0 ↑𝑐 𝐵 ) = 0 ) )
18 15 17 syl5ibrcom ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 = 0 → ( 𝐴𝑐 𝐵 ) = 0 ) )
19 18 expimpd ( 𝐵 ∈ ℂ → ( ( 𝐵 ≠ 0 ∧ 𝐴 = 0 ) → ( 𝐴𝑐 𝐵 ) = 0 ) )
20 19 ancomsd ( 𝐵 ∈ ℂ → ( ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) → ( 𝐴𝑐 𝐵 ) = 0 ) )
21 20 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) → ( 𝐴𝑐 𝐵 ) = 0 ) )
22 14 21 impbid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) )