Step | Hyp | Ref
| Expression |
1 | | nn0uz 12374 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | eqid 2739 |
. 2
⊢
(ℤ≥‘(⌊‘(2 ·
(abs‘𝐴)))) =
(ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) |
3 | | halfre 11942 |
. . 3
⊢ (1 / 2)
∈ ℝ |
4 | 3 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ → (1 / 2)
∈ ℝ) |
5 | | halflt1 11946 |
. . 3
⊢ (1 / 2)
< 1 |
6 | 5 | a1i 11 |
. 2
⊢ (𝐴 ∈ ℂ → (1 / 2)
< 1) |
7 | | 2re 11802 |
. . . 4
⊢ 2 ∈
ℝ |
8 | | abscl 14740 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
9 | | remulcl 10712 |
. . . 4
⊢ ((2
∈ ℝ ∧ (abs‘𝐴) ∈ ℝ) → (2 ·
(abs‘𝐴)) ∈
ℝ) |
10 | 7, 8, 9 | sylancr 590 |
. . 3
⊢ (𝐴 ∈ ℂ → (2
· (abs‘𝐴))
∈ ℝ) |
11 | 7 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ) |
12 | | 0le2 11830 |
. . . . 5
⊢ 0 ≤
2 |
13 | 12 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
2) |
14 | | absge0 14749 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
15 | 11, 8, 13, 14 | mulge0d 11307 |
. . 3
⊢ (𝐴 ∈ ℂ → 0 ≤ (2
· (abs‘𝐴))) |
16 | | flge0nn0 13293 |
. . 3
⊢ (((2
· (abs‘𝐴))
∈ ℝ ∧ 0 ≤ (2 · (abs‘𝐴))) → (⌊‘(2 ·
(abs‘𝐴))) ∈
ℕ0) |
17 | 10, 15, 16 | syl2anc 587 |
. 2
⊢ (𝐴 ∈ ℂ →
(⌊‘(2 · (abs‘𝐴))) ∈
ℕ0) |
18 | | eftval.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) |
19 | 18 | eftval 15534 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
20 | 19 | adantl 485 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
21 | | eftcl 15531 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) |
22 | 20, 21 | eqeltrd 2834 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) ∈
ℂ) |
23 | 8 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈
ℝ) |
24 | | eluznn0 12411 |
. . . . . . 7
⊢
(((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0) |
25 | 17, 24 | sylan 583 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 𝑘 ∈ ℕ0) |
26 | | nn0p1nn 12027 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℕ) |
28 | 23, 27 | nndivred 11782 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) ∈ ℝ) |
29 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 / 2) ∈
ℝ) |
30 | 23, 25 | reexpcld 13631 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
31 | 25 | faccld 13748 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℕ) |
32 | 30, 31 | nndivred 11782 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
33 | | expcl 13551 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
34 | 25, 33 | syldan 594 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑𝑘) ∈ ℂ) |
35 | 34 | absge0d 14906 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(abs‘(𝐴↑𝑘))) |
36 | | absexp 14766 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
37 | 25, 36 | syldan 594 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
38 | 35, 37 | breqtrd 5066 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
((abs‘𝐴)↑𝑘)) |
39 | 31 | nnred 11743 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℝ) |
40 | 31 | nngt0d 11777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 <
(!‘𝑘)) |
41 | | divge0 11599 |
. . . . 5
⊢
(((((abs‘𝐴)↑𝑘) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑘)) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 <
(!‘𝑘))) → 0 ≤
(((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
42 | 30, 38, 39, 40, 41 | syl22anc 838 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
43 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) ∈
ℝ) |
44 | | peano2nn0 12028 |
. . . . . . . . . . 11
⊢
((⌊‘(2 · (abs‘𝐴))) ∈ ℕ0 →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈
ℕ0) |
45 | 17, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈
ℕ0) |
46 | 45 | nn0red 12049 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((⌊‘(2 · (abs‘𝐴))) + 1) ∈ ℝ) |
47 | 46 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((⌊‘(2
· (abs‘𝐴))) +
1) ∈ ℝ) |
48 | 27 | nnred 11743 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℝ) |
49 | | flltp1 13273 |
. . . . . . . . 9
⊢ ((2
· (abs‘𝐴))
∈ ℝ → (2 · (abs‘𝐴)) < ((⌊‘(2 ·
(abs‘𝐴))) +
1)) |
50 | 43, 49 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) <
((⌊‘(2 · (abs‘𝐴))) + 1)) |
51 | | eluzp1p1 12364 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴)))) → (𝑘 + 1) ∈
(ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1))) |
52 | 51 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
(ℤ≥‘((⌊‘(2 · (abs‘𝐴))) + 1))) |
53 | | eluzle 12349 |
. . . . . . . . 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 10890 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (2 ·
(abs‘𝐴)) < (𝑘 + 1)) |
56 | 23 | recnd 10759 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘𝐴) ∈
ℂ) |
57 | | 2cn 11803 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
58 | | mulcom 10713 |
. . . . . . . 8
⊢
(((abs‘𝐴)
∈ ℂ ∧ 2 ∈ ℂ) → ((abs‘𝐴) · 2) = (2 · (abs‘𝐴))) |
59 | 56, 57, 58 | sylancl 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) = (2 ·
(abs‘𝐴))) |
60 | 27 | nncnd 11744 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈ ℂ) |
61 | 60 | mulid2d 10749 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (1 · (𝑘 + 1)) = (𝑘 + 1)) |
62 | 55, 59, 61 | 3brtr4d 5072 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) · 2) < (1 ·
(𝑘 + 1))) |
63 | | 2rp 12489 |
. . . . . . . 8
⊢ 2 ∈
ℝ+ |
64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 2 ∈
ℝ+) |
65 | | 1red 10732 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 1 ∈
ℝ) |
66 | 27 | nnrpd 12524 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
ℝ+) |
67 | 23, 64, 65, 66 | lt2mul2divd 12595 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (((abs‘𝐴) · 2) < (1 ·
(𝑘 + 1)) ↔
((abs‘𝐴) / (𝑘 + 1)) < (1 /
2))) |
68 | 62, 67 | mpbid 235 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴) / (𝑘 + 1)) < (1 / 2)) |
69 | | ltle 10819 |
. . . . . 6
⊢
((((abs‘𝐴) /
(𝑘 + 1)) ∈ ℝ
∧ (1 / 2) ∈ ℝ) → (((abs‘𝐴) / (𝑘 + 1)) < (1 / 2) → ((abs‘𝐴) / (𝑘 + 1)) ≤ (1 / 2))) |
70 | 28, 3, 69 | sylancl 589 |
. . . . 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 11670 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) ≤ ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
73 | | peano2nn0 12028 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
74 | 25, 73 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ∈
ℕ0) |
75 | 18 | eftval 15534 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ ℕ0
→ (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) |
76 | 74, 75 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘(𝑘 + 1)) = ((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) |
77 | 76 | fveq2d 6690 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1))))) |
78 | | absexp 14766 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1))) |
79 | 74, 78 | syldan 594 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = ((abs‘𝐴)↑(𝑘 + 1))) |
80 | 56, 25 | expp1d 13615 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑(𝑘 + 1)) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴))) |
81 | 79, 80 | eqtrd 2774 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐴↑(𝑘 + 1))) = (((abs‘𝐴)↑𝑘) · (abs‘𝐴))) |
82 | 74 | faccld 13748 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℕ) |
83 | 82 | nnred 11743 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℝ) |
84 | 82 | nnnn0d 12048 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℕ0) |
85 | 84 | nn0ge0d 12051 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → 0 ≤
(!‘(𝑘 +
1))) |
86 | 83, 85 | absidd 14884 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) →
(abs‘(!‘(𝑘 +
1))) = (!‘(𝑘 +
1))) |
87 | | facp1 13742 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
88 | 25, 87 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
89 | 86, 88 | eqtrd 2774 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) →
(abs‘(!‘(𝑘 +
1))) = ((!‘𝑘)
· (𝑘 +
1))) |
90 | 81, 89 | oveq12d 7200 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1)))) |
91 | | expcl 13551 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐴↑(𝑘 + 1)) ∈ ℂ) |
92 | 74, 91 | syldan 594 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐴↑(𝑘 + 1)) ∈ ℂ) |
93 | 82 | nncnd 11744 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ∈
ℂ) |
94 | 82 | nnne0d 11778 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘(𝑘 + 1)) ≠ 0) |
95 | 92, 93, 94 | absdivd 14917 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((abs‘(𝐴↑(𝑘 + 1))) / (abs‘(!‘(𝑘 + 1))))) |
96 | 30 | recnd 10759 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘𝐴)↑𝑘) ∈ ℂ) |
97 | 31 | nncnd 11744 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ∈
ℂ) |
98 | 31 | nnne0d 11778 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (!‘𝑘) ≠ 0) |
99 | 27 | nnne0d 11778 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝑘 + 1) ≠ 0) |
100 | 96, 97, 56, 60, 98, 99 | divmuldivd 11547 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) · (abs‘𝐴)) / ((!‘𝑘) · (𝑘 + 1)))) |
101 | 90, 95, 100 | 3eqtr4d 2784 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑(𝑘 + 1)) / (!‘(𝑘 + 1)))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1)))) |
102 | 77, 101 | eqtrd 2774 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · ((abs‘𝐴) / (𝑘 + 1)))) |
103 | | halfcn 11943 |
. . . . 5
⊢ (1 / 2)
∈ ℂ |
104 | 25, 22 | syldan 594 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) ∈ ℂ) |
105 | 104 | abscld 14898 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
106 | 105 | recnd 10759 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) ∈ ℂ) |
107 | | mulcom 10713 |
. . . . 5
⊢ (((1 / 2)
∈ ℂ ∧ (abs‘(𝐹‘𝑘)) ∈ ℂ) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2))) |
108 | 103, 106,
107 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((abs‘(𝐹‘𝑘)) · (1 / 2))) |
109 | 25, 19 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
110 | 109 | fveq2d 6690 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (abs‘((𝐴↑𝑘) / (!‘𝑘)))) |
111 | | eftabs 15533 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
112 | 25, 111 | syldan 594 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
113 | 110, 112 | eqtrd 2774 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘𝑘)) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
114 | 113 | oveq1d 7197 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((abs‘(𝐹‘𝑘)) · (1 / 2)) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
115 | 108, 114 | eqtrd 2774 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → ((1 / 2) ·
(abs‘(𝐹‘𝑘))) = ((((abs‘𝐴)↑𝑘) / (!‘𝑘)) · (1 / 2))) |
116 | 72, 102, 115 | 3brtr4d 5072 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈
(ℤ≥‘(⌊‘(2 · (abs‘𝐴))))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((1 / 2) ·
(abs‘(𝐹‘𝑘)))) |
117 | 1, 2, 4, 6, 17, 22, 116 | cvgrat 15343 |
1
⊢ (𝐴 ∈ ℂ → seq0( + ,
𝐹) ∈ dom ⇝
) |