| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eftl.5 | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 2 |  | eftl.4 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 3 | 2 | nnnn0d 12589 | . . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 4 |  | eftl.1 | . . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) | 
| 5 | 4 | eftlcl 16144 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) | 
| 6 | 1, 3, 5 | syl2anc 584 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ) | 
| 7 | 6 | abscld 15476 | . 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ∈ ℝ) | 
| 8 | 1 | abscld 15476 | . . 3
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) | 
| 9 |  | eftl.2 | . . . 4
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦
(((abs‘𝐴)↑𝑛) / (!‘𝑛))) | 
| 10 | 9 | reeftlcl 16145 | . . 3
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑀
∈ ℕ0) → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ ℝ) | 
| 11 | 8, 3, 10 | syl2anc 584 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ ℝ) | 
| 12 | 8, 3 | reexpcld 14204 | . . 3
⊢ (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ) | 
| 13 |  | peano2nn0 12568 | . . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) | 
| 14 | 3, 13 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) | 
| 15 | 14 | nn0red 12590 | . . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) | 
| 16 | 3 | faccld 14324 | . . . . 5
⊢ (𝜑 → (!‘𝑀) ∈ ℕ) | 
| 17 | 16, 2 | nnmulcld 12320 | . . . 4
⊢ (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ) | 
| 18 | 15, 17 | nndivred 12321 | . . 3
⊢ (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ) | 
| 19 | 12, 18 | remulcld 11292 | . 2
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ) | 
| 20 |  | eqid 2736 | . . 3
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) | 
| 21 | 2 | nnzd 12642 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 22 |  | eqidd 2737 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 23 |  | eluznn0 12960 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) | 
| 24 | 3, 23 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) | 
| 25 | 4 | eftval 16113 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) | 
| 26 | 25 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((𝐴↑𝑘) / (!‘𝑘))) | 
| 27 |  | eftcl 16110 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 28 | 1, 27 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 29 | 26, 28 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ) | 
| 30 | 24, 29 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) | 
| 31 | 4 | eftlcvg 16143 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ seq𝑀( + , 𝐹) ∈ dom ⇝
) | 
| 32 | 1, 3, 31 | syl2anc 584 | . . . 4
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | 
| 33 | 20, 21, 22, 30, 32 | isumclim2 15795 | . . 3
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘)) | 
| 34 |  | eqidd 2737 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑘)) | 
| 35 | 9 | eftval 16113 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) | 
| 36 | 35 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) | 
| 37 |  | reeftcl 16111 | . . . . . . . 8
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 38 | 8, 37 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ) | 
| 39 | 36, 38 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℝ) | 
| 40 | 24, 39 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℝ) | 
| 41 | 40 | recnd 11290 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) | 
| 42 | 8 | recnd 11290 | . . . . 5
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) | 
| 43 | 9 | eftlcvg 16143 | . . . . 5
⊢
(((abs‘𝐴)
∈ ℂ ∧ 𝑀
∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | 
| 44 | 42, 3, 43 | syl2anc 584 | . . . 4
⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | 
| 45 | 20, 21, 34, 41, 44 | isumclim2 15795 | . . 3
⊢ (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 46 |  | eftabs 16112 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) | 
| 47 | 1, 46 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐴↑𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘))) | 
| 48 | 26 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝐹‘𝑘)) = (abs‘((𝐴↑𝑘) / (!‘𝑘)))) | 
| 49 | 47, 48, 36 | 3eqtr4rd 2787 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) | 
| 50 | 24, 49 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) = (abs‘(𝐹‘𝑘))) | 
| 51 | 20, 33, 45, 21, 30, 50 | iserabs 15852 | . 2
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 52 |  | nn0uz 12921 | . . . 4
⊢
ℕ0 = (ℤ≥‘0) | 
| 53 |  | 0zd 12627 | . . . 4
⊢ (𝜑 → 0 ∈
ℤ) | 
| 54 | 2 | nncnd 12283 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 55 |  | nn0cn 12538 | . . . . 5
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) | 
| 56 |  | nn0ex 12534 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 57 | 56 | mptex 7244 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V | 
| 58 | 9, 57 | eqeltri 2836 | . . . . . 6
⊢ 𝐺 ∈ V | 
| 59 | 58 | shftval4 15117 | . . . . 5
⊢ ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗))) | 
| 60 | 54, 55, 59 | syl2an 596 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗))) | 
| 61 |  | nn0addcl 12563 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (𝑀 + 𝑗) ∈
ℕ0) | 
| 62 | 3, 61 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈
ℕ0) | 
| 63 | 9 | eftval 16113 | . . . . . 6
⊢ ((𝑀 + 𝑗) ∈ ℕ0 → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗)))) | 
| 64 | 62, 63 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗)))) | 
| 65 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) | 
| 66 |  | reeftcl 16111 | . . . . . 6
⊢
(((abs‘𝐴)
∈ ℝ ∧ (𝑀 +
𝑗) ∈
ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ) | 
| 67 | 65, 62, 66 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ) | 
| 68 | 64, 67 | eqeltrd 2840 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ) | 
| 69 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗)) | 
| 70 | 69 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 71 |  | eftl.3 | . . . . . 6
⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛))) | 
| 72 |  | ovex 7465 | . . . . . 6
⊢
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ V | 
| 73 | 70, 71, 72 | fvmpt 7015 | . . . . 5
⊢ (𝑗 ∈ ℕ0
→ (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 74 | 73 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 75 | 12, 16 | nndivred 12321 | . . . . . 6
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ) | 
| 76 | 75 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ) | 
| 77 | 2 | peano2nnd 12284 | . . . . . . 7
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) | 
| 78 | 77 | nnrecred 12318 | . . . . . 6
⊢ (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ) | 
| 79 |  | reexpcl 14120 | . . . . . 6
⊢ (((1 /
(𝑀 + 1)) ∈ ℝ
∧ 𝑗 ∈
ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ) | 
| 80 | 78, 79 | sylan 580 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) ∈
ℝ) | 
| 81 | 76, 80 | remulcld 11292 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ) | 
| 82 | 65, 62 | reexpcld 14204 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ) | 
| 83 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ∈
ℝ) | 
| 84 | 62 | faccld 14324 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℕ) | 
| 85 | 84 | nnred 12282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℝ) | 
| 86 | 85, 81 | remulcld 11292 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ) | 
| 87 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑀 ∈
ℕ0) | 
| 88 |  | uzid 12894 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) | 
| 89 | 21, 88 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) | 
| 90 |  | uzaddcl 12947 | . . . . . . . . 9
⊢ ((𝑀 ∈
(ℤ≥‘𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ≥‘𝑀)) | 
| 91 | 89, 90 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ≥‘𝑀)) | 
| 92 | 1 | absge0d 15484 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) | 
| 93 | 92 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) | 
| 94 |  | eftl.6 | . . . . . . . . 9
⊢ (𝜑 → (abs‘𝐴) ≤ 1) | 
| 95 | 94 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ≤
1) | 
| 96 | 65, 87, 91, 93, 95 | leexp2rd 14295 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀)) | 
| 97 | 16 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ∈
ℕ) | 
| 98 |  | nnexpcl 14116 | . . . . . . . . . . . . 13
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0)
→ ((𝑀 + 1)↑𝑗) ∈
ℕ) | 
| 99 | 77, 98 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ) | 
| 100 | 97, 99 | nnmulcld 12320 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℕ) | 
| 101 | 100 | nnred 12282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℝ) | 
| 102 | 8, 3, 92 | expge0d 14205 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀)) | 
| 103 | 12, 102 | jca 511 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) | 
| 104 | 103 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) | 
| 105 |  | faclbnd6 14339 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) | 
| 106 | 3, 105 | sylan 580 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) | 
| 107 |  | lemul1a 12122 | . . . . . . . . . 10
⊢
(((((!‘𝑀)
· ((𝑀 +
1)↑𝑗)) ∈ ℝ
∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧
(((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤
((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀))) | 
| 108 | 101, 85, 104, 106, 107 | syl31anc 1374 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀))) | 
| 109 | 85, 83 | remulcld 11292 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ) | 
| 110 | 100 | nnrpd 13076 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℝ+) | 
| 111 | 83, 109, 110 | lemuldiv2d 13128 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))) | 
| 112 | 108, 111 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) | 
| 113 | 84 | nncnd 12283 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘(𝑀 + 𝑗)) ∈
ℂ) | 
| 114 | 12 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ) | 
| 115 | 114 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ∈
ℂ) | 
| 116 | 100 | nncnd 12283 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ∈
ℂ) | 
| 117 | 100 | nnne0d 12317 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘𝑀) ·
((𝑀 + 1)↑𝑗)) ≠ 0) | 
| 118 | 113, 115,
116, 117 | divassd 12079 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))) | 
| 119 | 77 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ∈
ℂ) | 
| 121 | 77 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ∈
ℕ) | 
| 122 | 121 | nnne0d 12317 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑀 + 1) ≠ 0) | 
| 123 |  | nn0z 12640 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℤ) | 
| 124 | 123 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℤ) | 
| 125 | 120, 122,
124 | exprecd 14195 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗))) | 
| 126 | 125 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗)))) | 
| 127 | 75 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ) | 
| 128 | 127 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ) | 
| 129 | 99 | nncnd 12283 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ) | 
| 130 | 99 | nnne0d 12317 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ≠ 0) | 
| 131 | 128, 129,
130 | divrecd 12047 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗)))) | 
| 132 | 16 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ (𝜑 → (!‘𝑀) ∈ ℂ) | 
| 133 | 132 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ∈
ℂ) | 
| 134 |  | facne0 14326 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ≠
0) | 
| 135 | 3, 134 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (!‘𝑀) ≠ 0) | 
| 136 | 135 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(!‘𝑀) ≠
0) | 
| 137 | 115, 133,
129, 136, 130 | divdiv1d 12075 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) | 
| 138 | 126, 131,
137 | 3eqtr2rd 2783 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 139 | 138 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) | 
| 140 | 118, 139 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) | 
| 141 | 112, 140 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) | 
| 142 | 82, 83, 86, 96, 141 | letrd 11419 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))) | 
| 143 | 84 | nngt0d 12316 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 <
(!‘(𝑀 + 𝑗))) | 
| 144 |  | ledivmul 12145 | . . . . . . 7
⊢
((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 <
(!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))) | 
| 145 | 82, 81, 85, 143, 144 | syl112anc 1375 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))) | 
| 146 | 142, 145 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 147 | 64, 146 | eqbrtrd 5164 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 148 |  | 0z 12626 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 149 | 21 | znegcld 12726 | . . . . . 6
⊢ (𝜑 → -𝑀 ∈ ℤ) | 
| 150 | 58 | seqshft 15125 | . . . . . 6
⊢ ((0
∈ ℤ ∧ -𝑀
∈ ℤ) → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀)) | 
| 151 | 148, 149,
150 | sylancr 587 | . . . . 5
⊢ (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀)) | 
| 152 |  | 0cn 11254 | . . . . . . . . . . . 12
⊢ 0 ∈
ℂ | 
| 153 |  | subneg 11559 | . . . . . . . . . . . 12
⊢ ((0
∈ ℂ ∧ 𝑀
∈ ℂ) → (0 − -𝑀) = (0 + 𝑀)) | 
| 154 | 152, 153 | mpan 690 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℂ → (0
− -𝑀) = (0 + 𝑀)) | 
| 155 |  | addlid 11445 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℂ → (0 +
𝑀) = 𝑀) | 
| 156 | 154, 155 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℂ → (0
− -𝑀) = 𝑀) | 
| 157 | 54, 156 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (0 − -𝑀) = 𝑀) | 
| 158 | 157 | seqeq1d 14049 | . . . . . . . 8
⊢ (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺)) | 
| 159 | 158, 45 | eqbrtrd 5164 | . . . . . . 7
⊢ (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 160 |  | seqex 14045 | . . . . . . . 8
⊢ seq(0
− -𝑀)( + , 𝐺) ∈ V | 
| 161 |  | climshft 15613 | . . . . . . . 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 257 | . . . . . 6
⊢ (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 164 |  | ovex 7465 | . . . . . . 7
⊢ (seq(0
− -𝑀)( + , 𝐺) shift -𝑀) ∈ V | 
| 165 |  | sumex 15725 | . . . . . . 7
⊢
Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐺‘𝑘) ∈ V | 
| 166 | 164, 165 | breldm 5918 | . . . . . 6
⊢ ((seq(0
− -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ ) | 
| 167 | 163, 166 | syl 17 | . . . . 5
⊢ (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ ) | 
| 168 | 151, 167 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ ) | 
| 169 | 2 | nnge1d 12315 | . . . . . . . . . 10
⊢ (𝜑 → 1 ≤ 𝑀) | 
| 170 |  | 1nn 12278 | . . . . . . . . . . 11
⊢ 1 ∈
ℕ | 
| 171 |  | nnleltp1 12675 | . . . . . . . . . . 11
⊢ ((1
∈ ℕ ∧ 𝑀
∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1))) | 
| 172 | 170, 2, 171 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1))) | 
| 173 | 169, 172 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 1 < (𝑀 + 1)) | 
| 174 | 14 | nn0ge0d 12592 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑀 + 1)) | 
| 175 | 15, 174 | absidd 15462 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1)) | 
| 176 | 173, 175 | breqtrrd 5170 | . . . . . . . 8
⊢ (𝜑 → 1 < (abs‘(𝑀 + 1))) | 
| 177 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛)) = (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛)) | 
| 178 |  | ovex 7465 | . . . . . . . . . 10
⊢ ((1 /
(𝑀 + 1))↑𝑗) ∈ V | 
| 179 | 69, 177, 178 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗)) | 
| 180 | 179 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗)) | 
| 181 | 119, 176,
180 | georeclim 15909 | . . . . . . 7
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))) ⇝
((𝑀 + 1) / ((𝑀 + 1) −
1))) | 
| 182 | 80 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 /
(𝑀 + 1))↑𝑗) ∈
ℂ) | 
| 183 | 180, 182 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((1 / (𝑀 +
1))↑𝑛))‘𝑗) ∈
ℂ) | 
| 184 | 180 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 /
(𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 185 | 74, 184 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐻‘𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 /
(𝑀 + 1))↑𝑛))‘𝑗))) | 
| 186 | 52, 53, 127, 181, 183, 185 | isermulc2 15695 | . . . . . 6
⊢ (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1)))) | 
| 187 |  | ax-1cn 11214 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 188 |  | pncan 11515 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) | 
| 189 | 54, 187, 188 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) | 
| 190 | 189 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀)) | 
| 191 | 190 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀))) | 
| 192 | 15, 2 | nndivred 12321 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ) | 
| 193 | 192 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ) | 
| 194 | 114, 193,
132, 135 | div23d 12081 | . . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀))) | 
| 195 | 191, 194 | eqtr4d 2779 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀))) | 
| 196 | 114, 193,
132, 135 | divassd 12079 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀)))) | 
| 197 | 2 | nnne0d 12317 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 0) | 
| 198 | 119, 54, 132, 197, 135 | divdiv1d 12075 | . . . . . . . . 9
⊢ (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀)))) | 
| 199 | 54, 132 | mulcomd 11283 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀)) | 
| 200 | 199 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) | 
| 201 | 198, 200 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) | 
| 202 | 201 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) | 
| 203 | 195, 196,
202 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) | 
| 204 | 186, 203 | breqtrd 5168 | . . . . 5
⊢ (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) | 
| 205 |  | seqex 14045 | . . . . . 6
⊢ seq0( + ,
𝐻) ∈
V | 
| 206 |  | ovex 7465 | . . . . . 6
⊢
(((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ V | 
| 207 | 205, 206 | breldm 5918 | . . . . 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 15881 | . . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) | 
| 210 |  | eqid 2736 | . . . . 5
⊢
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘(0 +
𝑀)) | 
| 211 |  | fveq2 6905 | . . . . 5
⊢ (𝑘 = (𝑀 + 𝑗) → (𝐺‘𝑘) = (𝐺‘(𝑀 + 𝑗))) | 
| 212 | 54 | addlidd 11463 | . . . . . . . . 9
⊢ (𝜑 → (0 + 𝑀) = 𝑀) | 
| 213 | 212 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀)) | 
| 214 | 213 | eleq2d 2826 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(0 +
𝑀)) ↔ 𝑘 ∈
(ℤ≥‘𝑀))) | 
| 215 | 214 | biimpa 476 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
𝑀))) → 𝑘 ∈
(ℤ≥‘𝑀)) | 
| 216 | 215, 41 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
𝑀))) → (𝐺‘𝑘) ∈ ℂ) | 
| 217 | 52, 210, 211, 21, 53, 216 | isumshft 15876 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(0 +
𝑀))(𝐺‘𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗))) | 
| 218 | 213 | sumeq1d 15737 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(0 +
𝑀))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 219 | 217, 218 | eqtr3d 2778 | . . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘)) | 
| 220 | 81 | recnd 11290 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ) | 
| 221 | 52, 53, 74, 220, 204 | isumclim 15794 | . . 3
⊢ (𝜑 → Σ𝑗 ∈ ℕ0
((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) | 
| 222 | 209, 219,
221 | 3brtr3d 5173 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) | 
| 223 | 7, 11, 19, 51, 222 | letrd 11419 | 1
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) |