ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eftlub GIF version

Theorem eftlub 11693
Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
eftl.1 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
eftl.2 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
eftl.3 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
eftl.4 (𝜑𝑀 ∈ ℕ)
eftl.5 (𝜑𝐴 ∈ ℂ)
eftl.6 (𝜑 → (abs‘𝐴) ≤ 1)
Assertion
Ref Expression
eftlub (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑛)   𝐹(𝑛)   𝐺(𝑛)   𝐻(𝑘,𝑛)

Proof of Theorem eftlub
Dummy variables 𝑗 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eftl.5 . . . 4 (𝜑𝐴 ∈ ℂ)
2 eftl.4 . . . . 5 (𝜑𝑀 ∈ ℕ)
32nnnn0d 9227 . . . 4 (𝜑𝑀 ∈ ℕ0)
4 eftl.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
54eftlcl 11691 . . . 4 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
61, 3, 5syl2anc 411 . . 3 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
76abscld 11185 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ∈ ℝ)
81abscld 11185 . . 3 (𝜑 → (abs‘𝐴) ∈ ℝ)
9 eftl.2 . . . 4 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
109reeftlcl 11692 . . 3 (((abs‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
118, 3, 10syl2anc 411 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
128, 3reexpcld 10667 . . 3 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ)
13 peano2nn0 9214 . . . . . 6 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
143, 13syl 14 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℕ0)
1514nn0red 9228 . . . 4 (𝜑 → (𝑀 + 1) ∈ ℝ)
163faccld 10711 . . . . 5 (𝜑 → (!‘𝑀) ∈ ℕ)
1716, 2nnmulcld 8966 . . . 4 (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ)
1815, 17nndivred 8967 . . 3 (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ)
1912, 18remulcld 7986 . 2 (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ)
20 eqid 2177 . . 3 (ℤ𝑀) = (ℤ𝑀)
212nnzd 9372 . . . 4 (𝜑𝑀 ∈ ℤ)
22 eqidd 2178 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐹𝑘))
23 eluznn0 9597 . . . . . 6 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
243, 23sylan 283 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
254eftvalcn 11660 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
261, 25sylan 283 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
27 eftcl 11657 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
281, 27sylan 283 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
2926, 28eqeltrd 2254 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
3024, 29syldan 282 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
314eftlcvg 11690 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
321, 3, 31syl2anc 411 . . . 4 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
3320, 21, 22, 30, 32isumclim2 11425 . . 3 (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘))
34 eqidd 2178 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (𝐺𝑘))
358recnd 7984 . . . . . . . 8 (𝜑 → (abs‘𝐴) ∈ ℂ)
369eftvalcn 11660 . . . . . . . 8 (((abs‘𝐴) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
3735, 36sylan 283 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
38 reeftcl 11658 . . . . . . . 8 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
398, 38sylan 283 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
4037, 39eqeltrd 2254 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4124, 40syldan 282 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℝ)
4241recnd 7984 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℂ)
439eftlcvg 11690 . . . . 5 (((abs‘𝐴) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4435, 3, 43syl2anc 411 . . . 4 (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4520, 21, 34, 42, 44isumclim2 11425 . . 3 (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
46 eftabs 11659 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
471, 46sylan 283 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
4826fveq2d 5519 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘(𝐹𝑘)) = (abs‘((𝐴𝑘) / (!‘𝑘))))
4947, 48, 373eqtr4rd 2221 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5024, 49syldan 282 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5120, 33, 45, 21, 30, 50iserabs 11478 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
52 nn0uz 9560 . . . 4 0 = (ℤ‘0)
53 0zd 9263 . . . 4 (𝜑 → 0 ∈ ℤ)
542nncnd 8931 . . . . 5 (𝜑𝑀 ∈ ℂ)
55 nn0cn 9184 . . . . 5 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
56 nn0ex 9180 . . . . . . . 8 0 ∈ V
5756mptex 5742 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V
589, 57eqeltri 2250 . . . . . 6 𝐺 ∈ V
5958shftval4 10832 . . . . 5 ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6054, 55, 59syl2an 289 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6135adantr 276 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
62 nn0addcl 9209 . . . . . . 7 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
633, 62sylan 283 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
649eftvalcn 11660 . . . . . 6 (((abs‘𝐴) ∈ ℂ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
6561, 63, 64syl2anc 411 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
668adantr 276 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
67 reeftcl 11658 . . . . . 6 (((abs‘𝐴) ∈ ℝ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6866, 63, 67syl2anc 411 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6965, 68eqeltrd 2254 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ)
70 simpr 110 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
7112, 16nndivred 8967 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
7271adantr 276 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
732peano2nnd 8932 . . . . . . . 8 (𝜑 → (𝑀 + 1) ∈ ℕ)
7473nnrecred 8964 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
75 reexpcl 10534 . . . . . . 7 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7674, 75sylan 283 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7772, 76remulcld 7986 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ)
78 oveq2 5882 . . . . . . 7 (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗))
7978oveq2d 5890 . . . . . 6 (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
80 eftl.3 . . . . . 6 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
8179, 80fvmptg 5592 . . . . 5 ((𝑗 ∈ ℕ0 ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8270, 77, 81syl2anc 411 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8366, 63reexpcld 10667 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ)
8412adantr 276 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℝ)
8563faccld 10711 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℕ)
8685nnred 8930 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℝ)
8786, 77remulcld 7986 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ)
883adantr 276 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑀 ∈ ℕ0)
89 uzid 9540 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
9021, 89syl 14 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ𝑀))
91 uzaddcl 9584 . . . . . . . . 9 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
9290, 91sylan 283 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
931absge0d 11188 . . . . . . . . 9 (𝜑 → 0 ≤ (abs‘𝐴))
9493adantr 276 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
95 eftl.6 . . . . . . . . 9 (𝜑 → (abs‘𝐴) ≤ 1)
9695adantr 276 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ≤ 1)
9766, 88, 92, 94, 96leexp2rd 10680 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀))
9816adantr 276 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℕ)
99 nnexpcl 10530 . . . . . . . . . . . . 13 (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10073, 99sylan 283 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10198, 100nnmulcld 8966 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℕ)
102101nnred 8930 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ)
1038, 3, 93expge0d 10668 . . . . . . . . . . . 12 (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀))
10412, 103jca 306 . . . . . . . . . . 11 (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
105104adantr 276 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
106 faclbnd6 10719 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
1073, 106sylan 283 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
108 lemul1a 8813 . . . . . . . . . 10 (((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ ∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧ (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
109102, 86, 105, 107, 108syl31anc 1241 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
11086, 84remulcld 7986 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ)
111101nnrpd 9692 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ+)
11284, 110, 111lemuldiv2d 9745 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
113109, 112mpbid 147 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
11485nncnd 8931 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℂ)
11512recnd 7984 . . . . . . . . . . 11 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ)
116115adantr 276 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℂ)
117101nncnd 8931 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℂ)
118101nnap0d 8963 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) # 0)
119114, 116, 117, 118divassapd 8781 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
12073nncnd 8931 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 + 1) ∈ ℂ)
121120adantr 276 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
12273adantr 276 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
123122nnap0d 8963 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) # 0)
124 nn0z 9271 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
125124adantl 277 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
126121, 123, 125exprecapd 10658 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗)))
127126oveq2d 5890 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
12871recnd 7984 . . . . . . . . . . . . 13 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
129128adantr 276 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
130100nncnd 8931 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ)
131100nnap0d 8963 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) # 0)
132129, 130, 131divrecapd 8748 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
13316nncnd 8931 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑀) ∈ ℂ)
134133adantr 276 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℂ)
13598nnap0d 8963 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) # 0)
136116, 134, 130, 135, 131divdivap1d 8777 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
137127, 132, 1363eqtr2rd 2217 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
138137oveq2d 5890 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
139119, 138eqtrd 2210 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
140113, 139breqtrd 4029 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14183, 84, 87, 97, 140letrd 8079 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14285nngt0d 8961 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 < (!‘(𝑀 + 𝑗)))
143 ledivmul 8832 . . . . . . 7 ((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 < (!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
14483, 77, 86, 142, 143syl112anc 1242 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
145141, 144mpbird 167 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14665, 145eqbrtrd 4025 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14758a1i 9 . . . . . 6 (𝜑𝐺 ∈ V)
14821znegcld 9375 . . . . . 6 (𝜑 → -𝑀 ∈ ℤ)
149 0cn 7948 . . . . . . . . . . . . 13 0 ∈ ℂ
150 subneg 8204 . . . . . . . . . . . . 13 ((0 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 − -𝑀) = (0 + 𝑀))
151149, 150mpan 424 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 − -𝑀) = (0 + 𝑀))
152 addlid 8094 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
153151, 152eqtrd 2210 . . . . . . . . . . 11 (𝑀 ∈ ℂ → (0 − -𝑀) = 𝑀)
15454, 153syl 14 . . . . . . . . . 10 (𝜑 → (0 − -𝑀) = 𝑀)
155154fveq2d 5519 . . . . . . . . 9 (𝜑 → (ℤ‘(0 − -𝑀)) = (ℤ𝑀))
156155eleq2d 2247 . . . . . . . 8 (𝜑 → (𝑘 ∈ (ℤ‘(0 − -𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
157156pm5.32i 454 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) ↔ (𝜑𝑘 ∈ (ℤ𝑀)))
158157, 41sylbi 121 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) → (𝐺𝑘) ∈ ℝ)
159 readdcl 7936 . . . . . . 7 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
160159adantl 277 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
161147, 53, 148, 158, 160seq3shft 10842 . . . . 5 (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀))
162 seqex 10444 . . . . . . 7 seq(0 − -𝑀)( + , 𝐺) ∈ V
16354negcld 8253 . . . . . . 7 (𝜑 → -𝑀 ∈ ℂ)
164 ovshftex 10823 . . . . . . 7 ((seq(0 − -𝑀)( + , 𝐺) ∈ V ∧ -𝑀 ∈ ℂ) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
165162, 163, 164sylancr 414 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
16620, 21, 34, 41, 44isumrecl 11432 . . . . . 6 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
167154seqeq1d 10448 . . . . . . . 8 (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺))
168167, 45eqbrtrd 4025 . . . . . . 7 (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
169 climshft 11307 . . . . . . . 8 ((-𝑀 ∈ ℤ ∧ seq(0 − -𝑀)( + , 𝐺) ∈ V) → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
170148, 162, 169sylancl 413 . . . . . . 7 (𝜑 → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
171168, 170mpbird 167 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
172 breldmg 4833 . . . . . 6 (((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V ∧ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ ∧ (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
173165, 166, 171, 172syl3anc 1238 . . . . 5 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
174161, 173eqeltrd 2254 . . . 4 (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ )
175 seqex 10444 . . . . . 6 seq0( + , 𝐻) ∈ V
176175a1i 9 . . . . 5 (𝜑 → seq0( + , 𝐻) ∈ V)
1772nnge1d 8960 . . . . . . . . . 10 (𝜑 → 1 ≤ 𝑀)
178 1nn 8928 . . . . . . . . . . 11 1 ∈ ℕ
179 nnleltp1 9310 . . . . . . . . . . 11 ((1 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
180178, 2, 179sylancr 414 . . . . . . . . . 10 (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
181177, 180mpbid 147 . . . . . . . . 9 (𝜑 → 1 < (𝑀 + 1))
18214nn0ge0d 9230 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝑀 + 1))
18315, 182absidd 11171 . . . . . . . . 9 (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1))
184181, 183breqtrrd 4031 . . . . . . . 8 (𝜑 → 1 < (abs‘(𝑀 + 1)))
18574adantr 276 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (1 / (𝑀 + 1)) ∈ ℝ)
186185, 70reexpcld 10667 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
187 eqid 2177 . . . . . . . . . 10 (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))
18878, 187fvmptg 5592 . . . . . . . . 9 ((𝑗 ∈ ℕ0 ∧ ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
18970, 186, 188syl2anc 411 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
190120, 184, 189georeclim 11516 . . . . . . 7 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))) ⇝ ((𝑀 + 1) / ((𝑀 + 1) − 1)))
19176recnd 7984 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℂ)
192189, 191eqeltrd 2254 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) ∈ ℂ)
193189oveq2d 5890 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
19482, 193eqtr4d 2213 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)))
19552, 53, 128, 190, 192, 194isermulc2 11343 . . . . . 6 (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))))
196 ax-1cn 7903 . . . . . . . . . . 11 1 ∈ ℂ
197 pncan 8161 . . . . . . . . . . 11 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
19854, 196, 197sylancl 413 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
199198oveq2d 5890 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀))
200199oveq2d 5890 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
20115, 2nndivred 8967 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ)
202201recnd 7984 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ)
20316nnap0d 8963 . . . . . . . . 9 (𝜑 → (!‘𝑀) # 0)
204115, 202, 133, 203div23apd 8783 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
205200, 204eqtr4d 2213 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)))
206115, 202, 133, 203divassapd 8781 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))))
2072nnap0d 8963 . . . . . . . . . 10 (𝜑𝑀 # 0)
208120, 54, 133, 207, 203divdivap1d 8777 . . . . . . . . 9 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀))))
20954, 133mulcomd 7977 . . . . . . . . . 10 (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀))
210209oveq2d 5890 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
211208, 210eqtrd 2210 . . . . . . . 8 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
212211oveq2d 5890 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
213205, 206, 2123eqtrd 2214 . . . . . 6 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
214195, 213breqtrd 4029 . . . . 5 (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
215 breldmg 4833 . . . . 5 ((seq0( + , 𝐻) ∈ V ∧ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ ∧ seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) → seq0( + , 𝐻) ∈ dom ⇝ )
216176, 19, 214, 215syl3anc 1238 . . . 4 (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
21752, 53, 60, 69, 82, 77, 146, 174, 216isumle 11498 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
218 eqid 2177 . . . . 5 (ℤ‘(0 + 𝑀)) = (ℤ‘(0 + 𝑀))
219 fveq2 5515 . . . . 5 (𝑘 = (𝑀 + 𝑗) → (𝐺𝑘) = (𝐺‘(𝑀 + 𝑗)))
22054addid2d 8105 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
221220fveq2d 5519 . . . . . . . 8 (𝜑 → (ℤ‘(0 + 𝑀)) = (ℤ𝑀))
222221eleq2d 2247 . . . . . . 7 (𝜑 → (𝑘 ∈ (ℤ‘(0 + 𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
223222biimpa 296 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → 𝑘 ∈ (ℤ𝑀))
224223, 42syldan 282 . . . . 5 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → (𝐺𝑘) ∈ ℂ)
22552, 218, 219, 21, 53, 224isumshft 11493 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)))
226221sumeq1d 11369 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
227225, 226eqtr3d 2212 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
22877recnd 7984 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ)
22952, 53, 82, 228, 214isumclim 11424 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
230217, 227, 2293brtr3d 4034 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
2317, 11, 19, 51, 230letrd 8079 1 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  Vcvv 2737   class class class wbr 4003  cmpt 4064  dom cdm 4626  cfv 5216  (class class class)co 5874  cc 7808  cr 7809  0cc0 7810  1c1 7811   + caddc 7813   · cmul 7815   < clt 7990  cle 7991  cmin 8126  -cneg 8127   / cdiv 8627  cn 8917  0cn0 9174  cz 9251  cuz 9526  seqcseq 10442  cexp 10516  !cfa 10700   shift cshi 10818  abscabs 11001  cli 11281  Σcsu 11356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-pnf 7992  df-mnf 7993  df-xr 7994  df-ltxr 7995  df-le 7996  df-sub 8128  df-neg 8129  df-reap 8530  df-ap 8537  df-div 8628  df-inn 8918  df-2 8976  df-3 8977  df-4 8978  df-n0 9175  df-z 9252  df-uz 9527  df-q 9618  df-rp 9652  df-ico 9892  df-fz 10007  df-fzo 10140  df-seqfrec 10443  df-exp 10517  df-fac 10701  df-ihash 10751  df-shft 10819  df-cj 10846  df-re 10847  df-im 10848  df-rsqrt 11002  df-abs 11003  df-clim 11282  df-sumdc 11357
This theorem is referenced by:  ef01bndlem  11759  eirraplem  11779  dveflem  14080
  Copyright terms: Public domain W3C validator