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