Metamath Proof Explorer

Theorem fourierdlem47

Description: For r large enough, the final expression is less than the given positive E . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem47.ibl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐹 ) ∈ 𝐿1 )
fourierdlem47.iblmul ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 · - 𝐺 ) ) ∈ 𝐿1 )
fourierdlem47.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ ℂ )
fourierdlem47.g ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℂ ) → 𝐺 ∈ ℂ )
fourierdlem47.absg ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐺 ) ≤ 1 )
fourierdlem47.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
fourierdlem47.x ⊢ 𝑋 = ( abs ‘ 𝐴 )
fourierdlem47.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
fourierdlem47.y ⊢ 𝑌 = ( abs ‘ 𝐶 )
fourierdlem47.z ⊢ 𝑍 = ∫ 𝐼 ( abs ‘ 𝐹 ) d 𝑥
fourierdlem47.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
fourierdlem47.b ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → 𝐵 ∈ ℂ )
fourierdlem47.absb ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐵 ) ≤ 1 )
fourierdlem47.d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → 𝐷 ∈ ℂ )
fourierdlem47.absd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐷 ) ≤ 1 )
fourierdlem47.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) + 1 )
Assertion fourierdlem47 ( 𝜑 → ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 fourierdlem47.ibl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐹 ) ∈ 𝐿1 )
2 fourierdlem47.iblmul ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 · - 𝐺 ) ) ∈ 𝐿1 )
3 fourierdlem47.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ ℂ )
4 fourierdlem47.g ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℂ ) → 𝐺 ∈ ℂ )
5 fourierdlem47.absg ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐺 ) ≤ 1 )
6 fourierdlem47.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 fourierdlem47.x ⊢ 𝑋 = ( abs ‘ 𝐴 )
8 fourierdlem47.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
9 fourierdlem47.y ⊢ 𝑌 = ( abs ‘ 𝐶 )
10 fourierdlem47.z ⊢ 𝑍 = ∫ 𝐼 ( abs ‘ 𝐹 ) d 𝑥
11 fourierdlem47.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
12 fourierdlem47.b ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → 𝐵 ∈ ℂ )
13 fourierdlem47.absb ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐵 ) ≤ 1 )
14 fourierdlem47.d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) → 𝐷 ∈ ℂ )
15 fourierdlem47.absd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( abs ‘ 𝐷 ) ≤ 1 )
16 fourierdlem47.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) + 1 )
17 6 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
18 7 17 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
19 8 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
20 9 19 eqeltrid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
21 18 20 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ℝ )
22 3 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ 𝐹 ) ∈ ℝ )
23 3 1 iblabs ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( abs ‘ 𝐹 ) ) ∈ 𝐿1 )
24 22 23 itgrecl ⊢ ( 𝜑 → ∫ 𝐼 ( abs ‘ 𝐹 ) d 𝑥 ∈ ℝ )
25 10 24 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
26 21 25 readdcld ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ )
27 11 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
28 11 rpne0d ⊢ ( 𝜑 → 𝐸 ≠ 0 )
29 26 27 28 redivcld ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ )
30 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
31 29 30 readdcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ )
32 31 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℤ )
33 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
34 reflcl ⊢ ( ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℝ )
35 31 34 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℝ )
36 0lt1 ⊢ 0 < 1
37 36 a1i ⊢ ( 𝜑 → 0 < 1 )
38 6 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
39 38 7 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑋 )
40 8 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐶 ) )
41 40 9 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑌 )
42 18 20 39 41 addge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑋 + 𝑌 ) )
43 3 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( abs ‘ 𝐹 ) )
44 23 22 43 itgge0 ⊢ ( 𝜑 → 0 ≤ ∫ 𝐼 ( abs ‘ 𝐹 ) d 𝑥 )
45 44 10 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑍 )
46 21 25 42 45 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
47 26 11 46 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) )
48 flge0nn0 ⊢ ( ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) → ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ∈ ℕ0 )
49 29 47 48 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ∈ ℕ0 )
50 nn0addge1 ⊢ ( ( 1 ∈ ℝ ∧ ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ∈ ℕ0 ) → 1 ≤ ( 1 + ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ) )
51 30 49 50 syl2anc ⊢ ( 𝜑 → 1 ≤ ( 1 + ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ) )
52 1z ⊢ 1 ∈ ℤ
53 fladdz ⊢ ( ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) )
54 29 52 53 sylancl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) )
55 49 nn0cnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ∈ ℂ )
56 30 recnd ⊢ ( 𝜑 → 1 ∈ ℂ )
57 55 56 addcomd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) = ( 1 + ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ) )
58 54 57 eqtr2d ⊢ ( 𝜑 → ( 1 + ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) ) = ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
59 51 58 breqtrd ⊢ ( 𝜑 → 1 ≤ ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
60 33 30 35 37 59 ltletrd ⊢ ( 𝜑 → 0 < ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
61 elnnz ⊢ ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℕ ↔ ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℤ ∧ 0 < ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ) )
62 32 60 61 sylanbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℕ )
63 62 peano2nnd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) + 1 ) ∈ ℕ )
64 16 63 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
65 elioore ⊢ ( 𝑟 ∈ ( 𝑀 (,) +∞ ) → 𝑟 ∈ ℝ )
66 65 2 sylan2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 · - 𝐺 ) ) ∈ 𝐿1 )
67 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ ℂ )
68 simpll ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝜑 )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
70 65 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑟 ∈ ℝ )
71 70 recnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑟 ∈ ℂ )
72 68 69 71 4 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ ℂ )
73 6 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐴 ∈ ℂ )
74 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐶 ∈ ℂ )
75 eqid ⊢ ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) = ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 )
76 11 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐸 ∈ ℝ+ )
77 65 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑟 ∈ ℝ )
78 7 eqcomi ⊢ ( abs ‘ 𝐴 ) = 𝑋
79 9 eqcomi ⊢ ( abs ‘ 𝐶 ) = 𝑌
80 78 79 oveq12i ⊢ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) = ( 𝑋 + 𝑌 )
81 80 oveq1i ⊢ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) = ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) )
82 17 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
83 19 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ 𝐶 ) ∈ ℝ )
84 82 83 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) ∈ ℝ )
85 72 negcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → - 𝐺 ∈ ℂ )
86 67 85 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 · - 𝐺 ) ∈ ℂ )
87 86 66 itgcl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ∈ ℂ )
88 87 abscld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ∈ ℝ )
89 84 88 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ∈ ℝ )
90 81 89 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ∈ ℝ )
91 27 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐸 ∈ ℝ )
92 28 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐸 ≠ 0 )
93 90 91 92 redivcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) ∈ ℝ )
94 1red ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 1 ∈ ℝ )
95 93 94 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) + 1 ) ∈ ℝ )
96 7 82 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑋 ∈ ℝ )
97 9 83 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑌 ∈ ℝ )
98 96 97 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( 𝑋 + 𝑌 ) ∈ ℝ )
99 25 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑍 ∈ ℝ )
100 98 99 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ )
101 100 91 92 redivcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ )
102 101 94 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ )
103 102 34 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℝ )
104 103 94 readdcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) + 1 ) ∈ ℝ )
105 16 104 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑀 ∈ ℝ )
106 86 abscld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ ( 𝐹 · - 𝐺 ) ) ∈ ℝ )
107 86 66 iblabs ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( 𝑥 ∈ 𝐼 ↦ ( abs ‘ ( 𝐹 · - 𝐺 ) ) ) ∈ 𝐿1 )
108 106 107 itgrecl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ∫ 𝐼 ( abs ‘ ( 𝐹 · - 𝐺 ) ) d 𝑥 ∈ ℝ )
109 86 66 itgabs ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ≤ ∫ 𝐼 ( abs ‘ ( 𝐹 · - 𝐺 ) ) d 𝑥 )
110 23 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( 𝑥 ∈ 𝐼 ↦ ( abs ‘ 𝐹 ) ) ∈ 𝐿1 )
111 67 abscld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ 𝐹 ) ∈ ℝ )
112 67 85 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ ( 𝐹 · - 𝐺 ) ) = ( ( abs ‘ 𝐹 ) · ( abs ‘ - 𝐺 ) ) )
113 85 abscld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ - 𝐺 ) ∈ ℝ )
114 1red ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 1 ∈ ℝ )
115 67 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( abs ‘ 𝐹 ) )
116 recn ⊢ ( 𝑟 ∈ ℝ → 𝑟 ∈ ℂ )
117 116 4 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ ) → 𝐺 ∈ ℂ )
118 117 absnegd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ ) → ( abs ‘ - 𝐺 ) = ( abs ‘ 𝐺 ) )
119 118 5 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑟 ∈ ℝ ) → ( abs ‘ - 𝐺 ) ≤ 1 )
120 68 69 70 119 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ - 𝐺 ) ≤ 1 )
121 113 114 111 115 120 lemul2ad ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( abs ‘ 𝐹 ) · ( abs ‘ - 𝐺 ) ) ≤ ( ( abs ‘ 𝐹 ) · 1 ) )
122 111 recnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ 𝐹 ) ∈ ℂ )
123 122 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( abs ‘ 𝐹 ) · 1 ) = ( abs ‘ 𝐹 ) )
124 121 123 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( abs ‘ 𝐹 ) · ( abs ‘ - 𝐺 ) ) ≤ ( abs ‘ 𝐹 ) )
125 112 124 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( abs ‘ ( 𝐹 · - 𝐺 ) ) ≤ ( abs ‘ 𝐹 ) )
126 107 110 106 111 125 itgle ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ∫ 𝐼 ( abs ‘ ( 𝐹 · - 𝐺 ) ) d 𝑥 ≤ ∫ 𝐼 ( abs ‘ 𝐹 ) d 𝑥 )
127 126 10 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ∫ 𝐼 ( abs ‘ ( 𝐹 · - 𝐺 ) ) d 𝑥 ≤ 𝑍 )
128 88 108 99 109 127 letrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ≤ 𝑍 )
129 88 99 98 128 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ≤ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
130 90 100 76 129 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) ≤ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) )
131 flltp1 ⊢ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) < ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) )
132 101 131 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) < ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) )
133 101 52 53 sylancl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( ( ⌊ ‘ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ) + 1 ) )
134 132 133 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) < ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
135 93 101 103 130 134 lelttrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) < ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
136 93 103 94 135 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) + 1 ) < ( ( ⌊ ‘ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) + 1 ) )
137 136 16 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) + 1 ) < 𝑀 )
138 105 rexrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑀 ∈ ℝ* )
139 pnfxr ⊢ +∞ ∈ ℝ*
140 139 a1i ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → +∞ ∈ ℝ* )
141 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑟 ∈ ( 𝑀 (,) +∞ ) )
142 ioogtlb ⊢ ( ( 𝑀 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑀 < 𝑟 )
143 138 140 141 142 syl3anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑀 < 𝑟 )
144 95 105 77 137 143 lttrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) + 1 ) < 𝑟 )
145 95 77 144 ltled ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( ( ( ( 𝑋 + 𝑌 ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝐸 ) + 1 ) ≤ 𝑟 )
146 77 recnd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝑟 ∈ ℂ )
147 146 12 syldan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐵 ∈ ℂ )
148 65 13 sylan2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ 𝐵 ) ≤ 1 )
149 146 14 syldan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → 𝐷 ∈ ℂ )
150 65 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ 𝐷 ) ≤ 1 )
151 66 67 72 73 7 74 9 75 76 77 145 147 148 149 150 fourierdlem30 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( 𝑀 (,) +∞ ) ) → ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 )
152 151 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( 𝑀 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 )
153 oveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 (,) +∞ ) = ( 𝑀 (,) +∞ ) )
154 153 raleqdv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 ↔ ∀ 𝑟 ∈ ( 𝑀 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 ) )
155 154 rspcev ⊢ ( ( 𝑀 ∈ ℕ ∧ ∀ 𝑟 ∈ ( 𝑀 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 ) → ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 )
156 64 152 155 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∀ 𝑟 ∈ ( 𝑚 (,) +∞ ) ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑟 ) ) − ( 𝐶 · - ( 𝐷 / 𝑟 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑟 ) ) d 𝑥 ) ) < 𝐸 )