Metamath Proof Explorer

Theorem cxpsub

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

Ref Expression
Assertion cxpsub ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB−C=ABAC

Proof

Step Hyp Ref Expression
1 negcl ⊢C∈ℂ→−C∈ℂ
2 cxpadd ⊢A∈ℂ∧A≠0∧B∈ℂ∧−C∈ℂ→AB+−C=AB⁢A−C
3 1 2 syl3an3 ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB+−C=AB⁢A−C
4 simp2 ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→B∈ℂ
5 simp3 ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→C∈ℂ
6 4 5 negsubd ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→B+−C=B−C
7 6 oveq2d ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB+−C=AB−C
8 simp1l ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→A∈ℂ
9 simp1r ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→A≠0
10 cxpneg ⊢A∈ℂ∧A≠0∧C∈ℂ→A−C=1AC
11 8 9 5 10 syl3anc ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→A−C=1AC
12 11 oveq2d ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB⁢A−C=AB⁢1AC
13 cxpcl ⊢A∈ℂ∧B∈ℂ→AB∈ℂ
14 8 4 13 syl2anc ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB∈ℂ
15 cxpcl ⊢A∈ℂ∧C∈ℂ→AC∈ℂ
16 8 5 15 syl2anc ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AC∈ℂ
17 cxpne0 ⊢A∈ℂ∧A≠0∧C∈ℂ→AC≠0
18 8 9 5 17 syl3anc ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AC≠0
19 14 16 18 divrecd ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→ABAC=AB⁢1AC
20 12 19 eqtr4d ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB⁢A−C=ABAC
21 3 7 20 3eqtr3d ⊢A∈ℂ∧A≠0∧B∈ℂ∧C∈ℂ→AB−C=ABAC