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

Theorem eftlub 11653
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 9188 . . . 4 (𝜑𝑀 ∈ ℕ0)
4 eftl.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
54eftlcl 11651 . . . 4 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
61, 3, 5syl2anc 409 . . 3 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
76abscld 11145 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ∈ ℝ)
81abscld 11145 . . 3 (𝜑 → (abs‘𝐴) ∈ ℝ)
9 eftl.2 . . . 4 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
109reeftlcl 11652 . . 3 (((abs‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
118, 3, 10syl2anc 409 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
128, 3reexpcld 10626 . . 3 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ)
13 peano2nn0 9175 . . . . . 6 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
143, 13syl 14 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℕ0)
1514nn0red 9189 . . . 4 (𝜑 → (𝑀 + 1) ∈ ℝ)
163faccld 10670 . . . . 5 (𝜑 → (!‘𝑀) ∈ ℕ)
1716, 2nnmulcld 8927 . . . 4 (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ)
1815, 17nndivred 8928 . . 3 (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ)
1912, 18remulcld 7950 . 2 (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ)
20 eqid 2170 . . 3 (ℤ𝑀) = (ℤ𝑀)
212nnzd 9333 . . . 4 (𝜑𝑀 ∈ ℤ)
22 eqidd 2171 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐹𝑘))
23 eluznn0 9558 . . . . . 6 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
243, 23sylan 281 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
254eftvalcn 11620 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
261, 25sylan 281 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
27 eftcl 11617 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
281, 27sylan 281 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
2926, 28eqeltrd 2247 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
3024, 29syldan 280 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
314eftlcvg 11650 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
321, 3, 31syl2anc 409 . . . 4 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
3320, 21, 22, 30, 32isumclim2 11385 . . 3 (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘))
34 eqidd 2171 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (𝐺𝑘))
358recnd 7948 . . . . . . . 8 (𝜑 → (abs‘𝐴) ∈ ℂ)
369eftvalcn 11620 . . . . . . . 8 (((abs‘𝐴) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
3735, 36sylan 281 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
38 reeftcl 11618 . . . . . . . 8 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
398, 38sylan 281 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
4037, 39eqeltrd 2247 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4124, 40syldan 280 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℝ)
4241recnd 7948 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℂ)
439eftlcvg 11650 . . . . 5 (((abs‘𝐴) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4435, 3, 43syl2anc 409 . . . 4 (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4520, 21, 34, 42, 44isumclim2 11385 . . 3 (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
46 eftabs 11619 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
471, 46sylan 281 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
4826fveq2d 5500 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘(𝐹𝑘)) = (abs‘((𝐴𝑘) / (!‘𝑘))))
4947, 48, 373eqtr4rd 2214 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5024, 49syldan 280 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5120, 33, 45, 21, 30, 50iserabs 11438 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
52 nn0uz 9521 . . . 4 0 = (ℤ‘0)
53 0zd 9224 . . . 4 (𝜑 → 0 ∈ ℤ)
542nncnd 8892 . . . . 5 (𝜑𝑀 ∈ ℂ)
55 nn0cn 9145 . . . . 5 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
56 nn0ex 9141 . . . . . . . 8 0 ∈ V
5756mptex 5722 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V
589, 57eqeltri 2243 . . . . . 6 𝐺 ∈ V
5958shftval4 10792 . . . . 5 ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6054, 55, 59syl2an 287 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6135adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
62 nn0addcl 9170 . . . . . . 7 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
633, 62sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
649eftvalcn 11620 . . . . . 6 (((abs‘𝐴) ∈ ℂ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
6561, 63, 64syl2anc 409 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
668adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
67 reeftcl 11618 . . . . . 6 (((abs‘𝐴) ∈ ℝ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6866, 63, 67syl2anc 409 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6965, 68eqeltrd 2247 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ)
70 simpr 109 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
7112, 16nndivred 8928 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
7271adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
732peano2nnd 8893 . . . . . . . 8 (𝜑 → (𝑀 + 1) ∈ ℕ)
7473nnrecred 8925 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
75 reexpcl 10493 . . . . . . 7 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7674, 75sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7772, 76remulcld 7950 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ)
78 oveq2 5861 . . . . . . 7 (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗))
7978oveq2d 5869 . . . . . 6 (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
80 eftl.3 . . . . . 6 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
8179, 80fvmptg 5572 . . . . 5 ((𝑗 ∈ ℕ0 ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8270, 77, 81syl2anc 409 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8366, 63reexpcld 10626 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ)
8412adantr 274 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℝ)
8563faccld 10670 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℕ)
8685nnred 8891 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℝ)
8786, 77remulcld 7950 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ)
883adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑀 ∈ ℕ0)
89 uzid 9501 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
9021, 89syl 14 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ𝑀))
91 uzaddcl 9545 . . . . . . . . 9 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
9290, 91sylan 281 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
931absge0d 11148 . . . . . . . . 9 (𝜑 → 0 ≤ (abs‘𝐴))
9493adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 0 ≤ (abs‘𝐴))
95 eftl.6 . . . . . . . . 9 (𝜑 → (abs‘𝐴) ≤ 1)
9695adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ≤ 1)
9766, 88, 92, 94, 96leexp2rd 10639 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀))
9816adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℕ)
99 nnexpcl 10489 . . . . . . . . . . . . 13 (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10073, 99sylan 281 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10198, 100nnmulcld 8927 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℕ)
102101nnred 8891 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ)
1038, 3, 93expge0d 10627 . . . . . . . . . . . 12 (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀))
10412, 103jca 304 . . . . . . . . . . 11 (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
105104adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
106 faclbnd6 10678 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
1073, 106sylan 281 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
108 lemul1a 8774 . . . . . . . . . 10 (((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ ∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧ (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
109102, 86, 105, 107, 108syl31anc 1236 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
11086, 84remulcld 7950 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ)
111101nnrpd 9651 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ+)
11284, 110, 111lemuldiv2d 9704 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
113109, 112mpbid 146 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
11485nncnd 8892 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℂ)
11512recnd 7948 . . . . . . . . . . 11 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ)
116115adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℂ)
117101nncnd 8892 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℂ)
118101nnap0d 8924 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) # 0)
119114, 116, 117, 118divassapd 8743 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
12073nncnd 8892 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 + 1) ∈ ℂ)
121120adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
12273adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
123122nnap0d 8924 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) # 0)
124 nn0z 9232 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
125124adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
126121, 123, 125exprecapd 10617 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗)))
127126oveq2d 5869 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
12871recnd 7948 . . . . . . . . . . . . 13 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
129128adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
130100nncnd 8892 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ)
131100nnap0d 8924 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) # 0)
132129, 130, 131divrecapd 8710 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
13316nncnd 8892 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑀) ∈ ℂ)
134133adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℂ)
13598nnap0d 8924 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) # 0)
136116, 134, 130, 135, 131divdivap1d 8739 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
137127, 132, 1363eqtr2rd 2210 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
138137oveq2d 5869 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
139119, 138eqtrd 2203 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
140113, 139breqtrd 4015 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14183, 84, 87, 97, 140letrd 8043 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14285nngt0d 8922 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 < (!‘(𝑀 + 𝑗)))
143 ledivmul 8793 . . . . . . 7 ((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 < (!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
14483, 77, 86, 142, 143syl112anc 1237 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
145141, 144mpbird 166 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14665, 145eqbrtrd 4011 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14758a1i 9 . . . . . 6 (𝜑𝐺 ∈ V)
14821znegcld 9336 . . . . . 6 (𝜑 → -𝑀 ∈ ℤ)
149 0cn 7912 . . . . . . . . . . . . 13 0 ∈ ℂ
150 subneg 8168 . . . . . . . . . . . . 13 ((0 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 − -𝑀) = (0 + 𝑀))
151149, 150mpan 422 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 − -𝑀) = (0 + 𝑀))
152 addid2 8058 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
153151, 152eqtrd 2203 . . . . . . . . . . 11 (𝑀 ∈ ℂ → (0 − -𝑀) = 𝑀)
15454, 153syl 14 . . . . . . . . . 10 (𝜑 → (0 − -𝑀) = 𝑀)
155154fveq2d 5500 . . . . . . . . 9 (𝜑 → (ℤ‘(0 − -𝑀)) = (ℤ𝑀))
156155eleq2d 2240 . . . . . . . 8 (𝜑 → (𝑘 ∈ (ℤ‘(0 − -𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
157156pm5.32i 451 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) ↔ (𝜑𝑘 ∈ (ℤ𝑀)))
158157, 41sylbi 120 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) → (𝐺𝑘) ∈ ℝ)
159 readdcl 7900 . . . . . . 7 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
160159adantl 275 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
161147, 53, 148, 158, 160seq3shft 10802 . . . . 5 (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀))
162 seqex 10403 . . . . . . 7 seq(0 − -𝑀)( + , 𝐺) ∈ V
16354negcld 8217 . . . . . . 7 (𝜑 → -𝑀 ∈ ℂ)
164 ovshftex 10783 . . . . . . 7 ((seq(0 − -𝑀)( + , 𝐺) ∈ V ∧ -𝑀 ∈ ℂ) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
165162, 163, 164sylancr 412 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
16620, 21, 34, 41, 44isumrecl 11392 . . . . . 6 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
167154seqeq1d 10407 . . . . . . . 8 (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺))
168167, 45eqbrtrd 4011 . . . . . . 7 (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
169 climshft 11267 . . . . . . . 8 ((-𝑀 ∈ ℤ ∧ seq(0 − -𝑀)( + , 𝐺) ∈ V) → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
170148, 162, 169sylancl 411 . . . . . . 7 (𝜑 → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
171168, 170mpbird 166 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
172 breldmg 4817 . . . . . 6 (((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V ∧ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ ∧ (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
173165, 166, 171, 172syl3anc 1233 . . . . 5 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
174161, 173eqeltrd 2247 . . . 4 (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ )
175 seqex 10403 . . . . . 6 seq0( + , 𝐻) ∈ V
176175a1i 9 . . . . 5 (𝜑 → seq0( + , 𝐻) ∈ V)
1772nnge1d 8921 . . . . . . . . . 10 (𝜑 → 1 ≤ 𝑀)
178 1nn 8889 . . . . . . . . . . 11 1 ∈ ℕ
179 nnleltp1 9271 . . . . . . . . . . 11 ((1 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
180178, 2, 179sylancr 412 . . . . . . . . . 10 (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
181177, 180mpbid 146 . . . . . . . . 9 (𝜑 → 1 < (𝑀 + 1))
18214nn0ge0d 9191 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝑀 + 1))
18315, 182absidd 11131 . . . . . . . . 9 (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1))
184181, 183breqtrrd 4017 . . . . . . . 8 (𝜑 → 1 < (abs‘(𝑀 + 1)))
18574adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (1 / (𝑀 + 1)) ∈ ℝ)
186185, 70reexpcld 10626 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
187 eqid 2170 . . . . . . . . . 10 (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))
18878, 187fvmptg 5572 . . . . . . . . 9 ((𝑗 ∈ ℕ0 ∧ ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
18970, 186, 188syl2anc 409 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
190120, 184, 189georeclim 11476 . . . . . . 7 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))) ⇝ ((𝑀 + 1) / ((𝑀 + 1) − 1)))
19176recnd 7948 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℂ)
192189, 191eqeltrd 2247 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) ∈ ℂ)
193189oveq2d 5869 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
19482, 193eqtr4d 2206 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)))
19552, 53, 128, 190, 192, 194isermulc2 11303 . . . . . 6 (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))))
196 ax-1cn 7867 . . . . . . . . . . 11 1 ∈ ℂ
197 pncan 8125 . . . . . . . . . . 11 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
19854, 196, 197sylancl 411 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
199198oveq2d 5869 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀))
200199oveq2d 5869 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
20115, 2nndivred 8928 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ)
202201recnd 7948 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ)
20316nnap0d 8924 . . . . . . . . 9 (𝜑 → (!‘𝑀) # 0)
204115, 202, 133, 203div23apd 8745 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
205200, 204eqtr4d 2206 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)))
206115, 202, 133, 203divassapd 8743 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))))
2072nnap0d 8924 . . . . . . . . . 10 (𝜑𝑀 # 0)
208120, 54, 133, 207, 203divdivap1d 8739 . . . . . . . . 9 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀))))
20954, 133mulcomd 7941 . . . . . . . . . 10 (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀))
210209oveq2d 5869 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
211208, 210eqtrd 2203 . . . . . . . 8 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
212211oveq2d 5869 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
213205, 206, 2123eqtrd 2207 . . . . . 6 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
214195, 213breqtrd 4015 . . . . 5 (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
215 breldmg 4817 . . . . 5 ((seq0( + , 𝐻) ∈ V ∧ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ ∧ seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) → seq0( + , 𝐻) ∈ dom ⇝ )
216176, 19, 214, 215syl3anc 1233 . . . 4 (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
21752, 53, 60, 69, 82, 77, 146, 174, 216isumle 11458 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
218 eqid 2170 . . . . 5 (ℤ‘(0 + 𝑀)) = (ℤ‘(0 + 𝑀))
219 fveq2 5496 . . . . 5 (𝑘 = (𝑀 + 𝑗) → (𝐺𝑘) = (𝐺‘(𝑀 + 𝑗)))
22054addid2d 8069 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
221220fveq2d 5500 . . . . . . . 8 (𝜑 → (ℤ‘(0 + 𝑀)) = (ℤ𝑀))
222221eleq2d 2240 . . . . . . 7 (𝜑 → (𝑘 ∈ (ℤ‘(0 + 𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
223222biimpa 294 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → 𝑘 ∈ (ℤ𝑀))
224223, 42syldan 280 . . . . 5 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → (𝐺𝑘) ∈ ℂ)
22552, 218, 219, 21, 53, 224isumshft 11453 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)))
226221sumeq1d 11329 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
227225, 226eqtr3d 2205 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
22877recnd 7948 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ)
22952, 53, 82, 228, 214isumclim 11384 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
230217, 227, 2293brtr3d 4020 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
2317, 11, 19, 51, 230letrd 8043 1 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wcel 2141  Vcvv 2730   class class class wbr 3989  cmpt 4050  dom cdm 4611  cfv 5198  (class class class)co 5853  cc 7772  cr 7773  0cc0 7774  1c1 7775   + caddc 7777   · cmul 7779   < clt 7954  cle 7955  cmin 8090  -cneg 8091   / cdiv 8589  cn 8878  0cn0 9135  cz 9212  cuz 9487  seqcseq 10401  cexp 10475  !cfa 10659   shift cshi 10778  abscabs 10961  cli 11241  Σcsu 11316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-frec 6370  df-1o 6395  df-oadd 6399  df-er 6513  df-en 6719  df-dom 6720  df-fin 6721  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-q 9579  df-rp 9611  df-ico 9851  df-fz 9966  df-fzo 10099  df-seqfrec 10402  df-exp 10476  df-fac 10660  df-ihash 10710  df-shft 10779  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963  df-clim 11242  df-sumdc 11317
This theorem is referenced by:  ef01bndlem  11719  eirraplem  11739  dveflem  13481
  Copyright terms: Public domain W3C validator