Proof of Theorem fourierdlem47
Step | Hyp | Ref
| Expression |
1 | | fourierdlem47.m |
. . 3
⊢ 𝑀 = ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1) |
2 | | fourierdlem47.x |
. . . . . . . . . . 11
⊢ 𝑋 = (abs‘𝐴) |
3 | | fourierdlem47.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | 3 | abscld 15321 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
5 | 2, 4 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
6 | | fourierdlem47.y |
. . . . . . . . . . 11
⊢ 𝑌 = (abs‘𝐶) |
7 | | fourierdlem47.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
8 | 7 | abscld 15321 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
9 | 6, 8 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
10 | 5, 9 | readdcld 11184 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ) |
11 | | fourierdlem47.z |
. . . . . . . . . 10
⊢ 𝑍 = ∫𝐼(abs‘𝐹) d𝑥 |
12 | | fourierdlem47.f |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ) |
13 | 12 | abscld 15321 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℝ) |
14 | | fourierdlem47.ibl |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐹) ∈
𝐿1) |
15 | 12, 14 | iblabs 25193 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (abs‘𝐹)) ∈
𝐿1) |
16 | 13, 15 | itgrecl 25162 |
. . . . . . . . . 10
⊢ (𝜑 → ∫𝐼(abs‘𝐹) d𝑥 ∈ ℝ) |
17 | 11, 16 | eqeltrid 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ ℝ) |
18 | 10, 17 | readdcld 11184 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ) |
19 | | fourierdlem47.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
20 | 19 | rpred 12957 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℝ) |
21 | 19 | rpne0d 12962 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ≠ 0) |
22 | 18, 20, 21 | redivcld 11983 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ) |
23 | | 1red 11156 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
24 | 22, 23 | readdcld 11184 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ) |
25 | 24 | flcld 13703 |
. . . . 5
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℤ) |
26 | | 0red 11158 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
27 | | reflcl 13701 |
. . . . . . 7
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
28 | 24, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
29 | | 0lt1 11677 |
. . . . . . 7
⊢ 0 <
1 |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 < 1) |
31 | 3 | absge0d 15329 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) |
32 | 31, 2 | breqtrrdi 5147 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑋) |
33 | 7 | absge0d 15329 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) |
34 | 33, 6 | breqtrrdi 5147 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑌) |
35 | 5, 9, 32, 34 | addge0d 11731 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝑋 + 𝑌)) |
36 | 12 | absge0d 15329 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ≤ (abs‘𝐹)) |
37 | 15, 13, 36 | itgge0 25175 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ∫𝐼(abs‘𝐹) d𝑥) |
38 | 37, 11 | breqtrrdi 5147 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑍) |
39 | 10, 17, 35, 38 | addge0d 11731 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ ((𝑋 + 𝑌) + 𝑍)) |
40 | 18, 19, 39 | divge0d 12997 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) |
41 | | flge0nn0 13725 |
. . . . . . . . 9
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ ∧ 0 ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈
ℕ0) |
42 | 22, 40, 41 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈
ℕ0) |
43 | | nn0addge1 12459 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈ ℕ0) → 1 ≤
(1 + (⌊‘(((𝑋 +
𝑌) + 𝑍) / 𝐸)))) |
44 | 23, 42, 43 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ (1 +
(⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)))) |
45 | | 1z 12533 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
46 | | fladdz 13730 |
. . . . . . . . 9
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘((((𝑋
+ 𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
47 | 22, 45, 46 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
48 | 42 | nn0cnd 12475 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈ ℂ) |
49 | 23 | recnd 11183 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
50 | 48, 49 | addcomd 11357 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1) = (1 + (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)))) |
51 | 47, 50 | eqtr2d 2777 |
. . . . . . 7
⊢ (𝜑 → (1 +
(⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸))) = (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
52 | 44, 51 | breqtrd 5131 |
. . . . . 6
⊢ (𝜑 → 1 ≤
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1))) |
53 | 26, 23, 28, 30, 52 | ltletrd 11315 |
. . . . 5
⊢ (𝜑 → 0 <
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1))) |
54 | | elnnz 12509 |
. . . . 5
⊢
((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℕ ↔
((⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℤ ∧ 0 <
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)))) |
55 | 25, 53, 54 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℕ) |
56 | 55 | peano2nnd 12170 |
. . 3
⊢ (𝜑 → ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1) ∈
ℕ) |
57 | 1, 56 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
58 | | elioore 13294 |
. . . . 5
⊢ (𝑟 ∈ (𝑀(,)+∞) → 𝑟 ∈ ℝ) |
59 | | fourierdlem47.iblmul |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈
𝐿1) |
60 | 58, 59 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈
𝐿1) |
61 | 12 | adantlr 713 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ) |
62 | | simpll 765 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝜑) |
63 | | simpr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
64 | 58 | ad2antlr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ) |
65 | 64 | recnd 11183 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℂ) |
66 | | fourierdlem47.g |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℂ) → 𝐺 ∈ ℂ) |
67 | 62, 63, 65, 66 | syl21anc 836 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ ℂ) |
68 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐴 ∈ ℂ) |
69 | 7 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐶 ∈ ℂ) |
70 | | eqid 2736 |
. . . 4
⊢
(abs‘∫𝐼(𝐹 · -𝐺) d𝑥) = (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) |
71 | 19 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ∈
ℝ+) |
72 | 58 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ ℝ) |
73 | 2 | eqcomi 2745 |
. . . . . . . . . 10
⊢
(abs‘𝐴) =
𝑋 |
74 | 6 | eqcomi 2745 |
. . . . . . . . . 10
⊢
(abs‘𝐶) =
𝑌 |
75 | 73, 74 | oveq12i 7369 |
. . . . . . . . 9
⊢
((abs‘𝐴) +
(abs‘𝐶)) = (𝑋 + 𝑌) |
76 | 75 | oveq1i 7367 |
. . . . . . . 8
⊢
(((abs‘𝐴) +
(abs‘𝐶)) +
(abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) = ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) |
77 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐴) ∈
ℝ) |
78 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐶) ∈
ℝ) |
79 | 77, 78 | readdcld 11184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((abs‘𝐴) + (abs‘𝐶)) ∈ ℝ) |
80 | 67 | negcld 11499 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → -𝐺 ∈ ℂ) |
81 | 61, 80 | mulcld 11175 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (𝐹 · -𝐺) ∈ ℂ) |
82 | 81, 60 | itgcl 25148 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(𝐹 · -𝐺) d𝑥 ∈ ℂ) |
83 | 82 | abscld 15321 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ∈ ℝ) |
84 | 79, 83 | readdcld 11184 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((abs‘𝐴) + (abs‘𝐶)) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ∈ ℝ) |
85 | 76, 84 | eqeltrrid 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ∈ ℝ) |
86 | 20 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ∈ ℝ) |
87 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ≠ 0) |
88 | 85, 86, 87 | redivcld 11983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) ∈ ℝ) |
89 | | 1red 11156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 1 ∈
ℝ) |
90 | 88, 89 | readdcld 11184 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) ∈ ℝ) |
91 | 2, 77 | eqeltrid 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑋 ∈ ℝ) |
92 | 6, 78 | eqeltrid 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑌 ∈ ℝ) |
93 | 91, 92 | readdcld 11184 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑋 + 𝑌) ∈ ℝ) |
94 | 17 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑍 ∈ ℝ) |
95 | 93, 94 | readdcld 11184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ) |
96 | 95, 86, 87 | redivcld 11983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ) |
97 | 96, 89 | readdcld 11184 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ) |
98 | 97, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
99 | 98, 89 | readdcld 11184 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
((⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) + 1) ∈
ℝ) |
100 | 1, 99 | eqeltrid 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 ∈ ℝ) |
101 | 81 | abscld 15321 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) ∈ ℝ) |
102 | 81, 60 | iblabs 25193 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (abs‘(𝐹 · -𝐺))) ∈
𝐿1) |
103 | 101, 102 | itgrecl 25162 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ∈ ℝ) |
104 | 81, 60 | itgabs 25199 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ≤ ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥) |
105 | 15 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (abs‘𝐹)) ∈
𝐿1) |
106 | 61 | abscld 15321 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℝ) |
107 | 61, 80 | absmuld 15339 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) = ((abs‘𝐹) · (abs‘-𝐺))) |
108 | 80 | abscld 15321 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘-𝐺) ∈ ℝ) |
109 | | 1red 11156 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 1 ∈ ℝ) |
110 | 61 | absge0d 15329 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (abs‘𝐹)) |
111 | | recn 11141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℂ) |
112 | 111, 66 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → 𝐺 ∈ ℂ) |
113 | 112 | absnegd 15334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘-𝐺) = (abs‘𝐺)) |
114 | | fourierdlem47.absg |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘𝐺) ≤ 1) |
115 | 113, 114 | eqbrtrd 5127 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘-𝐺) ≤ 1) |
116 | 62, 63, 64, 115 | syl21anc 836 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘-𝐺) ≤ 1) |
117 | 108, 109,
106, 110, 116 | lemul2ad 12095 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · (abs‘-𝐺)) ≤ ((abs‘𝐹) · 1)) |
118 | 106 | recnd 11183 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℂ) |
119 | 118 | mulid1d 11172 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · 1) = (abs‘𝐹)) |
120 | 117, 119 | breqtrd 5131 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · (abs‘-𝐺)) ≤ (abs‘𝐹)) |
121 | 107, 120 | eqbrtrd 5127 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) ≤ (abs‘𝐹)) |
122 | 102, 105,
101, 106, 121 | itgle 25174 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ≤ ∫𝐼(abs‘𝐹) d𝑥) |
123 | 122, 11 | breqtrrdi 5147 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ≤ 𝑍) |
124 | 83, 103, 94, 104, 123 | letrd 11312 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ≤ 𝑍) |
125 | 83, 94, 93, 124 | leadd2dd 11770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ≤ ((𝑋 + 𝑌) + 𝑍)) |
126 | 85, 95, 71, 125 | lediv1dd 13015 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) |
127 | | flltp1 13705 |
. . . . . . . . . . 11
⊢ ((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
128 | 96, 127 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
129 | 96, 45, 46 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
130 | 128, 129 | breqtrrd 5133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
131 | 88, 96, 98, 126, 130 | lelttrd 11313 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) < (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
132 | 88, 98, 89, 131 | ltadd1dd 11766 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1)) |
133 | 132, 1 | breqtrrdi 5147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < 𝑀) |
134 | 100 | rexrd 11205 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 ∈
ℝ*) |
135 | | pnfxr 11209 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
136 | 135 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → +∞ ∈
ℝ*) |
137 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ (𝑀(,)+∞)) |
138 | | ioogtlb 43723 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 < 𝑟) |
139 | 134, 136,
137, 138 | syl3anc 1371 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 < 𝑟) |
140 | 90, 100, 72, 133, 139 | lttrd 11316 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < 𝑟) |
141 | 90, 72, 140 | ltled 11303 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) ≤ 𝑟) |
142 | 72 | recnd 11183 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ ℂ) |
143 | | fourierdlem47.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐵 ∈ ℂ) |
144 | 142, 143 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐵 ∈ ℂ) |
145 | | fourierdlem47.absb |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐵) ≤ 1) |
146 | 58, 145 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐵) ≤ 1) |
147 | | fourierdlem47.d |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐷 ∈ ℂ) |
148 | 142, 147 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐷 ∈ ℂ) |
149 | | fourierdlem47.absd |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐷) ≤ 1) |
150 | 58, 149 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐷) ≤ 1) |
151 | 60, 61, 67, 68, 2, 69, 6, 70, 71, 72, 141, 144, 146, 148, 150 | fourierdlem30 44368 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
152 | 151 | ralrimiva 3143 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
153 | | oveq1 7364 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑚(,)+∞) = (𝑀(,)+∞)) |
154 | 153 | raleqdv 3313 |
. . 3
⊢ (𝑚 = 𝑀 → (∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸 ↔ ∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸)) |
155 | 154 | rspcev 3581 |
. 2
⊢ ((𝑀 ∈ ℕ ∧
∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
156 | 57, 152, 155 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |