| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | eqid 2737 |
. 2
⊢
(ℤ≥‘(⌊‘(2 ·
(abs‘𝐴)))) =
(ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) |
| 3 | | halfre 12480 |
. . 3
⊢ (1 / 2)
∈ ℝ |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ → (1 / 2)
∈ ℝ) |
| 5 | | halflt1 12484 |
. . 3
⊢ (1 / 2)
< 1 |
| 6 | 5 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ → (1 / 2)
< 1) |
| 7 | | 2re 12340 |
. . . 4
⊢ 2 ∈
ℝ |
| 8 | | abscl 15317 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
| 9 | | remulcl 11240 |
. . . 4
⊢ ((2
∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) → (2 ·
(abs‘𝐴)) ∈
ℝ) |
| 10 | 7, 8, 9 | sylancr 587 |
. . 3
⊢ (𝐴 ∈ ℂ → (2
· (abs‘𝐴))
∈ ℝ) |
| 11 | 7 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ) |
| 12 | | 0le2 12368 |
. . . . 5
⊢ 0 ≤
2 |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
2) |
| 14 | | absge0 15326 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
| 15 | 11, 8, 13, 14 | mulge0d 11840 |
. . 3
⊢ (𝐴 ∈ ℂ → 0 ≤ (2
· (abs‘𝐴))) |
| 16 | | flge0nn0 13860 |
. . 3
⊢ (((2
· (abs‘𝐴))
∈ ℝ ∧ 0 ≤ (2 · (abs‘𝐴))) → (⌊‘(2 ·
(abs‘𝐴))) ∈
ℕ0) |
| 17 | 10, 15, 16 | syl2anc 584 |
. 2
⊢ (𝐴 ∈ ℂ →
(⌊‘(2 · (abs‘𝐴))) ∈
ℕ0) |
| 18 | | eftval.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) |
| 19 | 18 | eftval 16112 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
| 20 | 19 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
| 21 | | eftcl 16109 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) |
| 22 | 20, 21 | eqeltrd 2841 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) ∈
ℂ) |
| 23 | 8 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈
ℝ) |
| 24 | | eluznn0 12959 |
. . . . . . 7
⊢
(((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0) |
| 25 | 17, 24 | sylan 580 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0) |
| 26 | | nn0p1nn 12565 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℕ) |
| 28 | 23, 27 | nndivred 12320 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) ∈ ℝ) |
| 29 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 / 2) ∈
ℝ) |
| 30 | 23, 25 | reexpcld 14203 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
| 31 | 25 | faccld 14323 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℕ) |
| 32 | 30, 31 | nndivred 12320 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
| 33 | | expcl 14120 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
| 34 | 25, 33 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑𝑘) ∈ ℂ) |
| 35 | 34 | absge0d 15483 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(abs‘(𝐴↑𝑘))) |
| 36 | | absexp 15343 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
| 37 | 25, 36 | syldan 591 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
| 38 | 35, 37 | breqtrd 5169 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
((abs‘𝐴)↑𝑘)) |
| 39 | 31 | nnred 12281 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℝ) |
| 40 | 31 | nngt0d 12315 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 <
(!‘𝑘)) |
| 41 | | divge0 12137 |
. . . . 5
⊢
(((((abs‘𝐴)↑𝑘) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑘)) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 <
(!‘𝑘))) → 0 ≤
(((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
| 42 | 30, 38, 39, 40, 41 | syl22anc 839 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
| 43 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) ∈
ℝ) |
| 44 | | peano2nn0 12566 |
. . . . . . . . . . 11
⊢
((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈
ℕ0) |
| 45 | 17, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈
ℕ0) |
| 46 | 45 | nn0red 12588 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℝ) |
| 47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((⌊‘(2
· (abs‘𝐴))) +
1) ∈ ℝ) |
| 48 | 27 | nnred 12281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℝ) |
| 49 | | flltp1 13840 |
. . . . . . . . 9
⊢ ((2
· (abs‘𝐴))
∈ ℝ → (2 · (abs‘𝐴)) < ((⌊‘(2 ·
(abs‘𝐴))) +
1)) |
| 50 | 43, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) <
((⌊‘(2 · (abs‘𝐴))) + 1)) |
| 51 | | eluzp1p1 12906 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) → (𝑘 + 1) ∈
(ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1))) |
| 52 | 51 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
(ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1))) |
| 53 | | eluzle 12891 |
. . . . . . . . 9
⊢ ((𝑘 + 1) ∈
(ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1)) →
((⌊‘(2 · (abs‘𝐴))) + 1) ≤ (𝑘 + 1)) |
| 54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((⌊‘(2
· (abs‘𝐴))) +
1) ≤ (𝑘 +
1)) |
| 55 | 43, 47, 48, 50, 54 | ltletrd 11421 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) < (𝑘 + 1)) |
| 56 | 23 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈
ℂ) |
| 57 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 58 | | mulcom 11241 |
. . . . . . . 8
⊢
(((abs‘𝐴)
∈ ℂ ∧ 2 ∈ ℂ) → ((abs‘𝐴) · 2) = (2 · (abs‘𝐴))) |
| 59 | 56, 57, 58 | sylancl 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) = (2 ·
(abs‘𝐴))) |
| 60 | 27 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℂ) |
| 61 | 60 | mullidd 11279 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 · (𝑘 + 1)) = (𝑘 + 1)) |
| 62 | 55, 59, 61 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) < (1 ·
(𝑘 + 1))) |
| 63 | | 2rp 13039 |
. . . . . . . 8
⊢ 2 ∈
ℝ+ |
| 64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 2 ∈
ℝ+) |
| 65 | | 1red 11262 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 1 ∈
ℝ) |
| 66 | 27 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
ℝ+) |
| 67 | 23, 64, 65, 66 | lt2mul2divd 13146 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴) · 2) < (1 ·
(𝑘 + 1)) ↔
((abs‘𝐴) / (𝑘 + 1)) < (1 /
2))) |
| 68 | 62, 67 | mpbid 232 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) < (1 / 2)) |
| 69 | | ltle 11349 |
. . . . . 6
⊢
((((abs‘𝐴) /
(𝑘 + 1)) ∈ ℝ
∧ (1 / 2) ∈ ℝ) → (((abs‘𝐴) / (𝑘 + 1)) < (1 / 2) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2))) |
| 70 | 28, 3, 69 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴) / (𝑘 + 1)) < (1 / 2) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2))) |
| 71 | 68, 70 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2)) |
| 72 | 28, 29, 32, 42, 71 | lemul2ad 12208 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) ≤ ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
| 73 | | peano2nn0 12566 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
| 74 | 25, 73 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
ℕ0) |
| 75 | 18 | eftval 16112 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ ℕ0
→ (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) |
| 76 | 74, 75 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) |
| 77 | 76 | fveq2d 6910 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1))))) |
| 78 | | absexp 15343 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1))) |
| 79 | 74, 78 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1))) |
| 80 | 56, 25 | expp1d 14187 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑(𝑘 + 1)) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴))) |
| 81 | 79, 80 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴))) |
| 82 | 74 | faccld 14323 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℕ) |
| 83 | 82 | nnred 12281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℝ) |
| 84 | 82 | nnnn0d 12587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℕ0) |
| 85 | 84 | nn0ge0d 12590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(!‘(𝑘 +
1))) |
| 86 | 83, 85 | absidd 15461 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) →
(abs‘(!‘(𝑘 +
1))) = (!‘(𝑘 +
1))) |
| 87 | | facp1 14317 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
| 88 | 25, 87 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
| 89 | 86, 88 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) →
(abs‘(!‘(𝑘 +
1))) = ((!‘𝑘)
· (𝑘 +
1))) |
| 90 | 81, 89 | oveq12d 7449 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1)))) |
| 91 | | expcl 14120 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐴↑(𝑘 + 1)) ∈ ℂ) |
| 92 | 74, 91 | syldan 591 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑(𝑘 + 1)) ∈ ℂ) |
| 93 | 82 | nncnd 12282 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℂ) |
| 94 | 82 | nnne0d 12316 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ≠ 0) |
| 95 | 92, 93, 94 | absdivd 15494 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1))))) |
| 96 | 30 | recnd 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℂ) |
| 97 | 31 | nncnd 12282 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℂ) |
| 98 | 31 | nnne0d 12316 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ≠ 0) |
| 99 | 27 | nnne0d 12316 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ≠ 0) |
| 100 | 96, 97, 56, 60, 98, 99 | divmuldivd 12084 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1)))) |
| 101 | 90, 95, 100 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1)))) |
| 102 | 77, 101 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1)))) |
| 103 | | halfcn 12481 |
. . . . 5
⊢ (1 / 2)
∈ ℂ |
| 104 | 25, 22 | syldan 591 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) ∈ ℂ) |
| 105 | 104 | abscld 15475 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
| 106 | 105 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℂ) |
| 107 | | mulcom 11241 |
. . . . 5
⊢ (((1 / 2)
∈ ℂ ∧ (abs‘(𝐹‘𝑘)) ∈ ℂ) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2))) |
| 108 | 103, 106,
107 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2))) |
| 109 | 25, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
| 110 | 109 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (abs‘((𝐴↑𝑘) / (!‘𝑘)))) |
| 111 | | eftabs 16111 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
| 112 | 25, 111 | syldan 591 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
| 113 | 110, 112 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
| 114 | 113 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐹‘𝑘)) · (1 / 2)) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
| 115 | 108, 114 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
| 116 | 72, 102, 115 | 3brtr4d 5175 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((1 / 2) ·
(abs‘(𝐹‘𝑘)))) |
| 117 | 1, 2, 4, 6, 17, 22, 116 | cvgrat 15919 |
1
⊢ (𝐴 ∈ ℂ → seq0( + ,
𝐹) ∈ dom ⇝
) |