Step | Hyp | Ref
| Expression |
1 | | etransclem23.k |
. . . . . 6
⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1))) |
2 | | etransclem23.l |
. . . . . . 7
⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) |
3 | 2 | oveq1i 7180 |
. . . . . 6
⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))) |
4 | 1, 3 | eqtri 2761 |
. . . . 5
⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))) |
5 | 4 | fveq2i 6677 |
. . . 4
⊢
(abs‘𝐾) =
(abs‘(Σ𝑗 ∈
(0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))) |
7 | | fzfid 13432 |
. . . . 5
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
8 | | etransclem23.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴:ℕ0⟶ℤ) |
9 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ) |
10 | | elfznn0 13091 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
11 | 10 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) |
12 | 9, 11 | ffvelrnd 6862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ) |
13 | 12 | zcnd 12169 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ) |
14 | | ere 15534 |
. . . . . . . . . 10
⊢ e ∈
ℝ |
15 | 14 | recni 10733 |
. . . . . . . . 9
⊢ e ∈
ℂ |
16 | 15 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ) |
17 | | elfzelz 12998 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) |
18 | 17 | zcnd 12169 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ) |
19 | 18 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ) |
20 | 16, 19 | cxpcld 25451 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈
ℂ) |
21 | 13, 20 | mulcld 10739 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑐𝑗)) ∈
ℂ) |
22 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ) |
23 | | elioore 12851 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ) |
24 | 23 | recnd 10747 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ) |
25 | 24 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ) |
26 | 25 | negcld 11062 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ) |
27 | 22, 26 | cxpcld 25451 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈
ℂ) |
28 | | ax-resscn 10672 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
30 | | etransclem23.p |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℕ) |
31 | | etransclem23.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
32 | 29, 30, 31 | etransclem8 43325 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
33 | 32 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ) |
34 | 23 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ) |
35 | 33, 34 | ffvelrnd 6862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ) |
36 | 35 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ) |
37 | 27, 36 | mulcld 10739 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) |
38 | | reelprrecn 10707 |
. . . . . . . . 9
⊢ ℝ
∈ {ℝ, ℂ} |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ,
ℂ}) |
40 | | reopn 42365 |
. . . . . . . . . 10
⊢ ℝ
∈ (topGen‘ran (,)) |
41 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
42 | 41 | tgioo2 23555 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
43 | 40, 42 | eleqtri 2831 |
. . . . . . . . 9
⊢ ℝ
∈ ((TopOpen‘ℂfld) ↾t
ℝ) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
45 | 30 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ) |
46 | | etransclem23.m |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
47 | 46 | nnnn0d 12036 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
48 | 47 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈
ℕ0) |
49 | | etransclem6 43323 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) |
50 | | etransclem6 43323 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) |
51 | 31, 49, 50 | 3eqtri 2765 |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))) |
52 | | 0red 10722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ) |
53 | 17 | zred 12168 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ) |
54 | 53 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ) |
55 | 39, 44, 45, 48, 51, 52, 54 | etransclem18 43335 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈
𝐿1) |
56 | 37, 55 | itgcl 24536 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ) |
57 | 21, 56 | mulcld 10739 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ) |
58 | 7, 57 | fsumcl 15183 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ) |
59 | | nnm1nn0 12017 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
60 | 30, 59 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
61 | 60 | faccld 13736 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ) |
62 | 61 | nncnd 11732 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℂ) |
63 | 61 | nnne0d 11766 |
. . . 4
⊢ (𝜑 → (!‘(𝑃 − 1)) ≠
0) |
64 | 58, 62, 63 | absdivd 14905 |
. . 3
⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1))))) |
65 | 61 | nnred 11731 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℝ) |
66 | 61 | nnnn0d 12036 |
. . . . . 6
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℕ0) |
67 | 66 | nn0ge0d 12039 |
. . . . 5
⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1))) |
68 | 65, 67 | absidd 14872 |
. . . 4
⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1))) |
69 | 68 | oveq2d 7186 |
. . 3
⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1)))) |
70 | 6, 64, 69 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1)))) |
71 | 2, 58 | eqeltrid 2837 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℂ) |
72 | 71, 62, 63 | divcld 11494 |
. . . . . 6
⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈
ℂ) |
73 | 1, 72 | eqeltrid 2837 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℂ) |
74 | 73 | abscld 14886 |
. . . 4
⊢ (𝜑 → (abs‘𝐾) ∈
ℝ) |
75 | 70, 74 | eqeltrrd 2834 |
. . 3
⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈
ℝ) |
76 | 46 | nnred 11731 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℝ) |
77 | 30 | nnnn0d 12036 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
78 | 76, 77 | reexpcld 13619 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ) |
79 | | peano2nn0 12016 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
80 | 47, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
81 | 78, 80 | reexpcld 13619 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ) |
82 | 81 | recnd 10747 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) |
83 | 46 | nncnd 11732 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℂ) |
84 | 82, 83 | mulcomd 10740 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1)))) |
85 | 30 | nncnd 11732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ ℂ) |
86 | | 1cnd 10714 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℂ) |
87 | 85, 86 | npcand 11079 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃) |
88 | 87 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1)) |
89 | 88 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1))) |
90 | 80 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) |
91 | 90, 85 | mulcomd 10740 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1))) |
92 | 91 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1)))) |
93 | 83, 77, 80 | expmuld 13605 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃)) |
94 | 83, 80, 77 | expmuld 13605 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
95 | 92, 93, 94 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
96 | 76, 80 | reexpcld 13619 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ) |
97 | 96 | recnd 10747 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ) |
98 | 97, 60 | expp1d 13603 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) |
99 | 89, 95, 98 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) |
100 | 99 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))) |
101 | 97, 60 | expcld 13602 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈
ℂ) |
102 | 83, 101, 97 | mul12d 10927 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1))))) |
103 | 83, 97 | mulcld 10739 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ) |
104 | 101, 103 | mulcomd 10740 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
105 | 102, 104 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
106 | 84, 100, 105 | 3eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
107 | 106 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
108 | 107 | oveq2d 7186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))) |
109 | 21 | abscld 14886 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈
ℝ) |
110 | 109 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ∈
ℂ) |
111 | 103 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ) |
112 | 101 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈
ℂ) |
113 | 110, 111,
112 | mulassd 10742 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))) |
114 | 108, 113 | eqtr4d 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
115 | 114 | sumeq2dv 15153 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
116 | 110, 111 | mulcld 10739 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ) |
117 | 7, 101, 116 | fsummulc1 15233 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
118 | 115, 117 | eqtr4d 2776 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))) |
119 | 118 | oveq1d 7185 |
. . . . 5
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1)))) |
120 | 7, 116 | fsumcl 15183 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ) |
121 | 120, 101,
62, 63 | divassd 11529 |
. . . . 5
⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1))))) |
122 | 119, 121 | eqtrd 2773 |
. . . 4
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1))))) |
123 | 81 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ) |
124 | 76 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ) |
125 | 123, 124 | remulcld 10749 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ) |
126 | 109, 125 | remulcld 10749 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ) |
127 | 7, 126 | fsumrecl 15184 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ) |
128 | 127, 61 | nndivred 11770 |
. . . 4
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈
ℝ) |
129 | 122, 128 | eqeltrrd 2834 |
. . 3
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈
ℝ) |
130 | | 1red 10720 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
131 | 58 | abscld 14886 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ) |
132 | 61 | nnrpd 12512 |
. . . . 5
⊢ (𝜑 → (!‘(𝑃 − 1)) ∈
ℝ+) |
133 | 57 | abscld 14886 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ) |
134 | 7, 133 | fsumrecl 15184 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ) |
135 | 7, 57 | fsumabs 15249 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥))) |
136 | 81 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ) |
137 | | ioombl 24317 |
. . . . . . . . . . . 12
⊢
(0(,)𝑗) ∈ dom
vol |
138 | 137 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol) |
139 | | 0red 10722 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ) |
140 | | elfzle1 13001 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗) |
141 | | volioo 24321 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 𝑗
∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0)) |
142 | 139, 53, 140, 141 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0)) |
143 | 53, 139 | resubcld 11146 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ) |
144 | 142, 143 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ) |
145 | 144 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ) |
146 | 82 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) |
147 | | iblconstmpt 43039 |
. . . . . . . . . . 11
⊢
(((0(,)𝑗) ∈ dom
vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈
𝐿1) |
148 | 138, 145,
146, 147 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈
𝐿1) |
149 | 136, 148 | itgrecl 24550 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ) |
150 | 109, 149 | remulcld 10749 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ) |
151 | 7, 150 | fsumrecl 15184 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ) |
152 | 21, 56 | absmuld 14904 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ·
(abs‘∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥))) |
153 | 56 | abscld 14886 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ) |
154 | 21 | absge0d 14894 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑𝑐𝑗)))) |
155 | 37 | abscld 14886 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ) |
156 | 37, 55 | iblabs 24581 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦
(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥)))) ∈
𝐿1) |
157 | 155, 156 | itgrecl 24550 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ) |
158 | 37, 55 | itgabs 24587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) d𝑥) |
159 | 27, 36 | absmuld 14904 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) =
((abs‘(e↑𝑐-𝑥)) · (abs‘(𝐹‘𝑥)))) |
160 | 27 | abscld 14886 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘(e↑𝑐-𝑥)) ∈ ℝ) |
161 | | 1red 10720 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ) |
162 | 36 | abscld 14886 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ) |
163 | 27 | absge0d 14894 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤
(abs‘(e↑𝑐-𝑥))) |
164 | 36 | absge0d 14894 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥))) |
165 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ) |
166 | | 0re 10721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℝ |
167 | | epos 15652 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
e |
168 | 166, 14, 167 | ltleii 10841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
e |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e) |
170 | 23 | renegcld 11145 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ) |
171 | 165, 169,
170 | recxpcld 25466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (0(,)𝑗) → (e↑𝑐-𝑥) ∈
ℝ) |
172 | 165, 169,
170 | cxpge0d 25467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤
(e↑𝑐-𝑥)) |
173 | 171, 172 | absidd 14872 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0(,)𝑗) →
(abs‘(e↑𝑐-𝑥)) = (e↑𝑐-𝑥)) |
174 | 173 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘(e↑𝑐-𝑥)) = (e↑𝑐-𝑥)) |
175 | 171 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈
ℝ) |
176 | | 1red 10720 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ) |
177 | | 0xr 10766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈
ℝ*) |
179 | 53 | rexrd 10769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ*) |
180 | 179 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ*) |
181 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗)) |
182 | | ioogtlb 42573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℝ* ∧ 𝑗 ∈ ℝ* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥) |
183 | 178, 180,
181, 182 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥) |
184 | 23 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ) |
185 | 184 | lt0neg2d 11288 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0)) |
186 | 183, 185 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0) |
187 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ) |
188 | | 1lt2 11887 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 <
2 |
189 | | egt2lt3 15651 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 < e
∧ e < 3) |
190 | 189 | simpli 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 <
e |
191 | | 1re 10719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℝ |
192 | | 2re 11790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ |
193 | 191, 192,
14 | lttri 10844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) |
194 | 188, 190,
193 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 <
e |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e) |
196 | 170 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ) |
197 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ) |
198 | 187, 195,
196, 197 | cxpltd 25462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔
(e↑𝑐-𝑥) <
(e↑𝑐0))) |
199 | 186, 198 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) <
(e↑𝑐0)) |
200 | | cxp0 25413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (e ∈
ℂ → (e↑𝑐0) = 1) |
201 | 15, 200 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐0) =
1) |
202 | 199, 201 | breqtrd 5056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) < 1) |
203 | 175, 176,
202 | ltled 10866 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ≤ 1) |
204 | 174, 203 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘(e↑𝑐-𝑥)) ≤ 1) |
205 | 204 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘(e↑𝑐-𝑥)) ≤ 1) |
206 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆
ℂ) |
207 | 30 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ) |
208 | 47 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈
ℕ0) |
209 | 31, 49 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) |
210 | 23 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ) |
211 | 206, 207,
208, 209, 210 | etransclem13 43330 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
212 | 211 | fveq2d 6678 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))) |
213 | | nn0uz 12362 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
214 | 23 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → 𝑥 ∈
ℝ) |
215 | | nn0re 11985 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ ∈ ℕ0
→ ℎ ∈
ℝ) |
216 | 215 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → ℎ ∈ ℝ) |
217 | 214, 216 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → (𝑥 − ℎ) ∈ ℝ) |
218 | 217 | adantll 714 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ0) → (𝑥 − ℎ) ∈ ℝ) |
219 | 60, 77 | ifcld 4460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
220 | 219 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
221 | 218, 220 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ0) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ) |
222 | 221 | recnd 10747 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ0) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
223 | 213, 208,
222 | fprodabs 15420 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))) |
224 | | elfznn0 13091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ0) |
225 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → 𝑥 ∈
ℂ) |
226 | | nn0cn 11986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ ∈ ℕ0
→ ℎ ∈
ℂ) |
227 | 226 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → ℎ ∈ ℂ) |
228 | 225, 227 | subcld 11075 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ0) → (𝑥 − ℎ) ∈ ℂ) |
229 | 228 | adantll 714 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ0) → (𝑥 − ℎ) ∈ ℂ) |
230 | 224, 229 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ) |
231 | 219 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
232 | 230, 231 | absexpd 14902 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
233 | 232 | prodeq2dv 15369 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
234 | 212, 223,
233 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
235 | | nfv 1921 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) |
236 | | fzfid 13432 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin) |
237 | 224, 228 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ) |
238 | 237 | abscld 14886 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ) |
239 | 238 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ) |
240 | 239, 231 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ) |
241 | 237 | absge0d 14894 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ))) |
242 | 241 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ))) |
243 | 239, 231,
242 | expge0d 13620 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
244 | 78 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ) |
245 | 76 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ) |
246 | 245, 231 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ) |
247 | 224, 218 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ) |
248 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ) |
249 | 224, 227 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ) |
250 | 248, 249 | negsubdi2d 11091 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥)) |
251 | 250 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥)) |
252 | 224 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ0) |
253 | 252 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ) |
254 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ) |
255 | 210 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ) |
256 | | elfzle2 13002 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀) |
257 | 256 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀) |
258 | 197, 184,
183 | ltled 10866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥) |
259 | 258 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥) |
260 | 259 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥) |
261 | 253, 254,
245, 255, 257, 260 | le2subd 11338 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0)) |
262 | 83 | subid1d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑀 − 0) = 𝑀) |
263 | 262 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀 − 0) = 𝑀) |
264 | 261, 263 | breqtrd 5056 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ 𝑀) |
265 | 251, 264 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) ≤ 𝑀) |
266 | 247, 245,
265 | lenegcon1d 11300 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ)) |
267 | | elfzel2 12996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ) |
268 | 267 | zred 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ) |
269 | 268 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ) |
270 | 53 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ) |
271 | | iooltub 42588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((0
∈ ℝ* ∧ 𝑗 ∈ ℝ* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗) |
272 | 178, 180,
181, 271 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗) |
273 | | elfzle2 13002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀) |
274 | 273 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀) |
275 | 184, 270,
269, 272, 274 | ltletrd 10878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀) |
276 | 184, 269,
275 | ltled 10866 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀) |
277 | 276 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀) |
278 | 277 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀) |
279 | 252 | nn0ge0d 12039 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ) |
280 | 255, 254,
245, 253, 278, 279 | le2subd 11338 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0)) |
281 | 280, 263 | breqtrd 5056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀) |
282 | 247, 245 | absled 14880 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀))) |
283 | 266, 281,
282 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀) |
284 | | leexp1a 13631 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((abs‘(𝑥
− ℎ)) ∈ ℝ
∧ 𝑀 ∈ ℝ
∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ0) ∧ (0 ≤
(abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
285 | 239, 245,
231, 242, 283, 284 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃))) |
286 | 46 | nnge1d 11764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝑀) |
287 | 286 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀) |
288 | 219 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ) |
289 | 77 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑃 ∈ ℤ) |
290 | | iftrue 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1)) |
291 | 290 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1)) |
292 | 30 | nnred 11731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑃 ∈ ℝ) |
293 | 292 | lem1d 11651 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃) |
294 | 293 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃) |
295 | 291, 294 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃) |
296 | | iffalse 4423 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃) |
297 | 296 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃) |
298 | 292 | leidd 11284 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑃 ≤ 𝑃) |
299 | 298 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃) |
300 | 297, 299 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃) |
301 | 295, 300 | pm2.61dan 813 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃) |
302 | | eluz2 12330 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈
(ℤ≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)) |
303 | 288, 289,
301, 302 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘if(ℎ = 0, (𝑃 − 1), 𝑃))) |
304 | 303 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈
(ℤ≥‘if(ℎ = 0, (𝑃 − 1), 𝑃))) |
305 | 245, 287,
304 | leexp2ad 13709 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃)) |
306 | 240, 246,
244, 285, 305 | letrd 10875 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃)) |
307 | 235, 236,
240, 243, 244, 306 | fprodle 15442 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃)) |
308 | 78 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ) |
309 | | fprodconst 15424 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((0...𝑀) ∈ Fin
∧ (𝑀↑𝑃) ∈ ℂ) →
∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀)))) |
310 | 7, 308, 309 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀)))) |
311 | | hashfz0 13885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ0
→ (♯‘(0...𝑀)) = (𝑀 + 1)) |
312 | 47, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1)) |
313 | 312 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
314 | 310, 313 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
315 | 314 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
316 | 307, 315 | breqtrd 5056 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
317 | 234, 316 | eqbrtrd 5052 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
318 | 160, 161,
162, 136, 163, 164, 205, 317 | lemul12ad 11660 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
((abs‘(e↑𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1)))) |
319 | 82 | mulid2d 10737 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
320 | 319 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1))) |
321 | 318, 320 | breqtrd 5056 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
((abs‘(e↑𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
322 | 159, 321 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) →
(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
323 | 156, 148,
155, 136, 322 | itgle 24562 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) |
324 | 153, 157,
149, 158, 323 | letrd 10875 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) |
325 | 153, 149,
109, 154, 324 | lemul2ad 11658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) ·
(abs‘∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)) |
326 | 152, 325 | eqbrtrd 5052 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)) |
327 | 7, 133, 150, 326 | fsumle 15247 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)) |
328 | | itgconst 24571 |
. . . . . . . . . . 11
⊢
(((0(,)𝑗) ∈ dom
vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) →
∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗)))) |
329 | 138, 145,
146, 328 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗)))) |
330 | 47 | nn0ge0d 12039 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 𝑀) |
331 | 76, 77, 330 | expge0d 13620 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (𝑀↑𝑃)) |
332 | 78, 80, 331 | expge0d 13620 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
333 | 332 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1))) |
334 | 18 | subid1d 11064 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗) |
335 | 142, 334 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗) |
336 | 335, 273 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀) |
337 | 336 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀) |
338 | 145, 124,
123, 333, 337 | lemul2ad 11658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) |
339 | 329, 338 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) |
340 | 149, 125,
109, 154, 339 | lemul2ad 11658 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))) |
341 | 7, 150, 126, 340 | fsumle 15247 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))) |
342 | 134, 151,
127, 327, 341 | letrd 10875 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))) |
343 | 131, 134,
127, 135, 342 | letrd 10875 |
. . . . 5
⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))) |
344 | 131, 127,
132, 343 | lediv1dd 12572 |
. . . 4
⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1)))) |
345 | 344, 122 | breqtrd 5056 |
. . 3
⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1))))) |
346 | | etransclem23.lt1 |
. . 3
⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1) |
347 | 75, 129, 130, 345, 346 | lelttrd 10876 |
. 2
⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) < 1) |
348 | 70, 347 | eqbrtrd 5052 |
1
⊢ (𝜑 → (abs‘𝐾) < 1) |