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

Theorem eftlub 11385
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 9023 . . . 4 (𝜑𝑀 ∈ ℕ0)
4 eftl.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) / (!‘𝑛)))
54eftlcl 11383 . . . 4 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
61, 3, 5syl2anc 408 . . 3 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘) ∈ ℂ)
76abscld 10946 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ∈ ℝ)
81abscld 10946 . . 3 (𝜑 → (abs‘𝐴) ∈ ℝ)
9 eftl.2 . . . 4 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))
109reeftlcl 11384 . . 3 (((abs‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
118, 3, 10syl2anc 408 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
128, 3reexpcld 10434 . . 3 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℝ)
13 peano2nn0 9010 . . . . . 6 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
143, 13syl 14 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℕ0)
1514nn0red 9024 . . . 4 (𝜑 → (𝑀 + 1) ∈ ℝ)
163faccld 10475 . . . . 5 (𝜑 → (!‘𝑀) ∈ ℕ)
1716, 2nnmulcld 8762 . . . 4 (𝜑 → ((!‘𝑀) · 𝑀) ∈ ℕ)
1815, 17nndivred 8763 . . 3 (𝜑 → ((𝑀 + 1) / ((!‘𝑀) · 𝑀)) ∈ ℝ)
1912, 18remulcld 7789 . 2 (𝜑 → (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ)
20 eqid 2137 . . 3 (ℤ𝑀) = (ℤ𝑀)
212nnzd 9165 . . . 4 (𝜑𝑀 ∈ ℤ)
22 eqidd 2138 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = (𝐹𝑘))
23 eluznn0 9386 . . . . . 6 ((𝑀 ∈ ℕ0𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
243, 23sylan 281 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ0)
254eftvalcn 11352 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
261, 25sylan 281 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = ((𝐴𝑘) / (!‘𝑘)))
27 eftcl 11349 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
281, 27sylan 281 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → ((𝐴𝑘) / (!‘𝑘)) ∈ ℂ)
2926, 28eqeltrd 2214 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
3024, 29syldan 280 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
314eftlcvg 11382 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
321, 3, 31syl2anc 408 . . . 4 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
3320, 21, 22, 30, 32isumclim2 11184 . . 3 (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘))
34 eqidd 2138 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (𝐺𝑘))
358recnd 7787 . . . . . . . 8 (𝜑 → (abs‘𝐴) ∈ ℂ)
369eftvalcn 11352 . . . . . . . 8 (((abs‘𝐴) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
3735, 36sylan 281 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
38 reeftcl 11350 . . . . . . . 8 (((abs‘𝐴) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
398, 38sylan 281 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (((abs‘𝐴)↑𝑘) / (!‘𝑘)) ∈ ℝ)
4037, 39eqeltrd 2214 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4124, 40syldan 280 . . . . 5 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℝ)
4241recnd 7787 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) ∈ ℂ)
439eftlcvg 11382 . . . . 5 (((abs‘𝐴) ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4435, 3, 43syl2anc 408 . . . 4 (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
4520, 21, 34, 42, 44isumclim2 11184 . . 3 (𝜑 → seq𝑀( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
46 eftabs 11351 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
471, 46sylan 281 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘((𝐴𝑘) / (!‘𝑘))) = (((abs‘𝐴)↑𝑘) / (!‘𝑘)))
4826fveq2d 5418 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (abs‘(𝐹𝑘)) = (abs‘((𝐴𝑘) / (!‘𝑘))))
4947, 48, 373eqtr4rd 2181 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5024, 49syldan 280 . . 3 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐺𝑘) = (abs‘(𝐹𝑘)))
5120, 33, 45, 21, 30, 50iserabs 11237 . 2 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
52 nn0uz 9353 . . . 4 0 = (ℤ‘0)
53 0zd 9059 . . . 4 (𝜑 → 0 ∈ ℤ)
542nncnd 8727 . . . . 5 (𝜑𝑀 ∈ ℂ)
55 nn0cn 8980 . . . . 5 (𝑗 ∈ ℕ0𝑗 ∈ ℂ)
56 nn0ex 8976 . . . . . . . 8 0 ∈ V
5756mptex 5639 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛))) ∈ V
589, 57eqeltri 2210 . . . . . 6 𝐺 ∈ V
5958shftval4 10593 . . . . 5 ((𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6054, 55, 59syl2an 287 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((𝐺 shift -𝑀)‘𝑗) = (𝐺‘(𝑀 + 𝑗)))
6135adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℂ)
62 nn0addcl 9005 . . . . . . 7 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
633, 62sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ ℕ0)
649eftvalcn 11352 . . . . . 6 (((abs‘𝐴) ∈ ℂ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
6561, 63, 64syl2anc 408 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) = (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))))
668adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (abs‘𝐴) ∈ ℝ)
67 reeftcl 11350 . . . . . 6 (((abs‘𝐴) ∈ ℝ ∧ (𝑀 + 𝑗) ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6866, 63, 67syl2anc 408 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ∈ ℝ)
6965, 68eqeltrd 2214 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ∈ ℝ)
70 simpr 109 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℕ0)
7112, 16nndivred 8763 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
7271adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℝ)
732peano2nnd 8728 . . . . . . . 8 (𝜑 → (𝑀 + 1) ∈ ℕ)
7473nnrecred 8760 . . . . . . 7 (𝜑 → (1 / (𝑀 + 1)) ∈ ℝ)
75 reexpcl 10303 . . . . . . 7 (((1 / (𝑀 + 1)) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7674, 75sylan 281 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
7772, 76remulcld 7789 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ)
78 oveq2 5775 . . . . . . 7 (𝑛 = 𝑗 → ((1 / (𝑀 + 1))↑𝑛) = ((1 / (𝑀 + 1))↑𝑗))
7978oveq2d 5783 . . . . . 6 (𝑛 = 𝑗 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
80 eftl.3 . . . . . 6 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))
8179, 80fvmptg 5490 . . . . 5 ((𝑗 ∈ ℕ0 ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8270, 77, 81syl2anc 408 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
8366, 63reexpcld 10434 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ)
8412adantr 274 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℝ)
8563faccld 10475 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℕ)
8685nnred 8726 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℝ)
8786, 77remulcld 7789 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))) ∈ ℝ)
883adantr 274 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝑀 ∈ ℕ0)
89 uzid 9333 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
9021, 89syl 14 . . . . . . . . 9 (𝜑𝑀 ∈ (ℤ𝑀))
91 uzaddcl 9374 . . . . . . . . 9 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
9290, 91sylan 281 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 𝑗) ∈ (ℤ𝑀))
931absge0d 10949 . . . . . . . . 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 10447 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((abs‘𝐴)↑𝑀))
9816adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℕ)
99 nnexpcl 10299 . . . . . . . . . . . . 13 (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10073, 99sylan 281 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℕ)
10198, 100nnmulcld 8762 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℕ)
102101nnred 8726 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ)
1038, 3, 93expge0d 10435 . . . . . . . . . . . 12 (𝜑 → 0 ≤ ((abs‘𝐴)↑𝑀))
10412, 103jca 304 . . . . . . . . . . 11 (𝜑 → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
105104adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀)))
106 faclbnd6 10483 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
1073, 106sylan 281 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗)))
108 lemul1a 8609 . . . . . . . . . 10 (((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ ∧ (!‘(𝑀 + 𝑗)) ∈ ℝ ∧ (((abs‘𝐴)↑𝑀) ∈ ℝ ∧ 0 ≤ ((abs‘𝐴)↑𝑀))) ∧ ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ≤ (!‘(𝑀 + 𝑗))) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
109102, 86, 105, 107, 108syl31anc 1219 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)))
11086, 84remulcld 7789 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ∈ ℝ)
111101nnrpd 9475 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℝ+)
11284, 110, 111lemuldiv2d 9527 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((((!‘𝑀) · ((𝑀 + 1)↑𝑗)) · ((abs‘𝐴)↑𝑀)) ≤ ((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) ↔ ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
113109, 112mpbid 146 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
11485nncnd 8727 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (!‘(𝑀 + 𝑗)) ∈ ℂ)
11512recnd 7787 . . . . . . . . . . 11 (𝜑 → ((abs‘𝐴)↑𝑀) ∈ ℂ)
116115adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ∈ ℂ)
117101nncnd 8727 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) ∈ ℂ)
118101nnap0d 8759 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → ((!‘𝑀) · ((𝑀 + 1)↑𝑗)) # 0)
119114, 116, 117, 118divassapd 8579 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))))
12073nncnd 8727 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 + 1) ∈ ℂ)
121120adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
12273adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
123122nnap0d 8759 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → (𝑀 + 1) # 0)
124 nn0z 9067 . . . . . . . . . . . . . 14 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
125124adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ0) → 𝑗 ∈ ℤ)
126121, 123, 125exprecapd 10425 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) = (1 / ((𝑀 + 1)↑𝑗)))
127126oveq2d 5783 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
12871recnd 7787 . . . . . . . . . . . . 13 (𝜑 → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
129128adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / (!‘𝑀)) ∈ ℂ)
130100nncnd 8727 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) ∈ ℂ)
131100nnap0d 8759 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → ((𝑀 + 1)↑𝑗) # 0)
132129, 130, 131divrecapd 8546 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · (1 / ((𝑀 + 1)↑𝑗))))
13316nncnd 8727 . . . . . . . . . . . . 13 (𝜑 → (!‘𝑀) ∈ ℂ)
134133adantr 274 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) ∈ ℂ)
13598nnap0d 8759 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ0) → (!‘𝑀) # 0)
136116, 134, 130, 135, 131divdivap1d 8575 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) / ((𝑀 + 1)↑𝑗)) = (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))))
137127, 132, 1363eqtr2rd 2177 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
138137oveq2d 5783 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((!‘(𝑀 + 𝑗)) · (((abs‘𝐴)↑𝑀) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗)))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
139119, 138eqtrd 2170 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → (((!‘(𝑀 + 𝑗)) · ((abs‘𝐴)↑𝑀)) / ((!‘𝑀) · ((𝑀 + 1)↑𝑗))) = ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
140113, 139breqtrd 3949 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑𝑀) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14183, 84, 87, 97, 140letrd 7879 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗))))
14285nngt0d 8757 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → 0 < (!‘(𝑀 + 𝑗)))
143 ledivmul 8628 . . . . . . 7 ((((abs‘𝐴)↑(𝑀 + 𝑗)) ∈ ℝ ∧ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℝ ∧ ((!‘(𝑀 + 𝑗)) ∈ ℝ ∧ 0 < (!‘(𝑀 + 𝑗)))) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
14483, 77, 86, 142, 143syl112anc 1220 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ↔ ((abs‘𝐴)↑(𝑀 + 𝑗)) ≤ ((!‘(𝑀 + 𝑗)) · ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))))
145141, 144mpbird 166 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (((abs‘𝐴)↑(𝑀 + 𝑗)) / (!‘(𝑀 + 𝑗))) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14665, 145eqbrtrd 3945 . . . 4 ((𝜑𝑗 ∈ ℕ0) → (𝐺‘(𝑀 + 𝑗)) ≤ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
14758a1i 9 . . . . . 6 (𝜑𝐺 ∈ V)
14821znegcld 9168 . . . . . 6 (𝜑 → -𝑀 ∈ ℤ)
149 0cn 7751 . . . . . . . . . . . . 13 0 ∈ ℂ
150 subneg 8004 . . . . . . . . . . . . 13 ((0 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 − -𝑀) = (0 + 𝑀))
151149, 150mpan 420 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 − -𝑀) = (0 + 𝑀))
152 addid2 7894 . . . . . . . . . . . 12 (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
153151, 152eqtrd 2170 . . . . . . . . . . 11 (𝑀 ∈ ℂ → (0 − -𝑀) = 𝑀)
15454, 153syl 14 . . . . . . . . . 10 (𝜑 → (0 − -𝑀) = 𝑀)
155154fveq2d 5418 . . . . . . . . 9 (𝜑 → (ℤ‘(0 − -𝑀)) = (ℤ𝑀))
156155eleq2d 2207 . . . . . . . 8 (𝜑 → (𝑘 ∈ (ℤ‘(0 − -𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
157156pm5.32i 449 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) ↔ (𝜑𝑘 ∈ (ℤ𝑀)))
158157, 41sylbi 120 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 − -𝑀))) → (𝐺𝑘) ∈ ℝ)
159 readdcl 7739 . . . . . . 7 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
160159adantl 275 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
161147, 53, 148, 158, 160seq3shft 10603 . . . . 5 (𝜑 → seq0( + , (𝐺 shift -𝑀)) = (seq(0 − -𝑀)( + , 𝐺) shift -𝑀))
162 seqex 10213 . . . . . . 7 seq(0 − -𝑀)( + , 𝐺) ∈ V
16354negcld 8053 . . . . . . 7 (𝜑 → -𝑀 ∈ ℂ)
164 ovshftex 10584 . . . . . . 7 ((seq(0 − -𝑀)( + , 𝐺) ∈ V ∧ -𝑀 ∈ ℂ) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
165162, 163, 164sylancr 410 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V)
16620, 21, 34, 41, 44isumrecl 11191 . . . . . 6 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ)
167154seqeq1d 10217 . . . . . . . 8 (𝜑 → seq(0 − -𝑀)( + , 𝐺) = seq𝑀( + , 𝐺))
168167, 45eqbrtrd 3945 . . . . . . 7 (𝜑 → seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
169 climshft 11066 . . . . . . . 8 ((-𝑀 ∈ ℤ ∧ seq(0 − -𝑀)( + , 𝐺) ∈ V) → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
170148, 162, 169sylancl 409 . . . . . . 7 (𝜑 → ((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ↔ seq(0 − -𝑀)( + , 𝐺) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)))
171168, 170mpbird 166 . . . . . 6 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
172 breldmg 4740 . . . . . 6 (((seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ V ∧ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ∈ ℝ ∧ (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ⇝ Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘)) → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
173165, 166, 171, 172syl3anc 1216 . . . . 5 (𝜑 → (seq(0 − -𝑀)( + , 𝐺) shift -𝑀) ∈ dom ⇝ )
174161, 173eqeltrd 2214 . . . 4 (𝜑 → seq0( + , (𝐺 shift -𝑀)) ∈ dom ⇝ )
175 seqex 10213 . . . . . 6 seq0( + , 𝐻) ∈ V
176175a1i 9 . . . . 5 (𝜑 → seq0( + , 𝐻) ∈ V)
1772nnge1d 8756 . . . . . . . . . 10 (𝜑 → 1 ≤ 𝑀)
178 1nn 8724 . . . . . . . . . . 11 1 ∈ ℕ
179 nnleltp1 9106 . . . . . . . . . . 11 ((1 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
180178, 2, 179sylancr 410 . . . . . . . . . 10 (𝜑 → (1 ≤ 𝑀 ↔ 1 < (𝑀 + 1)))
181177, 180mpbid 146 . . . . . . . . 9 (𝜑 → 1 < (𝑀 + 1))
18214nn0ge0d 9026 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝑀 + 1))
18315, 182absidd 10932 . . . . . . . . 9 (𝜑 → (abs‘(𝑀 + 1)) = (𝑀 + 1))
184181, 183breqtrrd 3951 . . . . . . . 8 (𝜑 → 1 < (abs‘(𝑀 + 1)))
18574adantr 274 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ0) → (1 / (𝑀 + 1)) ∈ ℝ)
186185, 70reexpcld 10434 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ)
187 eqid 2137 . . . . . . . . . 10 (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))
18878, 187fvmptg 5490 . . . . . . . . 9 ((𝑗 ∈ ℕ0 ∧ ((1 / (𝑀 + 1))↑𝑗) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
18970, 186, 188syl2anc 408 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) = ((1 / (𝑀 + 1))↑𝑗))
190120, 184, 189georeclim 11275 . . . . . . 7 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))) ⇝ ((𝑀 + 1) / ((𝑀 + 1) − 1)))
19176recnd 7787 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((1 / (𝑀 + 1))↑𝑗) ∈ ℂ)
192189, 191eqeltrd 2214 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗) ∈ ℂ)
193189oveq2d 5783 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
19482, 193eqtr4d 2173 . . . . . . 7 ((𝜑𝑗 ∈ ℕ0) → (𝐻𝑗) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑛 ∈ ℕ0 ↦ ((1 / (𝑀 + 1))↑𝑛))‘𝑗)))
19552, 53, 128, 190, 192, 194isermulc2 11102 . . . . . 6 (𝜑 → seq0( + , 𝐻) ⇝ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))))
196 ax-1cn 7706 . . . . . . . . . . 11 1 ∈ ℂ
197 pncan 7961 . . . . . . . . . . 11 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
19854, 196, 197sylancl 409 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
199198oveq2d 5783 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / ((𝑀 + 1) − 1)) = ((𝑀 + 1) / 𝑀))
200199oveq2d 5783 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
20115, 2nndivred 8763 . . . . . . . . . 10 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℝ)
202201recnd 7787 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / 𝑀) ∈ ℂ)
20316nnap0d 8759 . . . . . . . . 9 (𝜑 → (!‘𝑀) # 0)
204115, 202, 133, 203div23apd 8581 . . . . . . . 8 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / 𝑀)))
205200, 204eqtr4d 2173 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)))
206115, 202, 133, 203divassapd 8579 . . . . . . 7 (𝜑 → ((((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / 𝑀)) / (!‘𝑀)) = (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))))
2072nnap0d 8759 . . . . . . . . . 10 (𝜑𝑀 # 0)
208120, 54, 133, 207, 203divdivap1d 8575 . . . . . . . . 9 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / (𝑀 · (!‘𝑀))))
20954, 133mulcomd 7780 . . . . . . . . . 10 (𝜑 → (𝑀 · (!‘𝑀)) = ((!‘𝑀) · 𝑀))
210209oveq2d 5783 . . . . . . . . 9 (𝜑 → ((𝑀 + 1) / (𝑀 · (!‘𝑀))) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
211208, 210eqtrd 2170 . . . . . . . 8 (𝜑 → (((𝑀 + 1) / 𝑀) / (!‘𝑀)) = ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))
212211oveq2d 5783 . . . . . . 7 (𝜑 → (((abs‘𝐴)↑𝑀) · (((𝑀 + 1) / 𝑀) / (!‘𝑀))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
213205, 206, 2123eqtrd 2174 . . . . . 6 (𝜑 → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((𝑀 + 1) / ((𝑀 + 1) − 1))) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
214195, 213breqtrd 3949 . . . . 5 (𝜑 → seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
215 breldmg 4740 . . . . 5 ((seq0( + , 𝐻) ∈ V ∧ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))) ∈ ℝ ∧ seq0( + , 𝐻) ⇝ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀)))) → seq0( + , 𝐻) ∈ dom ⇝ )
216176, 19, 214, 215syl3anc 1216 . . . 4 (𝜑 → seq0( + , 𝐻) ∈ dom ⇝ )
21752, 53, 60, 69, 82, 77, 146, 174, 216isumle 11257 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) ≤ Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)))
218 eqid 2137 . . . . 5 (ℤ‘(0 + 𝑀)) = (ℤ‘(0 + 𝑀))
219 fveq2 5414 . . . . 5 (𝑘 = (𝑀 + 𝑗) → (𝐺𝑘) = (𝐺‘(𝑀 + 𝑗)))
22054addid2d 7905 . . . . . . . . 9 (𝜑 → (0 + 𝑀) = 𝑀)
221220fveq2d 5418 . . . . . . . 8 (𝜑 → (ℤ‘(0 + 𝑀)) = (ℤ𝑀))
222221eleq2d 2207 . . . . . . 7 (𝜑 → (𝑘 ∈ (ℤ‘(0 + 𝑀)) ↔ 𝑘 ∈ (ℤ𝑀)))
223222biimpa 294 . . . . . 6 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → 𝑘 ∈ (ℤ𝑀))
224223, 42syldan 280 . . . . 5 ((𝜑𝑘 ∈ (ℤ‘(0 + 𝑀))) → (𝐺𝑘) ∈ ℂ)
22552, 218, 219, 21, 53, 224isumshft 11252 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)))
226221sumeq1d 11128 . . . 4 (𝜑 → Σ𝑘 ∈ (ℤ‘(0 + 𝑀))(𝐺𝑘) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
227225, 226eqtr3d 2172 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 (𝐺‘(𝑀 + 𝑗)) = Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘))
22877recnd 7787 . . . 4 ((𝜑𝑗 ∈ ℕ0) → ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) ∈ ℂ)
22952, 53, 82, 228, 214isumclim 11183 . . 3 (𝜑 → Σ𝑗 ∈ ℕ0 ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑗)) = (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
230217, 227, 2293brtr3d 3954 . 2 (𝜑 → Σ𝑘 ∈ (ℤ𝑀)(𝐺𝑘) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
2317, 11, 19, 51, 230letrd 7879 1 (𝜑 → (abs‘Σ𝑘 ∈ (ℤ𝑀)(𝐹𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1331  wcel 1480  Vcvv 2681   class class class wbr 3924  cmpt 3984  dom cdm 4534  cfv 5118  (class class class)co 5767  cc 7611  cr 7612  0cc0 7613  1c1 7614   + caddc 7616   · cmul 7618   < clt 7793  cle 7794  cmin 7926  -cneg 7927   / cdiv 8425  cn 8713  0cn0 8970  cz 9047  cuz 9319  seqcseq 10211  cexp 10285  !cfa 10464   shift cshi 10579  abscabs 10762  cli 11040  Σcsu 11115
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-iinf 4497  ax-cnex 7704  ax-resscn 7705  ax-1cn 7706  ax-1re 7707  ax-icn 7708  ax-addcl 7709  ax-addrcl 7710  ax-mulcl 7711  ax-mulrcl 7712  ax-addcom 7713  ax-mulcom 7714  ax-addass 7715  ax-mulass 7716  ax-distr 7717  ax-i2m1 7718  ax-0lt1 7719  ax-1rid 7720  ax-0id 7721  ax-rnegex 7722  ax-precex 7723  ax-cnre 7724  ax-pre-ltirr 7725  ax-pre-ltwlin 7726  ax-pre-lttrn 7727  ax-pre-apti 7728  ax-pre-ltadd 7729  ax-pre-mulgt0 7730  ax-pre-mulext 7731  ax-arch 7732  ax-caucvg 7733
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-nel 2402  df-ral 2419  df-rex 2420  df-reu 2421  df-rmo 2422  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-po 4213  df-iso 4214  df-iord 4283  df-on 4285  df-ilim 4286  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-isom 5127  df-riota 5723  df-ov 5770  df-oprab 5771  df-mpo 5772  df-1st 6031  df-2nd 6032  df-recs 6195  df-irdg 6260  df-frec 6281  df-1o 6306  df-oadd 6310  df-er 6422  df-en 6628  df-dom 6629  df-fin 6630  df-pnf 7795  df-mnf 7796  df-xr 7797  df-ltxr 7798  df-le 7799  df-sub 7928  df-neg 7929  df-reap 8330  df-ap 8337  df-div 8426  df-inn 8714  df-2 8772  df-3 8773  df-4 8774  df-n0 8971  df-z 9048  df-uz 9320  df-q 9405  df-rp 9435  df-ico 9670  df-fz 9784  df-fzo 9913  df-seqfrec 10212  df-exp 10286  df-fac 10465  df-ihash 10515  df-shft 10580  df-cj 10607  df-re 10608  df-im 10609  df-rsqrt 10763  df-abs 10764  df-clim 11041  df-sumdc 11116
This theorem is referenced by:  ef01bndlem  11452  eirraplem  11472  dveflem  12844
  Copyright terms: Public domain W3C validator