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

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 / ( 𝐴 ↑𝑐 𝐵 ) ) )