Metamath Proof Explorer

Theorem etransclem23

Description: This is the claim proof in Juillerat p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem23.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
etransclem23.l ⊢ 𝐿 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 )
etransclem23.k ⊢ 𝐾 = ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) )
etransclem23.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem23.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
etransclem23.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem23.lt1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) < 1 )
Assertion etransclem23 ( 𝜑 → ( abs ‘ 𝐾 ) < 1 )

Proof

Step Hyp Ref Expression
1 etransclem23.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
2 etransclem23.l ⊢ 𝐿 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 )
3 etransclem23.k ⊢ 𝐾 = ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) )
4 etransclem23.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
5 etransclem23.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 etransclem23.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
7 etransclem23.lt1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) < 1 )
8 2 oveq1i ⊢ ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑃 − 1 ) ) )
9 3 8 eqtri ⊢ 𝐾 = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑃 − 1 ) ) )
10 9 fveq2i ⊢ ( abs ‘ 𝐾 ) = ( abs ‘ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
11 10 a1i ⊢ ( 𝜑 → ( abs ‘ 𝐾 ) = ( abs ‘ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
12 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝐴 : ℕ0 ⟶ ℤ )
14 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℕ0 )
16 13 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℤ )
17 16 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
18 ere ⊢ e ∈ ℝ
19 18 recni ⊢ e ∈ ℂ
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → e ∈ ℂ )
21 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
22 21 zcnd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℂ )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℂ )
24 20 23 cxpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( e ↑𝑐 𝑗 ) ∈ ℂ )
25 17 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ∈ ℂ )
26 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → e ∈ ℂ )
27 elioore ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → 𝑥 ∈ ℝ )
28 27 recnd ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → 𝑥 ∈ ℂ )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ∈ ℂ )
30 29 negcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → - 𝑥 ∈ ℂ )
31 26 30 cxpcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 - 𝑥 ) ∈ ℂ )
32 ax-resscn ⊢ ℝ ⊆ ℂ
33 32 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
34 33 4 6 etransclem8 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝐹 : ℝ ⟶ ℂ )
36 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ∈ ℝ )
37 35 36 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
38 37 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
39 31 38 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
40 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ℝ ∈ { ℝ , ℂ } )
42 reopn ⊢ ℝ ∈ ( topGen ‘ ran (,) )
43 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
44 42 43 eleqtri ⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
45 44 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
46 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
47 5 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℕ0 )
49 etransclem6 ⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ ℎ ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − ℎ ) ↑ 𝑃 ) ) )
50 etransclem6 ⊢ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ ℎ ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − ℎ ) ↑ 𝑃 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) ) )
51 6 49 50 3eqtri ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑘 ) ↑ 𝑃 ) ) )
52 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ∈ ℝ )
53 21 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ℝ )
55 41 45 46 48 51 52 54 etransclem18 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 0 (,) 𝑗 ) ↦ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
56 39 55 itgcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ∈ ℂ )
57 25 56 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ∈ ℂ )
58 12 57 fsumcl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ∈ ℂ )
59 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
60 4 59 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
61 60 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
62 61 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
63 61 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
64 58 62 63 absdivd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) = ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( abs ‘ ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
65 61 nnred ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℝ )
66 61 nnnn0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ0 )
67 66 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ! ‘ ( 𝑃 − 1 ) ) )
68 65 67 absidd ⊢ ( 𝜑 → ( abs ‘ ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
69 68 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( abs ‘ ( ! ‘ ( 𝑃 − 1 ) ) ) ) = ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
70 11 64 69 3eqtrd ⊢ ( 𝜑 → ( abs ‘ 𝐾 ) = ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
71 2 58 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
72 71 62 63 divcld ⊢ ( 𝜑 → ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℂ )
73 3 72 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
74 73 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐾 ) ∈ ℝ )
75 70 74 eqeltrrd ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℝ )
76 5 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
77 4 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
78 76 77 reexpcld ⊢ ( 𝜑 → ( 𝑀 ↑ 𝑃 ) ∈ ℝ )
79 peano2nn0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
80 47 79 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
81 78 80 reexpcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
82 81 recnd ⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
83 5 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
84 82 83 mulcomd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) = ( 𝑀 · ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) )
85 4 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
86 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
87 85 86 npcand ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + 1 ) = 𝑃 )
88 87 eqcomd ⊢ ( 𝜑 → 𝑃 = ( ( 𝑃 − 1 ) + 1 ) )
89 88 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑃 ) = ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( ( 𝑃 − 1 ) + 1 ) ) )
90 80 nn0cnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℂ )
91 90 85 mulcomd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑃 ) = ( 𝑃 · ( 𝑀 + 1 ) ) )
92 91 oveq2d ⊢ ( 𝜑 → ( 𝑀 ↑ ( ( 𝑀 + 1 ) · 𝑃 ) ) = ( 𝑀 ↑ ( 𝑃 · ( 𝑀 + 1 ) ) ) )
93 83 77 80 expmuld ⊢ ( 𝜑 → ( 𝑀 ↑ ( ( 𝑀 + 1 ) · 𝑃 ) ) = ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑃 ) )
94 83 80 77 expmuld ⊢ ( 𝜑 → ( 𝑀 ↑ ( 𝑃 · ( 𝑀 + 1 ) ) ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
95 92 93 94 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ 𝑃 ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
96 76 80 reexpcld ⊢ ( 𝜑 → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
97 96 recnd ⊢ ( 𝜑 → ( 𝑀 ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
98 97 60 expp1d ⊢ ( 𝜑 → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( ( 𝑃 − 1 ) + 1 ) ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) )
99 89 95 98 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) )
100 99 oveq2d ⊢ ( 𝜑 → ( 𝑀 · ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) = ( 𝑀 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) )
101 97 60 expcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ∈ ℂ )
102 83 101 97 mul12d ⊢ ( 𝜑 → ( 𝑀 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) = ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) )
103 83 97 mulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
104 101 103 mulcomd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
105 102 104 eqtrd ⊢ ( 𝜑 → ( 𝑀 · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) = ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
106 84 100 105 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) = ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) = ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
108 107 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) ) )
109 25 abscld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) ∈ ℝ )
110 109 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) ∈ ℂ )
111 103 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ∈ ℂ )
112 101 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ∈ ℂ )
113 110 111 112 mulassd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) ) )
114 108 113 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) = ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
115 114 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
116 110 111 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
117 12 101 116 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
118 115 117 eqtr4d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) )
119 118 oveq1d ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
120 12 116 fsumcl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) ∈ ℂ )
121 120 101 62 63 divassd ⊢ ( 𝜑 → ( ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
122 119 121 eqtrd ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
123 81 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
124 76 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℝ )
125 123 124 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ∈ ℝ )
126 109 125 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) ∈ ℝ )
127 12 126 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) ∈ ℝ )
128 127 61 nndivred ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℝ )
129 122 128 eqeltrrd ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ∈ ℝ )
130 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
131 58 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ∈ ℝ )
132 61 nnrpd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℝ+ )
133 57 abscld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ∈ ℝ )
134 12 133 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ∈ ℝ )
135 12 57 fsumabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) )
136 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℝ )
137 ioombl ⊢ ( 0 (,) 𝑗 ) ∈ dom vol
138 137 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 0 (,) 𝑗 ) ∈ dom vol )
139 0red ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ∈ ℝ )
140 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑗 )
141 volioo ⊢ ( ( 0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗 ) → ( vol ‘ ( 0 (,) 𝑗 ) ) = ( 𝑗 − 0 ) )
142 139 53 140 141 syl3anc ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( vol ‘ ( 0 (,) 𝑗 ) ) = ( 𝑗 − 0 ) )
143 53 139 resubcld ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 0 ) ∈ ℝ )
144 142 143 eqeltrd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( vol ‘ ( 0 (,) 𝑗 ) ) ∈ ℝ )
145 144 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( vol ‘ ( 0 (,) 𝑗 ) ) ∈ ℝ )
146 82 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ )
147 iblconstmpt ⊢ ( ( ( 0 (,) 𝑗 ) ∈ dom vol ∧ ( vol ‘ ( 0 (,) 𝑗 ) ) ∈ ℝ ∧ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ ) → ( 𝑥 ∈ ( 0 (,) 𝑗 ) ↦ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) ∈ 𝐿1 )
148 138 145 146 147 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 0 (,) 𝑗 ) ↦ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) ∈ 𝐿1 )
149 136 148 itgrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ∈ ℝ )
150 109 149 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) ∈ ℝ )
151 12 150 fsumrecl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) ∈ ℝ )
152 25 56 absmuld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) = ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( abs ‘ ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) )
153 56 abscld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ∈ ℝ )
154 25 absge0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) )
155 39 abscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
156 39 55 iblabs ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 ∈ ( 0 (,) 𝑗 ) ↦ ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ 𝐿1 )
157 155 156 itgrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) d 𝑥 ∈ ℝ )
158 39 55 itgabs ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ≤ ∫ ( 0 (,) 𝑗 ) ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) d 𝑥 )
159 31 38 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
160 31 abscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) ∈ ℝ )
161 1red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 1 ∈ ℝ )
162 38 abscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
163 31 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ≤ ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) )
164 38 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
165 18 a1i ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → e ∈ ℝ )
166 0re ⊢ 0 ∈ ℝ
167 epos ⊢ 0 < e
168 166 18 167 ltleii ⊢ 0 ≤ e
169 168 a1i ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → 0 ≤ e )
170 27 renegcld ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → - 𝑥 ∈ ℝ )
171 165 169 170 recxpcld ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → ( e ↑𝑐 - 𝑥 ) ∈ ℝ )
172 165 169 170 cxpge0d ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → 0 ≤ ( e ↑𝑐 - 𝑥 ) )
173 171 172 absidd ⊢ ( 𝑥 ∈ ( 0 (,) 𝑗 ) → ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) = ( e ↑𝑐 - 𝑥 ) )
174 173 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) = ( e ↑𝑐 - 𝑥 ) )
175 171 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 - 𝑥 ) ∈ ℝ )
176 1red ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 1 ∈ ℝ )
177 0xr ⊢ 0 ∈ ℝ*
178 177 a1i ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ∈ ℝ* )
179 53 rexrd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℝ* )
180 179 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑗 ∈ ℝ* )
181 simpr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ∈ ( 0 (,) 𝑗 ) )
182 ioogtlb ⊢ ( ( 0 ∈ ℝ* ∧ 𝑗 ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 < 𝑥 )
183 178 180 181 182 syl3anc ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 < 𝑥 )
184 27 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ∈ ℝ )
185 184 lt0neg2d ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 0 < 𝑥 ↔ - 𝑥 < 0 ) )
186 183 185 mpbid ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → - 𝑥 < 0 )
187 18 a1i ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → e ∈ ℝ )
188 1lt2 ⊢ 1 < 2
189 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
190 189 simpli ⊢ 2 < e
191 1re ⊢ 1 ∈ ℝ
192 2re ⊢ 2 ∈ ℝ
193 191 192 18 lttri ⊢ ( ( 1 < 2 ∧ 2 < e ) → 1 < e )
194 188 190 193 mp2an ⊢ 1 < e
195 194 a1i ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 1 < e )
196 170 adantl ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → - 𝑥 ∈ ℝ )
197 0red ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ∈ ℝ )
198 187 195 196 197 cxpltd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( - 𝑥 < 0 ↔ ( e ↑𝑐 - 𝑥 ) < ( e ↑𝑐 0 ) ) )
199 186 198 mpbid ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 - 𝑥 ) < ( e ↑𝑐 0 ) )
200 cxp0 ⊢ ( e ∈ ℂ → ( e ↑𝑐 0 ) = 1 )
201 19 200 mp1i ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 0 ) = 1 )
202 199 201 breqtrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 - 𝑥 ) < 1 )
203 175 176 202 ltled ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( e ↑𝑐 - 𝑥 ) ≤ 1 )
204 174 203 eqbrtrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) ≤ 1 )
205 204 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) ≤ 1 )
206 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ℝ ⊆ ℂ )
207 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑃 ∈ ℕ )
208 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑀 ∈ ℕ0 )
209 6 49 eqtri ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 ↑ ( 𝑃 − 1 ) ) · ∏ ℎ ∈ ( 1 ... 𝑀 ) ( ( 𝑦 − ℎ ) ↑ 𝑃 ) ) )
210 27 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ∈ ℝ )
211 206 207 208 209 210 etransclem13 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 𝐹 ‘ 𝑥 ) = ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
212 211 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
213 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
214 27 adantr ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → 𝑥 ∈ ℝ )
215 nn0re ⊢ ( ℎ ∈ ℕ0 → ℎ ∈ ℝ )
216 215 adantl ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → ℎ ∈ ℝ )
217 214 216 resubcld ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → ( 𝑥 − ℎ ) ∈ ℝ )
218 217 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ℕ0 ) → ( 𝑥 − ℎ ) ∈ ℝ )
219 60 77 ifcld ⊢ ( 𝜑 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
220 219 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ℕ0 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
221 218 220 reexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ℕ0 ) → ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℝ )
222 221 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ℕ0 ) → ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℂ )
223 213 208 222 fprodabs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ∏ ℎ ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
224 elfznn0 ⊢ ( ℎ ∈ ( 0 ... 𝑀 ) → ℎ ∈ ℕ0 )
225 28 adantr ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → 𝑥 ∈ ℂ )
226 nn0cn ⊢ ( ℎ ∈ ℕ0 → ℎ ∈ ℂ )
227 226 adantl ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → ℎ ∈ ℂ )
228 225 227 subcld ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ℕ0 ) → ( 𝑥 − ℎ ) ∈ ℂ )
229 228 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ℕ0 ) → ( 𝑥 − ℎ ) ∈ ℂ )
230 224 229 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − ℎ ) ∈ ℂ )
231 219 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
232 230 231 absexpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
233 232 prodeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( 𝑥 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) = ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
234 212 223 233 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
235 nfv ⊢ Ⅎ ℎ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) )
236 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
237 224 228 sylan2 ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − ℎ ) ∈ ℂ )
238 237 abscld ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( 𝑥 − ℎ ) ) ∈ ℝ )
239 238 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( 𝑥 − ℎ ) ) ∈ ℝ )
240 239 231 reexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℝ )
241 237 absge0d ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( abs ‘ ( 𝑥 − ℎ ) ) )
242 241 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( abs ‘ ( 𝑥 − ℎ ) ) )
243 239 231 242 expge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
244 78 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 ↑ 𝑃 ) ∈ ℝ )
245 76 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℝ )
246 245 231 reexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∈ ℝ )
247 224 218 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − ℎ ) ∈ ℝ )
248 28 adantr ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℂ )
249 224 227 sylan2 ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ℎ ∈ ℂ )
250 248 249 negsubdi2d ⊢ ( ( 𝑥 ∈ ( 0 (,) 𝑗 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → - ( 𝑥 − ℎ ) = ( ℎ − 𝑥 ) )
251 250 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → - ( 𝑥 − ℎ ) = ( ℎ − 𝑥 ) )
252 224 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ℎ ∈ ℕ0 )
253 252 nn0red ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ℎ ∈ ℝ )
254 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ∈ ℝ )
255 210 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ ℝ )
256 elfzle2 ⊢ ( ℎ ∈ ( 0 ... 𝑀 ) → ℎ ≤ 𝑀 )
257 256 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ℎ ≤ 𝑀 )
258 197 184 183 ltled ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ≤ 𝑥 )
259 258 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 0 ≤ 𝑥 )
260 259 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ≤ 𝑥 )
261 253 254 245 255 257 260 le2subd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ℎ − 𝑥 ) ≤ ( 𝑀 − 0 ) )
262 83 subid1d ⊢ ( 𝜑 → ( 𝑀 − 0 ) = 𝑀 )
263 262 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 − 0 ) = 𝑀 )
264 261 263 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ℎ − 𝑥 ) ≤ 𝑀 )
265 251 264 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → - ( 𝑥 − ℎ ) ≤ 𝑀 )
266 247 245 265 lenegcon1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → - 𝑀 ≤ ( 𝑥 − ℎ ) )
267 elfzel2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
268 267 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
269 268 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑀 ∈ ℝ )
270 53 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑗 ∈ ℝ )
271 iooltub ⊢ ( ( 0 ∈ ℝ* ∧ 𝑗 ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 < 𝑗 )
272 178 180 181 271 syl3anc ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 < 𝑗 )
273 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ≤ 𝑀 )
274 273 adantr ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑗 ≤ 𝑀 )
275 184 270 269 272 274 ltletrd ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 < 𝑀 )
276 184 269 275 ltled ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑀 ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ≤ 𝑀 )
277 276 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → 𝑥 ≤ 𝑀 )
278 277 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 𝑥 ≤ 𝑀 )
279 252 nn0ge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ℎ )
280 255 254 245 253 278 279 le2subd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − ℎ ) ≤ ( 𝑀 − 0 ) )
281 280 263 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑥 − ℎ ) ≤ 𝑀 )
282 247 245 absled ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( 𝑥 − ℎ ) ) ≤ 𝑀 ↔ ( - 𝑀 ≤ ( 𝑥 − ℎ ) ∧ ( 𝑥 − ℎ ) ≤ 𝑀 ) ) )
283 266 281 282 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( 𝑥 − ℎ ) ) ≤ 𝑀 )
284 leexp1a ⊢ ( ( ( ( abs ‘ ( 𝑥 − ℎ ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 ) ∧ ( 0 ≤ ( abs ‘ ( 𝑥 − ℎ ) ) ∧ ( abs ‘ ( 𝑥 − ℎ ) ) ≤ 𝑀 ) ) → ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ( 𝑀 ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
285 239 245 231 242 283 284 syl32anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ( 𝑀 ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
286 5 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
287 286 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 1 ≤ 𝑀 )
288 219 nn0zd ⊢ ( 𝜑 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
289 77 nn0zd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
290 iftrue ⊢ ( ℎ = 0 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
291 290 adantl ⊢ ( ( 𝜑 ∧ ℎ = 0 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
292 4 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
293 292 lem1d ⊢ ( 𝜑 → ( 𝑃 − 1 ) ≤ 𝑃 )
294 293 adantr ⊢ ( ( 𝜑 ∧ ℎ = 0 ) → ( 𝑃 − 1 ) ≤ 𝑃 )
295 291 294 eqbrtrd ⊢ ( ( 𝜑 ∧ ℎ = 0 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ≤ 𝑃 )
296 iffalse ⊢ ( ¬ ℎ = 0 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
297 296 adantl ⊢ ( ( 𝜑 ∧ ¬ ℎ = 0 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
298 292 leidd ⊢ ( 𝜑 → 𝑃 ≤ 𝑃 )
299 298 adantr ⊢ ( ( 𝜑 ∧ ¬ ℎ = 0 ) → 𝑃 ≤ 𝑃 )
300 297 299 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ℎ = 0 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ≤ 𝑃 )
301 295 300 pm2.61dan ⊢ ( 𝜑 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ≤ 𝑃 )
302 eluz2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ↔ ( if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ≤ 𝑃 ) )
303 288 289 301 302 syl3anbrc ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
304 303 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ( ℤ≥ ‘ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
305 245 287 304 leexp2ad ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑀 ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ( 𝑀 ↑ 𝑃 ) )
306 240 246 244 285 305 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ( 𝑀 ↑ 𝑃 ) )
307 235 236 240 243 244 306 fprodle ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ∏ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑀 ↑ 𝑃 ) )
308 78 recnd ⊢ ( 𝜑 → ( 𝑀 ↑ 𝑃 ) ∈ ℂ )
309 fprodconst ⊢ ( ( ( 0 ... 𝑀 ) ∈ Fin ∧ ( 𝑀 ↑ 𝑃 ) ∈ ℂ ) → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑀 ↑ 𝑃 ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( ♯ ‘ ( 0 ... 𝑀 ) ) ) )
310 12 308 309 syl2anc ⊢ ( 𝜑 → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑀 ↑ 𝑃 ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( ♯ ‘ ( 0 ... 𝑀 ) ) ) )
311 hashfz0 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑀 ) ) = ( 𝑀 + 1 ) )
312 47 311 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝑀 ) ) = ( 𝑀 + 1 ) )
313 312 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑃 ) ↑ ( ♯ ‘ ( 0 ... 𝑀 ) ) ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
314 310 313 eqtrd ⊢ ( 𝜑 → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑀 ↑ 𝑃 ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
315 314 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑀 ↑ 𝑃 ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
316 307 315 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ∏ ℎ ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( 𝑥 − ℎ ) ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
317 234 316 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
318 160 161 162 136 163 164 205 317 lemul12ad ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 1 · ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) )
319 82 mullidd ⊢ ( 𝜑 → ( 1 · ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
320 319 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( 1 · ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ) = ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
321 318 320 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( ( abs ‘ ( e ↑𝑐 - 𝑥 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
322 159 321 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑥 ∈ ( 0 (,) 𝑗 ) ) → ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
323 156 148 155 136 322 itgle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( abs ‘ ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) ) d 𝑥 ≤ ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 )
324 153 157 149 158 323 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ≤ ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 )
325 153 149 109 154 324 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( abs ‘ ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) )
326 152 325 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) )
327 12 133 150 326 fsumle ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) )
328 itgconst ⊢ ( ( ( 0 (,) 𝑗 ) ∈ dom vol ∧ ( vol ‘ ( 0 (,) 𝑗 ) ) ∈ ℝ ∧ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) ∈ ℂ ) → ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 = ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · ( vol ‘ ( 0 (,) 𝑗 ) ) ) )
329 138 145 146 328 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 = ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · ( vol ‘ ( 0 (,) 𝑗 ) ) ) )
330 47 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑀 )
331 76 77 330 expge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑀 ↑ 𝑃 ) )
332 78 80 331 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
333 332 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) )
334 22 subid1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( 𝑗 − 0 ) = 𝑗 )
335 142 334 eqtrd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( vol ‘ ( 0 (,) 𝑗 ) ) = 𝑗 )
336 335 273 eqbrtrd ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( vol ‘ ( 0 (,) 𝑗 ) ) ≤ 𝑀 )
337 336 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( vol ‘ ( 0 (,) 𝑗 ) ) ≤ 𝑀 )
338 145 124 123 333 337 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · ( vol ‘ ( 0 (,) 𝑗 ) ) ) ≤ ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) )
339 329 338 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ≤ ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) )
340 149 125 109 154 339 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) ≤ ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) )
341 12 150 126 340 fsumle ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ∫ ( 0 (,) 𝑗 ) ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) d 𝑥 ) ≤ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) )
342 134 151 127 327 341 letrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( abs ‘ ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) )
343 131 134 127 135 342 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) ≤ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) )
344 131 127 132 343 lediv1dd ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ≤ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( ( ( 𝑀 ↑ 𝑃 ) ↑ ( 𝑀 + 1 ) ) · 𝑀 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
345 344 122 breqtrd ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ≤ ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
346 75 129 130 345 7 lelttrd ⊢ ( 𝜑 → ( ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) < 1 )
347 70 346 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ 𝐾 ) < 1 )