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 15000 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
5 | 2, 4 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
6 | | fourierdlem47.y |
. . . . . . . . . . 11
⊢ 𝑌 = (abs‘𝐶) |
7 | | fourierdlem47.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
8 | 7 | abscld 15000 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
9 | 6, 8 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℝ) |
10 | 5, 9 | readdcld 10862 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 + 𝑌) ∈ ℝ) |
11 | | fourierdlem47.z |
. . . . . . . . . 10
⊢ 𝑍 = ∫𝐼(abs‘𝐹) d𝑥 |
12 | | fourierdlem47.f |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ) |
13 | 12 | abscld 15000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℝ) |
14 | | fourierdlem47.ibl |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐹) ∈
𝐿1) |
15 | 12, 14 | iblabs 24726 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (abs‘𝐹)) ∈
𝐿1) |
16 | 13, 15 | itgrecl 24695 |
. . . . . . . . . 10
⊢ (𝜑 → ∫𝐼(abs‘𝐹) d𝑥 ∈ ℝ) |
17 | 11, 16 | eqeltrid 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ ℝ) |
18 | 10, 17 | readdcld 10862 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ) |
19 | | fourierdlem47.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
20 | 19 | rpred 12628 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℝ) |
21 | 19 | rpne0d 12633 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ≠ 0) |
22 | 18, 20, 21 | redivcld 11660 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ) |
23 | | 1red 10834 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
24 | 22, 23 | readdcld 10862 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ) |
25 | 24 | flcld 13373 |
. . . . 5
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℤ) |
26 | | 0red 10836 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
27 | | reflcl 13371 |
. . . . . . 7
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
28 | 24, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
29 | | 0lt1 11354 |
. . . . . . 7
⊢ 0 <
1 |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 < 1) |
31 | 3 | absge0d 15008 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (abs‘𝐴)) |
32 | 31, 2 | breqtrrdi 5095 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑋) |
33 | 7 | absge0d 15008 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) |
34 | 33, 6 | breqtrrdi 5095 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑌) |
35 | 5, 9, 32, 34 | addge0d 11408 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (𝑋 + 𝑌)) |
36 | 12 | absge0d 15008 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ≤ (abs‘𝐹)) |
37 | 15, 13, 36 | itgge0 24708 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ∫𝐼(abs‘𝐹) d𝑥) |
38 | 37, 11 | breqtrrdi 5095 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝑍) |
39 | 10, 17, 35, 38 | addge0d 11408 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ ((𝑋 + 𝑌) + 𝑍)) |
40 | 18, 19, 39 | divge0d 12668 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) |
41 | | flge0nn0 13395 |
. . . . . . . . 9
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ ∧ 0 ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈
ℕ0) |
42 | 22, 40, 41 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈
ℕ0) |
43 | | nn0addge1 12136 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈ ℕ0) → 1 ≤
(1 + (⌊‘(((𝑋 +
𝑌) + 𝑍) / 𝐸)))) |
44 | 23, 42, 43 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ (1 +
(⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)))) |
45 | | 1z 12207 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
46 | | fladdz 13400 |
. . . . . . . . 9
⊢
(((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘((((𝑋
+ 𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
47 | 22, 45, 46 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
48 | 42 | nn0cnd 12152 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) ∈ ℂ) |
49 | 23 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
50 | 48, 49 | addcomd 11034 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1) = (1 + (⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)))) |
51 | 47, 50 | eqtr2d 2778 |
. . . . . . 7
⊢ (𝜑 → (1 +
(⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸))) = (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
52 | 44, 51 | breqtrd 5079 |
. . . . . 6
⊢ (𝜑 → 1 ≤
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1))) |
53 | 26, 23, 28, 30, 52 | ltletrd 10992 |
. . . . 5
⊢ (𝜑 → 0 <
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1))) |
54 | | elnnz 12186 |
. . . . 5
⊢
((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℕ ↔
((⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℤ ∧ 0 <
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)))) |
55 | 25, 53, 54 | sylanbrc 586 |
. . . 4
⊢ (𝜑 → (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℕ) |
56 | 55 | peano2nnd 11847 |
. . 3
⊢ (𝜑 → ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1) ∈
ℕ) |
57 | 1, 56 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
58 | | elioore 12965 |
. . . . 5
⊢ (𝑟 ∈ (𝑀(,)+∞) → 𝑟 ∈ ℝ) |
59 | | fourierdlem47.iblmul |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈
𝐿1) |
60 | 58, 59 | sylan2 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈
𝐿1) |
61 | 12 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ) |
62 | | simpll 767 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝜑) |
63 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
64 | 58 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℝ) |
65 | 64 | recnd 10861 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝑟 ∈ ℂ) |
66 | | fourierdlem47.g |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℂ) → 𝐺 ∈ ℂ) |
67 | 62, 63, 65, 66 | syl21anc 838 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ ℂ) |
68 | 3 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐴 ∈ ℂ) |
69 | 7 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐶 ∈ ℂ) |
70 | | eqid 2737 |
. . . 4
⊢
(abs‘∫𝐼(𝐹 · -𝐺) d𝑥) = (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) |
71 | 19 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ∈
ℝ+) |
72 | 58 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ ℝ) |
73 | 2 | eqcomi 2746 |
. . . . . . . . . 10
⊢
(abs‘𝐴) =
𝑋 |
74 | 6 | eqcomi 2746 |
. . . . . . . . . 10
⊢
(abs‘𝐶) =
𝑌 |
75 | 73, 74 | oveq12i 7225 |
. . . . . . . . 9
⊢
((abs‘𝐴) +
(abs‘𝐶)) = (𝑋 + 𝑌) |
76 | 75 | oveq1i 7223 |
. . . . . . . 8
⊢
(((abs‘𝐴) +
(abs‘𝐶)) +
(abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) = ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) |
77 | 4 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐴) ∈
ℝ) |
78 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐶) ∈
ℝ) |
79 | 77, 78 | readdcld 10862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((abs‘𝐴) + (abs‘𝐶)) ∈ ℝ) |
80 | 67 | negcld 11176 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → -𝐺 ∈ ℂ) |
81 | 61, 80 | mulcld 10853 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (𝐹 · -𝐺) ∈ ℂ) |
82 | 81, 60 | itgcl 24681 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(𝐹 · -𝐺) d𝑥 ∈ ℂ) |
83 | 82 | abscld 15000 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ∈ ℝ) |
84 | 79, 83 | readdcld 10862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((abs‘𝐴) + (abs‘𝐶)) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ∈ ℝ) |
85 | 76, 84 | eqeltrrid 2843 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ∈ ℝ) |
86 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ∈ ℝ) |
87 | 21 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐸 ≠ 0) |
88 | 85, 86, 87 | redivcld 11660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) ∈ ℝ) |
89 | | 1red 10834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 1 ∈
ℝ) |
90 | 88, 89 | readdcld 10862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) ∈ ℝ) |
91 | 2, 77 | eqeltrid 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑋 ∈ ℝ) |
92 | 6, 78 | eqeltrid 2842 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑌 ∈ ℝ) |
93 | 91, 92 | readdcld 10862 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑋 + 𝑌) ∈ ℝ) |
94 | 17 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑍 ∈ ℝ) |
95 | 93, 94 | readdcld 10862 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + 𝑍) ∈ ℝ) |
96 | 95, 86, 87 | redivcld 11660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ) |
97 | 96, 89 | readdcld 10862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ∈ ℝ) |
98 | 97, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) ∈ ℝ) |
99 | 98, 89 | readdcld 10862 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
((⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) + 1) ∈
ℝ) |
100 | 1, 99 | eqeltrid 2842 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 ∈ ℝ) |
101 | 81 | abscld 15000 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) ∈ ℝ) |
102 | 81, 60 | iblabs 24726 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (abs‘(𝐹 · -𝐺))) ∈
𝐿1) |
103 | 101, 102 | itgrecl 24695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ∈ ℝ) |
104 | 81, 60 | itgabs 24732 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ≤ ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥) |
105 | 15 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (𝑥 ∈ 𝐼 ↦ (abs‘𝐹)) ∈
𝐿1) |
106 | 61 | abscld 15000 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℝ) |
107 | 61, 80 | absmuld 15018 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) = ((abs‘𝐹) · (abs‘-𝐺))) |
108 | 80 | abscld 15000 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘-𝐺) ∈ ℝ) |
109 | | 1red 10834 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 1 ∈ ℝ) |
110 | 61 | absge0d 15008 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → 0 ≤ (abs‘𝐹)) |
111 | | recn 10819 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℂ) |
112 | 111, 66 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → 𝐺 ∈ ℂ) |
113 | 112 | absnegd 15013 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘-𝐺) = (abs‘𝐺)) |
114 | | fourierdlem47.absg |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘𝐺) ≤ 1) |
115 | 113, 114 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘-𝐺) ≤ 1) |
116 | 62, 63, 64, 115 | syl21anc 838 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘-𝐺) ≤ 1) |
117 | 108, 109,
106, 110, 116 | lemul2ad 11772 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · (abs‘-𝐺)) ≤ ((abs‘𝐹) · 1)) |
118 | 106 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘𝐹) ∈ ℂ) |
119 | 118 | mulid1d 10850 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · 1) = (abs‘𝐹)) |
120 | 117, 119 | breqtrd 5079 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → ((abs‘𝐹) · (abs‘-𝐺)) ≤ (abs‘𝐹)) |
121 | 107, 120 | eqbrtrd 5075 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) ∧ 𝑥 ∈ 𝐼) → (abs‘(𝐹 · -𝐺)) ≤ (abs‘𝐹)) |
122 | 102, 105,
101, 106, 121 | itgle 24707 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ≤ ∫𝐼(abs‘𝐹) d𝑥) |
123 | 122, 11 | breqtrrdi 5095 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ∫𝐼(abs‘(𝐹 · -𝐺)) d𝑥 ≤ 𝑍) |
124 | 83, 103, 94, 104, 123 | letrd 10989 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘∫𝐼(𝐹 · -𝐺) d𝑥) ≤ 𝑍) |
125 | 83, 94, 93, 124 | leadd2dd 11447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) ≤ ((𝑋 + 𝑌) + 𝑍)) |
126 | 85, 95, 71, 125 | lediv1dd 12686 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) ≤ (((𝑋 + 𝑌) + 𝑍) / 𝐸)) |
127 | | flltp1 13375 |
. . . . . . . . . . 11
⊢ ((((𝑋 + 𝑌) + 𝑍) / 𝐸) ∈ ℝ → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
128 | 96, 127 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
129 | 96, 45, 46 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) →
(⌊‘((((𝑋 +
𝑌) + 𝑍) / 𝐸) + 1)) = ((⌊‘(((𝑋 + 𝑌) + 𝑍) / 𝐸)) + 1)) |
130 | 128, 129 | breqtrrd 5081 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + 𝑍) / 𝐸) < (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
131 | 88, 96, 98, 126, 130 | lelttrd 10990 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) < (⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1))) |
132 | 88, 98, 89, 131 | ltadd1dd 11443 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1)) |
133 | 132, 1 | breqtrrdi 5095 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < 𝑀) |
134 | 100 | rexrd 10883 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 ∈
ℝ*) |
135 | | pnfxr 10887 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
136 | 135 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → +∞ ∈
ℝ*) |
137 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ (𝑀(,)+∞)) |
138 | | ioogtlb 42708 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 < 𝑟) |
139 | 134, 136,
137, 138 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑀 < 𝑟) |
140 | 90, 100, 72, 133, 139 | lttrd 10993 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) < 𝑟) |
141 | 90, 72, 140 | ltled 10980 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → ((((𝑋 + 𝑌) + (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)) / 𝐸) + 1) ≤ 𝑟) |
142 | 72 | recnd 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝑟 ∈ ℂ) |
143 | | fourierdlem47.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐵 ∈ ℂ) |
144 | 142, 143 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐵 ∈ ℂ) |
145 | | fourierdlem47.absb |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐵) ≤ 1) |
146 | 58, 145 | sylan2 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐵) ≤ 1) |
147 | | fourierdlem47.d |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐷 ∈ ℂ) |
148 | 142, 147 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → 𝐷 ∈ ℂ) |
149 | | fourierdlem47.absd |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐷) ≤ 1) |
150 | 58, 149 | sylan2 596 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘𝐷) ≤ 1) |
151 | 60, 61, 67, 68, 2, 69, 6, 70, 71, 72, 141, 144, 146, 148, 150 | fourierdlem30 43353 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑀(,)+∞)) → (abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
152 | 151 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
153 | | oveq1 7220 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑚(,)+∞) = (𝑀(,)+∞)) |
154 | 153 | raleqdv 3325 |
. . 3
⊢ (𝑚 = 𝑀 → (∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸 ↔ ∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸)) |
155 | 154 | rspcev 3537 |
. 2
⊢ ((𝑀 ∈ ℕ ∧
∀𝑟 ∈ (𝑀(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |
156 | 57, 152, 155 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸) |