Metamath Proof Explorer

Theorem cxpmul2z

Description: Generalize cxpmul2 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion cxpmul2z ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℤ → A B ⁢ C = A B C

Proof

Step Hyp Ref Expression
1 elznn0 ⊢ C ∈ ℤ ↔ C ∈ ℝ ∧ C ∈ ℕ 0 ∨ − C ∈ ℕ 0
2 cxpmul2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℕ 0 → A B ⁢ C = A B C
3 2 3expia ⊢ A ∈ ℂ ∧ B ∈ ℂ → C ∈ ℕ 0 → A B ⁢ C = A B C
4 3 ad4ant13 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℕ 0 → A B ⁢ C = A B C
5 simplll ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A ∈ ℂ
6 simplr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → B ∈ ℂ
7 simprr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → − C ∈ ℕ 0
8 cxpmul2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ − C ∈ ℕ 0 → A B ⁢ − C = A B − C
9 5 6 7 8 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A B ⁢ − C = A B − C
10 9 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → 1 A B ⁢ − C = 1 A B − C
11 simprl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → C ∈ ℝ
12 11 recnd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → C ∈ ℂ
13 6 12 mulneg2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → B ⁢ − C = − B ⁢ C
14 13 negeqd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → − B ⁢ − C = − − B ⁢ C
15 6 12 mulcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → B ⁢ C ∈ ℂ
16 15 negnegd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → − − B ⁢ C = B ⁢ C
17 14 16 eqtrd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → − B ⁢ − C = B ⁢ C
18 17 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A − B ⁢ − C = A B ⁢ C
19 simpllr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A ≠ 0
20 12 negcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → − C ∈ ℂ
21 6 20 mulcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → B ⁢ − C ∈ ℂ
22 cxpneg ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ⁢ − C ∈ ℂ → A − B ⁢ − C = 1 A B ⁢ − C
23 5 19 21 22 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A − B ⁢ − C = 1 A B ⁢ − C
24 18 23 eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A B ⁢ C = 1 A B ⁢ − C
25 cxpcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A B ∈ ℂ
26 25 ad4ant13 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A B ∈ ℂ
27 expneg2 ⊢ A B ∈ ℂ ∧ C ∈ ℂ ∧ − C ∈ ℕ 0 → A B C = 1 A B − C
28 26 12 7 27 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A B C = 1 A B − C
29 10 24 28 3eqtr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ ∧ − C ∈ ℕ 0 → A B ⁢ C = A B C
30 29 expr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ → − C ∈ ℕ 0 → A B ⁢ C = A B C
31 4 30 jaod ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℝ → C ∈ ℕ 0 ∨ − C ∈ ℕ 0 → A B ⁢ C = A B C
32 31 expimpd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → C ∈ ℝ ∧ C ∈ ℕ 0 ∨ − C ∈ ℕ 0 → A B ⁢ C = A B C
33 1 32 biimtrid ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ → C ∈ ℤ → A B ⁢ C = A B C
34 33 impr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ C ∈ ℤ → A B ⁢ C = A B C