Proof of Theorem mulexpz
| Step | Hyp | Ref
| Expression |
| 1 | | elznn0nn 12627 |
. . 3
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
| 2 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
| 3 | | simpl 482 |
. . . . . 6
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) |
| 4 | 2, 3 | anim12i 613 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 ∈ ℂ ∧ 𝐵 ∈
ℂ)) |
| 5 | | mulexp 14142 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 6 | 5 | 3expa 1119 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 7 | 4, 6 | sylan 580 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 8 | | simplll 775 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈
ℂ) |
| 9 | | simplrl 777 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐵 ∈
ℂ) |
| 10 | 8, 9 | mulcld 11281 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴 · 𝐵) ∈ ℂ) |
| 11 | | recn 11245 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
| 12 | 11 | ad2antrl 728 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℂ) |
| 13 | | nnnn0 12533 |
. . . . . . 7
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℕ0) |
| 14 | 13 | ad2antll 729 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ0) |
| 15 | | expneg2 14111 |
. . . . . 6
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → ((𝐴 · 𝐵)↑𝑁) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
| 16 | 10, 12, 14, 15 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑𝑁) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
| 17 | | expneg2 14111 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
| 18 | 8, 12, 14, 17 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
| 19 | | expneg2 14111 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) = (1 / (𝐵↑-𝑁))) |
| 20 | 9, 12, 14, 19 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑𝑁) = (1 / (𝐵↑-𝑁))) |
| 21 | 18, 20 | oveq12d 7449 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑁) · (𝐵↑𝑁)) = ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁)))) |
| 22 | | mulexp 14142 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ ((𝐴 · 𝐵)↑-𝑁) = ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
| 23 | 8, 9, 14, 22 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑-𝑁) = ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
| 24 | 23 | oveq2d 7447 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = (1 / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
| 25 | | 1t1e1 12428 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
| 26 | 25 | oveq1i 7441 |
. . . . . . . 8
⊢ ((1
· 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁))) = (1 / ((𝐴↑-𝑁) · (𝐵↑-𝑁))) |
| 27 | 24, 26 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
| 28 | | expcl 14120 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑-𝑁) ∈
ℂ) |
| 29 | 8, 14, 28 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ) |
| 30 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0) |
| 31 | | nnz 12634 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℤ) |
| 32 | 31 | ad2antll 729 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℤ) |
| 33 | | expne0i 14135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐴↑-𝑁) ≠ 0) |
| 34 | 8, 30, 32, 33 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ≠ 0) |
| 35 | | expcl 14120 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐵↑-𝑁) ∈
ℂ) |
| 36 | 9, 14, 35 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑-𝑁) ∈ ℂ) |
| 37 | | simplrr 778 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐵 ≠ 0) |
| 38 | | expne0i 14135 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ -𝑁 ∈ ℤ) → (𝐵↑-𝑁) ≠ 0) |
| 39 | 9, 37, 32, 38 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐵↑-𝑁) ≠ 0) |
| 40 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 41 | | divmuldiv 11967 |
. . . . . . . . 9
⊢ (((1
∈ ℂ ∧ 1 ∈ ℂ) ∧ (((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0) ∧ ((𝐵↑-𝑁) ∈ ℂ ∧ (𝐵↑-𝑁) ≠ 0))) → ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
| 42 | 40, 40, 41 | mpanl12 702 |
. . . . . . . 8
⊢ ((((𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0) ∧ ((𝐵↑-𝑁) ∈ ℂ ∧ (𝐵↑-𝑁) ≠ 0)) → ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
| 43 | 29, 34, 36, 39, 42 | syl22anc 839 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((1 /
(𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁))) = ((1 · 1) / ((𝐴↑-𝑁) · (𝐵↑-𝑁)))) |
| 44 | 27, 43 | eqtr4d 2780 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
((𝐴 · 𝐵)↑-𝑁)) = ((1 / (𝐴↑-𝑁)) · (1 / (𝐵↑-𝑁)))) |
| 45 | 21, 44 | eqtr4d 2780 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴↑𝑁) · (𝐵↑𝑁)) = (1 / ((𝐴 · 𝐵)↑-𝑁))) |
| 46 | 16, 45 | eqtr4d 2780 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 47 | 7, 46 | jaodan 960 |
. . 3
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ))) →
((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 48 | 1, 47 | sylan2b 594 |
. 2
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
| 49 | 48 | 3impa 1110 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |