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 ∈ ℂ → A B − C = A B A C

Proof

Step Hyp Ref Expression
1 negcl ⊢ C ∈ ℂ → − C ∈ ℂ
2 cxpadd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ − C ∈ ℂ → A B + − C = A B ⁢ A − C
3 1 2 syl3an3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B + − C = A B ⁢ 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 ∈ ℂ → A B + − C = A B − 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 = 1 A C
11 8 9 5 10 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C = 1 A C
12 11 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B ⁢ A − C = A B ⁢ 1 A C
13 cxpcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A B ∈ ℂ
14 8 4 13 syl2anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B ∈ ℂ
15 cxpcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A C ∈ ℂ
16 8 5 15 syl2anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A C ∈ ℂ
17 cxpne0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ C ∈ ℂ → A C ≠ 0
18 8 9 5 17 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A C ≠ 0
19 14 16 18 divrecd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B A C = A B ⁢ 1 A C
20 12 19 eqtr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B ⁢ A − C = A B A C
21 3 7 20 3eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℂ → A B − C = A B A C