Proof of Theorem absexpz
| Step | Hyp | Ref
| Expression |
| 1 | | elznn0nn 12627 |
. 2
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
| 2 | | absexp 15343 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
| 3 | 2 | ex 412 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑁 ∈ ℕ0
→ (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑁 ∈ ℕ0
→ (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
| 5 | | 1cnd 11256 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 1
∈ ℂ) |
| 6 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈
ℂ) |
| 7 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℕ0) |
| 8 | 7 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ0) |
| 9 | 6, 8 | expcld 14186 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ) |
| 10 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ≠ 0) |
| 11 | | nnz 12634 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℤ) |
| 12 | 11 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℤ) |
| 13 | 6, 10, 12 | expne0d 14192 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ≠ 0) |
| 14 | | absdiv 15334 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ (𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) ≠ 0) → (abs‘(1 / (𝐴↑-𝑁))) = ((abs‘1) / (abs‘(𝐴↑-𝑁)))) |
| 15 | 5, 9, 13, 14 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(1 / (𝐴↑-𝑁))) = ((abs‘1) / (abs‘(𝐴↑-𝑁)))) |
| 16 | | abs1 15336 |
. . . . . . . . 9
⊢
(abs‘1) = 1 |
| 17 | 16 | oveq1i 7441 |
. . . . . . . 8
⊢
((abs‘1) / (abs‘(𝐴↑-𝑁))) = (1 / (abs‘(𝐴↑-𝑁))) |
| 18 | | absexp 15343 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (abs‘(𝐴↑-𝑁)) = ((abs‘𝐴)↑-𝑁)) |
| 19 | 6, 8, 18 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(𝐴↑-𝑁)) = ((abs‘𝐴)↑-𝑁)) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
(abs‘(𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
| 21 | 17, 20 | eqtrid 2789 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
((abs‘1) / (abs‘(𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
| 22 | 15, 21 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(1 / (𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
| 23 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℝ) |
| 24 | 23 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈
ℂ) |
| 25 | | expneg2 14111 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
| 26 | 6, 24, 8, 25 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
| 27 | 26 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(𝐴↑𝑁)) = (abs‘(1 / (𝐴↑-𝑁)))) |
| 28 | | abscl 15317 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
| 29 | 28 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘𝐴) ∈
ℝ) |
| 30 | 29 | recnd 11289 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘𝐴) ∈
ℂ) |
| 31 | | expneg2 14111 |
. . . . . . 7
⊢
(((abs‘𝐴)
∈ ℂ ∧ 𝑁
∈ ℂ ∧ -𝑁
∈ ℕ0) → ((abs‘𝐴)↑𝑁) = (1 / ((abs‘𝐴)↑-𝑁))) |
| 32 | 30, 24, 8, 31 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
((abs‘𝐴)↑𝑁) = (1 / ((abs‘𝐴)↑-𝑁))) |
| 33 | 22, 27, 32 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
| 34 | 33 | ex 412 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
| 35 | 4, 34 | jaod 860 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ)) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
| 36 | 35 | 3impia 1118 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
| 37 | 1, 36 | syl3an3b 1407 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |