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 ) ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) / ( 𝐴 ↑𝑐 𝐶 ) ) )