Proof of Theorem mulexpz
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12263 |
. . 3
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
2 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
3 | | simpl 482 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) |
4 | 2, 3 | anim12i 612 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℂ ∧ 𝐵 ∈
ℂ)) |
5 | | mulexp 13750 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
6 | 5 | 3expa 1116 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
7 | 4, 6 | sylan 579 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
8 | | simplll 771 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈
ℂ) |
9 | | simplrl 773 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐵 ∈
ℂ) |
10 | 8, 9 | mulcld 10926 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴 · 𝐵) ∈ ℂ) |
11 | | recn 10892 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
12 | 11 | ad2antrl 724 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℂ) |
13 | | nnnn0 12170 |
. . . . . . 7
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℕ0) |
14 | 13 | ad2antll 725 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ0) |
15 | | expneg2 13719 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → ((𝐴 · 𝐵)↑𝑁) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
16 | 10, 12, 14, 15 | syl3anc 1369 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑𝑁) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
17 | | expneg2 13719 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
18 | 8, 12, 14, 17 | syl3anc 1369 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
19 | | expneg2 13719 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) = (1 / (𝐵↑-𝑁))) |
20 | 9, 12, 14, 19 | syl3anc 1369 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑𝑁) = (1 / (𝐵↑-𝑁))) |
21 | 18, 20 | oveq12d 7273 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑁) · (𝐵↑𝑁)) = ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁)))) |
22 | | mulexp 13750 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑-𝑁) = ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
23 | 8, 9, 14, 22 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑-𝑁) = ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
24 | 23 | oveq2d 7271 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = (1 / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
25 | | 1t1e1 12065 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
26 | 25 | oveq1i 7265 |
. . . . . . . 8
⊢ ((1
· 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁))) = (1 / ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
27 | 24, 26 | eqtr4di 2797 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
28 | | expcl 13728 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑-𝑁) ∈
ℂ) |
29 | 8, 14, 28 | syl2anc 583 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ) |
30 | | simpllr 772 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0) |
31 | | nnz 12272 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℤ) |
32 | 31 | ad2antll 725 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℤ) |
33 | | expne0i 13743 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐴↑-𝑁) ≠ 0) |
34 | 8, 30, 32, 33 | syl3anc 1369 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ≠ 0) |
35 | | expcl 13728 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐵↑-𝑁) ∈
ℂ) |
36 | 9, 14, 35 | syl2anc 583 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑-𝑁) ∈ ℂ) |
37 | | simplrr 774 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐵 ≠ 0) |
38 | | expne0i 13743 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐵↑-𝑁) ≠ 0) |
39 | 9, 37, 32, 38 | syl3anc 1369 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑-𝑁) ≠ 0) |
40 | | ax-1cn 10860 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
41 | | divmuldiv 11605 |
. . . . . . . . 9
⊢ (((1
∈ ℂ ∧ 1 ∈ ℂ) ∧ (((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0) ∧ ((𝐵↑-𝑁) ∈ ℂ ∧ (𝐵↑-𝑁) ≠ 0))) → ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
42 | 40, 40, 41 | mpanl12 698 |
. . . . . . . 8
⊢ ((((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0) ∧ ((𝐵↑-𝑁) ∈ ℂ ∧ (𝐵↑-𝑁) ≠ 0)) → ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
43 | 29, 34, 36, 39, 42 | syl22anc 835 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((1 /
(𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
44 | 27, 43 | eqtr4d 2781 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁)))) |
45 | 21, 44 | eqtr4d 2781 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑁) · (𝐵↑𝑁)) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
46 | 16, 45 | eqtr4d 2781 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
47 | 7, 46 | jaodan 954 |
. . 3
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ))) →
((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
48 | 1, 47 | sylan2b 593 |
. 2
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
49 | 48 | 3impa 1108 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |