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

Metamath Proof Explorer

Theorem cxpsub

Description: Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion cxpsub ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) / ( 𝐴 ↑𝑐 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐶 ∈ ℂ → - 𝐶 ∈ ℂ )
2 cxpadd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ - 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 - 𝐶 ) ) )
3 1 2 syl3an3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 - 𝐶 ) ) )
4 simp2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
5 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
6 4 5 negsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
7 6 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 + - 𝐶 ) ) = ( 𝐴 ↑𝑐 ( 𝐵 − 𝐶 ) ) )
8 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
9 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ≠ 0 )
10 cxpneg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 - 𝐶 ) = ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) )
11 8 9 5 10 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 - 𝐶 ) = ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) )
12 11 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) )
13 cxpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
14 8 4 13 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
15 cxpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
16 8 5 15 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
17 cxpne0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ≠ 0 )
18 8 9 5 17 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ≠ 0 )
19 14 16 18 divrecd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) / ( 𝐴 ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) )
20 12 19 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) · ( 𝐴 ↑𝑐 - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) / ( 𝐴 ↑𝑐 𝐶 ) ) )
21 3 7 20 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) / ( 𝐴 ↑𝑐 𝐶 ) ) )