Proof of Theorem absexpzap
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 9061 |
. 2
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) |
2 | | absexp 10844 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
3 | 2 | ex 114 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑁 ∈ ℕ0
→ (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
4 | 3 | adantr 274 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝑁 ∈ ℕ0 →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
5 | | 1cnd 7775 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 1 ∈
ℂ) |
6 | | simpll 518 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 ∈ ℂ) |
7 | | nnnn0 8977 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℕ0) |
8 | 7 | ad2antll 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈
ℕ0) |
9 | 6, 8 | expcld 10417 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) ∈ ℂ) |
10 | | simplr 519 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝐴 # 0) |
11 | | nnz 9066 |
. . . . . . . . . 10
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℤ) |
12 | 11 | ad2antll 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → -𝑁 ∈ ℤ) |
13 | 6, 10, 12 | expap0d 10423 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑-𝑁) # 0) |
14 | | absdivap 10835 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ (𝐴↑-𝑁) ∈ ℂ ∧ (𝐴↑-𝑁) # 0) → (abs‘(1 / (𝐴↑-𝑁))) = ((abs‘1) / (abs‘(𝐴↑-𝑁)))) |
15 | 5, 9, 13, 14 | syl3anc 1216 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘(1 /
(𝐴↑-𝑁))) = ((abs‘1) / (abs‘(𝐴↑-𝑁)))) |
16 | | abs1 10837 |
. . . . . . . . 9
⊢
(abs‘1) = 1 |
17 | 16 | oveq1i 5777 |
. . . . . . . 8
⊢
((abs‘1) / (abs‘(𝐴↑-𝑁))) = (1 / (abs‘(𝐴↑-𝑁))) |
18 | | absexp 10844 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (abs‘(𝐴↑-𝑁)) = ((abs‘𝐴)↑-𝑁)) |
19 | 6, 8, 18 | syl2anc 408 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘(𝐴↑-𝑁)) = ((abs‘𝐴)↑-𝑁)) |
20 | 19 | oveq2d 5783 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (1 /
(abs‘(𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
21 | 17, 20 | syl5eq 2182 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((abs‘1) /
(abs‘(𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
22 | 15, 21 | eqtrd 2170 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘(1 /
(𝐴↑-𝑁))) = (1 / ((abs‘𝐴)↑-𝑁))) |
23 | | simprl 520 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℝ) |
24 | 23 | recnd 7787 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → 𝑁 ∈ ℂ) |
25 | | expineg2 10295 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
26 | 6, 10, 24, 8, 25 | syl22anc 1217 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) |
27 | 26 | fveq2d 5418 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘(𝐴↑𝑁)) = (abs‘(1 / (𝐴↑-𝑁)))) |
28 | | abscl 10816 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
29 | 28 | ad2antrr 479 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘𝐴) ∈
ℝ) |
30 | 29 | recnd 7787 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘𝐴) ∈
ℂ) |
31 | | abs00ap 10827 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) # 0 ↔
𝐴 # 0)) |
32 | 31 | ad2antrr 479 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((abs‘𝐴) # 0 ↔ 𝐴 # 0)) |
33 | 10, 32 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘𝐴) # 0) |
34 | | expineg2 10295 |
. . . . . . 7
⊢
((((abs‘𝐴)
∈ ℂ ∧ (abs‘𝐴) # 0) ∧ (𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)) →
((abs‘𝐴)↑𝑁) = (1 / ((abs‘𝐴)↑-𝑁))) |
35 | 30, 33, 24, 8, 34 | syl22anc 1217 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → ((abs‘𝐴)↑𝑁) = (1 / ((abs‘𝐴)↑-𝑁))) |
36 | 22, 27, 35 | 3eqtr4d 2180 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
37 | 36 | ex 114 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
38 | 4, 37 | jaod 706 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁))) |
39 | 38 | 3impia 1178 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ))) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
40 | 1, 39 | syl3an3b 1254 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |