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