Step | Hyp | Ref
| Expression |
1 | | eftl.5 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
2 | | eftl.4 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnnn0d 12293 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | | eftl.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) |
5 | 4 | eftlcl 15816 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
6 | 1, 3, 5 | syl2anc 584 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) |
7 | 6 | abscld 15148 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ∈ ℝ) |
8 | 1 | abscld 15148 |
. . 3
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
9 | | eftl.2 |
. . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛))) |
10 | 9 | reeftlcl 15817 |
. . 3
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑀
∈ ℕ0) → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ ℝ) |
11 | 8, 3, 10 | syl2anc 584 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ ℝ) |
12 | 8, 3 | reexpcld 13881 |
. . 3
⊢ (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ) |
13 | | peano2nn0 12273 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
14 | 3, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
15 | 14 | nn0red 12294 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
16 | 3 | faccld 13998 |
. . . . 5
⊢ (𝜑 → (!‘𝑀) ∈ ℕ) |
17 | 16, 2 | nnmulcld 12026 |
. . . 4
⊢ (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ) |
18 | 15, 17 | nndivred 12027 |
. . 3
⊢ (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ) |
19 | 12, 18 | remulcld 11005 |
. 2
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ) |
20 | | eqid 2738 |
. . 3
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
21 | 2 | nnzd 12425 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
22 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
23 | | eluznn0 12657 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
24 | 3, 23 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
25 | 4 | eftval 15786 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) |
27 | | eftcl 15783 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) |
28 | 1, 27 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) |
29 | 26, 28 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ) |
30 | 24, 29 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
31 | 4 | eftlcvg 15815 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ seq𝑀( + , 𝐹) ∈ dom ⇝
) |
32 | 1, 3, 31 | syl2anc 584 |
. . . 4
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
33 | 20, 21, 22, 30, 32 | isumclim2 15470 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘)) |
34 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
35 | 9 | eftval 15786 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
36 | 35 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
37 | | reeftcl 15784 |
. . . . . . . 8
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
38 | 8, 37 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) |
39 | 36, 38 | eqeltrd 2839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℝ) |
40 | 24, 39 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℝ) |
41 | 40 | recnd 11003 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) |
42 | 8 | recnd 11003 |
. . . . 5
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) |
43 | 9 | eftlcvg 15815 |
. . . . 5
⊢
(((abs‘𝐴)
∈ ℂ ∧ 𝑀
∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ ) |
44 | 42, 3, 43 | syl2anc 584 |
. . . 4
⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) |
45 | 20, 21, 34, 41, 44 | isumclim2 15470 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
46 | | eftabs 15785 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
47 | 1, 46 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) |
48 | 26 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝐹‘𝑘)) = (abs‘((𝐴↑𝑘) / (!‘𝑘)))) |
49 | 47, 48, 36 | 3eqtr4rd 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) |
50 | 24, 49 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) |
51 | 20, 33, 45, 21, 30, 50 | iserabs 15527 |
. 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
52 | | nn0uz 12620 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
53 | | 0zd 12331 |
. . . 4
⊢ (𝜑 → 0 ∈
ℤ) |
54 | 2 | nncnd 11989 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℂ) |
55 | | nn0cn 12243 |
. . . . 5
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) |
56 | | nn0ex 12239 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
57 | 56 | mptex 7099 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V |
58 | 9, 57 | eqeltri 2835 |
. . . . . 6
⊢ 𝐺 ∈ V |
59 | 58 | shftval4 14788 |
. . . . 5
⊢ ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗))) |
60 | 54, 55, 59 | syl2an 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗))) |
61 | | nn0addcl 12268 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (𝑀 + 𝑗) ∈
ℕ0) |
62 | 3, 61 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈
ℕ0) |
63 | 9 | eftval 15786 |
. . . . . 6
⊢ ((𝑀 + 𝑗) ∈ ℕ0 → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗)))) |
64 | 62, 63 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗)))) |
65 | 8 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
66 | | reeftcl 15784 |
. . . . . 6
⊢
(((abs‘𝐴)
∈ ℝ ∧ (𝑀 +
𝑗) ∈
ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ) |
67 | 65, 62, 66 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ) |
68 | 64, 67 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ) |
69 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗)) |
70 | 69 | oveq2d 7291 |
. . . . . 6
⊢ (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
71 | | eftl.3 |
. . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛))) |
72 | | ovex 7308 |
. . . . . 6
⊢
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ V |
73 | 70, 71, 72 | fvmpt 6875 |
. . . . 5
⊢ (𝑗 ∈ ℕ0
→ (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
74 | 73 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
75 | 12, 16 | nndivred 12027 |
. . . . . 6
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ) |
76 | 75 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ) |
77 | 2 | peano2nnd 11990 |
. . . . . . 7
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
78 | 77 | nnrecred 12024 |
. . . . . 6
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ) |
79 | | reexpcl 13799 |
. . . . . 6
⊢ (((1 /
(𝑀 + 1)) ∈ ℝ
∧ 𝑗 ∈
ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ) |
80 | 78, 79 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) ∈
ℝ) |
81 | 76, 80 | remulcld 11005 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ) |
82 | 65, 62 | reexpcld 13881 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ) |
83 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ∈
ℝ) |
84 | 62 | faccld 13998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℕ) |
85 | 84 | nnred 11988 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℝ) |
86 | 85, 81 | remulcld 11005 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ) |
87 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑀 ∈
ℕ0) |
88 | | uzid 12597 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
89 | 21, 88 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
90 | | uzaddcl 12644 |
. . . . . . . . 9
⊢ ((𝑀 ∈
(ℤ≥‘𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ≥‘𝑀)) |
91 | 89, 90 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ≥‘𝑀)) |
92 | 1 | absge0d 15156 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) |
93 | 92 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
94 | | eftl.6 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝐴) ≤ 1) |
95 | 94 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ≤
1) |
96 | 65, 87, 91, 93, 95 | leexp2rd 13972 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀)) |
97 | 16 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ∈
ℕ) |
98 | | nnexpcl 13795 |
. . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((𝑀 + 1)↑𝑗) ∈
ℕ) |
99 | 77, 98 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ) |
100 | 97, 99 | nnmulcld 12026 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℕ) |
101 | 100 | nnred 11988 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℝ) |
102 | 8, 3, 92 | expge0d 13882 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀)) |
103 | 12, 102 | jca 512 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) |
104 | 103 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) |
105 | | faclbnd6 14013 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) |
106 | 3, 105 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) |
107 | | lemul1a 11829 |
. . . . . . . . . 10
⊢
(((((!‘𝑀)
· ((𝑀 +
1)↑𝑗)) ∈ ℝ
∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧
(((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀))) |
108 | 101, 85, 104, 106, 107 | syl31anc 1372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀))) |
109 | 85, 83 | remulcld 11005 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ) |
110 | 100 | nnrpd 12770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℝ+) |
111 | 83, 109, 110 | lemuldiv2d 12822 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))) |
112 | 108, 111 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) |
113 | 84 | nncnd 11989 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℂ) |
114 | 12 | recnd 11003 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ) |
115 | 114 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ∈
ℂ) |
116 | 100 | nncnd 11989 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℂ) |
117 | 100 | nnne0d 12023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ≠ 0) |
118 | 113, 115,
116, 117 | divassd 11786 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))) |
119 | 77 | nncnd 11989 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) |
120 | 119 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ∈
ℂ) |
121 | 77 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ∈
ℕ) |
122 | 121 | nnne0d 12023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ≠ 0) |
123 | | nn0z 12343 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℤ) |
124 | 123 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℤ) |
125 | 120, 122,
124 | exprecd 13872 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗))) |
126 | 125 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗)))) |
127 | 75 | recnd 11003 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ) |
128 | 127 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ) |
129 | 99 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ) |
130 | 99 | nnne0d 12023 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ≠ 0) |
131 | 128, 129,
130 | divrecd 11754 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗)))) |
132 | 16 | nncnd 11989 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (!‘𝑀) ∈ ℂ) |
133 | 132 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ∈
ℂ) |
134 | | facne0 14000 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ≠
0) |
135 | 3, 134 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (!‘𝑀) ≠ 0) |
136 | 135 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ≠
0) |
137 | 115, 133,
129, 136, 130 | divdiv1d 11782 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) |
138 | 126, 131,
137 | 3eqtr2rd 2785 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
139 | 138 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) |
140 | 118, 139 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) |
141 | 112, 140 | breqtrd 5100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) |
142 | 82, 83, 86, 96, 141 | letrd 11132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) |
143 | 84 | nngt0d 12022 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 <
(!‘(𝑀 + 𝑗))) |
144 | | ledivmul 11851 |
. . . . . . 7
⊢
((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 <
(!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))) |
145 | 82, 81, 85, 143, 144 | syl112anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))) |
146 | 142, 145 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
147 | 64, 146 | eqbrtrd 5096 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
148 | | 0z 12330 |
. . . . . 6
⊢ 0 ∈
ℤ |
149 | 21 | znegcld 12428 |
. . . . . 6
⊢ (𝜑 → -𝑀 ∈ ℤ) |
150 | 58 | seqshft 14796 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ -𝑀
∈ ℤ) → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀)) |
151 | 148, 149,
150 | sylancr 587 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀)) |
152 | | 0cn 10967 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℂ |
153 | | subneg 11270 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℂ ∧ 𝑀
∈ ℂ) → (0 − -𝑀) = (0 + 𝑀)) |
154 | 152, 153 | mpan 687 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℂ → (0
− -𝑀) = (0 + 𝑀)) |
155 | | addid2 11158 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℂ → (0 +
𝑀) = 𝑀) |
156 | 154, 155 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℂ → (0
− -𝑀) = 𝑀) |
157 | 54, 156 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0 − -𝑀) = 𝑀) |
158 | 157 | seqeq1d 13727 |
. . . . . . . 8
⊢ (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺)) |
159 | 158, 45 | eqbrtrd 5096 |
. . . . . . 7
⊢ (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
160 | | seqex 13723 |
. . . . . . . 8
⊢ seq(0
− -𝑀)( + , 𝐺) ∈ V |
161 | | climshft 15285 |
. . . . . . . 8
⊢ ((-𝑀 ∈ ℤ ∧ seq(0
− -𝑀)( + , 𝐺) ∈ V) → ((seq(0
− -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘))) |
162 | 149, 160,
161 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘))) |
163 | 159, 162 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
164 | | ovex 7308 |
. . . . . . 7
⊢ (seq(0
− -𝑀)( + , 𝐺) shift -𝑀) ∈ V |
165 | | sumex 15399 |
. . . . . . 7
⊢
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐺‘𝑘) ∈ V |
166 | 164, 165 | breldm 5817 |
. . . . . 6
⊢ ((seq(0
− -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ ) |
167 | 163, 166 | syl 17 |
. . . . 5
⊢ (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ ) |
168 | 151, 167 | eqeltrd 2839 |
. . . 4
⊢ (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ ) |
169 | 2 | nnge1d 12021 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ 𝑀) |
170 | | 1nn 11984 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
171 | | nnleltp1 12375 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ ∧ 𝑀
∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1))) |
172 | 170, 2, 171 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1))) |
173 | 169, 172 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (𝑀 + 1)) |
174 | 14 | nn0ge0d 12296 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑀 + 1)) |
175 | 15, 174 | absidd 15134 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1)) |
176 | 173, 175 | breqtrrd 5102 |
. . . . . . . 8
⊢ (𝜑 → 1 < (abs‘(𝑀 + 1))) |
177 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛)) = (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛)) |
178 | | ovex 7308 |
. . . . . . . . . 10
⊢ ((1 /
(𝑀 + 1))↑𝑗) ∈ V |
179 | 69, 177, 178 | fvmpt 6875 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗)) |
180 | 179 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗)) |
181 | 119, 176,
180 | georeclim 15584 |
. . . . . . 7
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))) ⇝
((𝑀 + 1) / ((𝑀 + 1) −
1))) |
182 | 80 | recnd 11003 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) ∈
ℂ) |
183 | 180, 182 | eqeltrd 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))‘𝑗) ∈
ℂ) |
184 | 180 | oveq2d 7291 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 /
(𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
185 | 74, 184 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 /
(𝑀 + 1))↑𝑛))‘𝑗))) |
186 | 52, 53, 127, 181, 183, 185 | isermulc2 15369 |
. . . . . 6
⊢ (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1)))) |
187 | | ax-1cn 10929 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
188 | | pncan 11227 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
189 | 54, 187, 188 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
190 | 189 | oveq2d 7291 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀)) |
191 | 190 | oveq2d 7291 |
. . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀))) |
192 | 15, 2 | nndivred 12027 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ) |
193 | 192 | recnd 11003 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ) |
194 | 114, 193,
132, 135 | div23d 11788 |
. . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀))) |
195 | 191, 194 | eqtr4d 2781 |
. . . . . . 7
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀))) |
196 | 114, 193,
132, 135 | divassd 11786 |
. . . . . . 7
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀)))) |
197 | 2 | nnne0d 12023 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) |
198 | 119, 54, 132, 197, 135 | divdiv1d 11782 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀)))) |
199 | 54, 132 | mulcomd 10996 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀)) |
200 | 199 | oveq2d 7291 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) |
201 | 198, 200 | eqtrd 2778 |
. . . . . . . 8
⊢ (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) |
202 | 201 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
203 | 195, 196,
202 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
204 | 186, 203 | breqtrd 5100 |
. . . . 5
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
205 | | seqex 13723 |
. . . . . 6
⊢ seq0( + ,
𝐻) ∈
V |
206 | | ovex 7308 |
. . . . . 6
⊢
(((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ V |
207 | 205, 206 | breldm 5817 |
. . . . 5
⊢ (seq0( +
, 𝐻) ⇝
(((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) → seq0( + , 𝐻) ∈ dom ⇝ ) |
208 | 204, 207 | syl 17 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝
) |
209 | 52, 53, 60, 68, 74, 81, 147, 168, 208 | isumle 15556 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) |
210 | | eqid 2738 |
. . . . 5
⊢
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘(0 +
𝑀)) |
211 | | fveq2 6774 |
. . . . 5
⊢ (𝑘 = (𝑀 + 𝑗) → (𝐺‘𝑘) = (𝐺‘(𝑀 + 𝑗))) |
212 | 54 | addid2d 11176 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
213 | 212 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀)) |
214 | 213 | eleq2d 2824 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(0 +
𝑀)) ↔ 𝑘 ∈
(ℤ≥‘𝑀))) |
215 | 214 | biimpa 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
𝑀))) → 𝑘 ∈
(ℤ≥‘𝑀)) |
216 | 215, 41 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
𝑀))) → (𝐺‘𝑘) ∈ ℂ) |
217 | 52, 210, 211, 21, 53, 216 | isumshft 15551 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(0 +
𝑀))(𝐺‘𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗))) |
218 | 213 | sumeq1d 15413 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(0 +
𝑀))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
219 | 217, 218 | eqtr3d 2780 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) |
220 | 81 | recnd 11003 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ) |
221 | 52, 53, 74, 220, 204 | isumclim 15469 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
222 | 209, 219,
221 | 3brtr3d 5105 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |
223 | 7, 11, 19, 51, 222 | letrd 11132 |
1
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |