Metamath Proof Explorer


Theorem cxpneg

Description: Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpneg ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 - 𝐵 ) = ( 1 / ( 𝐴𝑐 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
2 simp3 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
3 cxpcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ∈ ℂ )
4 1 2 3 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ∈ ℂ )
5 2 negcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → - 𝐵 ∈ ℂ )
6 cxpcl ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( 𝐴𝑐 - 𝐵 ) ∈ ℂ )
7 1 5 6 syl2anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 - 𝐵 ) ∈ ℂ )
8 cxpne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )
9 2 negidd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐵 + - 𝐵 ) = 0 )
10 9 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 ( 𝐵 + - 𝐵 ) ) = ( 𝐴𝑐 0 ) )
11 simp2 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → 𝐴 ≠ 0 )
12 cxpadd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( 𝐴𝑐 ( 𝐵 + - 𝐵 ) ) = ( ( 𝐴𝑐 𝐵 ) · ( 𝐴𝑐 - 𝐵 ) ) )
13 1 11 2 5 12 syl211anc ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 ( 𝐵 + - 𝐵 ) ) = ( ( 𝐴𝑐 𝐵 ) · ( 𝐴𝑐 - 𝐵 ) ) )
14 cxp0 ( 𝐴 ∈ ℂ → ( 𝐴𝑐 0 ) = 1 )
15 1 14 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 0 ) = 1 )
16 10 13 15 3eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) · ( 𝐴𝑐 - 𝐵 ) ) = 1 )
17 4 7 8 16 mvllmuld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 - 𝐵 ) = ( 1 / ( 𝐴𝑐 𝐵 ) ) )