Metamath Proof Explorer


Theorem fourierdlem30

Description: Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem30.ibl ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝐹 · - 𝐺 ) ) ∈ 𝐿1 )
fourierlemreimleblemlte22.f ( ( 𝜑𝑥𝐼 ) → 𝐹 ∈ ℂ )
fourierdlem30.g ( ( 𝜑𝑥𝐼 ) → 𝐺 ∈ ℂ )
fourierdlem30.a ( 𝜑𝐴 ∈ ℂ )
fourierdlem30.x 𝑋 = ( abs ‘ 𝐴 )
fourierdlem30.c ( 𝜑𝐶 ∈ ℂ )
fourierdlem30.y 𝑌 = ( abs ‘ 𝐶 )
fourierdlem30.z 𝑍 = ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 )
fourierdlem30.e ( 𝜑𝐸 ∈ ℝ+ )
fourierdlem30.r ( 𝜑𝑅 ∈ ℝ )
fourierdlem30.ler ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ≤ 𝑅 )
fourierdlem30.b ( 𝜑𝐵 ∈ ℂ )
fourierdlem30.12 ( 𝜑 → ( abs ‘ 𝐵 ) ≤ 1 )
fourierdlem30.d ( 𝜑𝐷 ∈ ℂ )
fourierdlem30.14 ( 𝜑 → ( abs ‘ 𝐷 ) ≤ 1 )
Assertion fourierdlem30 ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 fourierdlem30.ibl ( 𝜑 → ( 𝑥𝐼 ↦ ( 𝐹 · - 𝐺 ) ) ∈ 𝐿1 )
2 fourierlemreimleblemlte22.f ( ( 𝜑𝑥𝐼 ) → 𝐹 ∈ ℂ )
3 fourierdlem30.g ( ( 𝜑𝑥𝐼 ) → 𝐺 ∈ ℂ )
4 fourierdlem30.a ( 𝜑𝐴 ∈ ℂ )
5 fourierdlem30.x 𝑋 = ( abs ‘ 𝐴 )
6 fourierdlem30.c ( 𝜑𝐶 ∈ ℂ )
7 fourierdlem30.y 𝑌 = ( abs ‘ 𝐶 )
8 fourierdlem30.z 𝑍 = ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 )
9 fourierdlem30.e ( 𝜑𝐸 ∈ ℝ+ )
10 fourierdlem30.r ( 𝜑𝑅 ∈ ℝ )
11 fourierdlem30.ler ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ≤ 𝑅 )
12 fourierdlem30.b ( 𝜑𝐵 ∈ ℂ )
13 fourierdlem30.12 ( 𝜑 → ( abs ‘ 𝐵 ) ≤ 1 )
14 fourierdlem30.d ( 𝜑𝐷 ∈ ℂ )
15 fourierdlem30.14 ( 𝜑 → ( abs ‘ 𝐷 ) ≤ 1 )
16 10 recnd ( 𝜑𝑅 ∈ ℂ )
17 0red ( 𝜑 → 0 ∈ ℝ )
18 1red ( 𝜑 → 1 ∈ ℝ )
19 0lt1 0 < 1
20 19 a1i ( 𝜑 → 0 < 1 )
21 4 abscld ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
22 5 21 eqeltrid ( 𝜑𝑋 ∈ ℝ )
23 6 abscld ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
24 7 23 eqeltrid ( 𝜑𝑌 ∈ ℝ )
25 22 24 readdcld ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ℝ )
26 3 negcld ( ( 𝜑𝑥𝐼 ) → - 𝐺 ∈ ℂ )
27 2 26 mulcld ( ( 𝜑𝑥𝐼 ) → ( 𝐹 · - 𝐺 ) ∈ ℂ )
28 27 1 itgcl ( 𝜑 → ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ∈ ℂ )
29 28 abscld ( 𝜑 → ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ∈ ℝ )
30 8 29 eqeltrid ( 𝜑𝑍 ∈ ℝ )
31 25 30 readdcld ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ )
32 9 rpred ( 𝜑𝐸 ∈ ℝ )
33 9 rpne0d ( 𝜑𝐸 ≠ 0 )
34 31 32 33 redivcld ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ )
35 34 18 readdcld ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ )
36 4 absge0d ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
37 36 5 breqtrrdi ( 𝜑 → 0 ≤ 𝑋 )
38 6 absge0d ( 𝜑 → 0 ≤ ( abs ‘ 𝐶 ) )
39 38 7 breqtrrdi ( 𝜑 → 0 ≤ 𝑌 )
40 22 24 37 39 addge0d ( 𝜑 → 0 ≤ ( 𝑋 + 𝑌 ) )
41 28 absge0d ( 𝜑 → 0 ≤ ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) )
42 41 8 breqtrrdi ( 𝜑 → 0 ≤ 𝑍 )
43 25 30 40 42 addge0d ( 𝜑 → 0 ≤ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
44 31 9 43 divge0d ( 𝜑 → 0 ≤ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) )
45 18 34 addge02d ( 𝜑 → ( 0 ≤ ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ↔ 1 ≤ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
46 44 45 mpbid ( 𝜑 → 1 ≤ ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) )
47 18 35 10 46 11 letrd ( 𝜑 → 1 ≤ 𝑅 )
48 17 18 10 20 47 ltletrd ( 𝜑 → 0 < 𝑅 )
49 48 gt0ne0d ( 𝜑𝑅 ≠ 0 )
50 12 16 49 divnegd ( 𝜑 → - ( 𝐵 / 𝑅 ) = ( - 𝐵 / 𝑅 ) )
51 50 oveq2d ( 𝜑 → ( 𝐴 · - ( 𝐵 / 𝑅 ) ) = ( 𝐴 · ( - 𝐵 / 𝑅 ) ) )
52 12 negcld ( 𝜑 → - 𝐵 ∈ ℂ )
53 4 52 16 49 divassd ( 𝜑 → ( ( 𝐴 · - 𝐵 ) / 𝑅 ) = ( 𝐴 · ( - 𝐵 / 𝑅 ) ) )
54 51 53 eqtr4d ( 𝜑 → ( 𝐴 · - ( 𝐵 / 𝑅 ) ) = ( ( 𝐴 · - 𝐵 ) / 𝑅 ) )
55 14 16 49 divnegd ( 𝜑 → - ( 𝐷 / 𝑅 ) = ( - 𝐷 / 𝑅 ) )
56 55 oveq2d ( 𝜑 → ( 𝐶 · - ( 𝐷 / 𝑅 ) ) = ( 𝐶 · ( - 𝐷 / 𝑅 ) ) )
57 14 negcld ( 𝜑 → - 𝐷 ∈ ℂ )
58 6 57 16 49 divassd ( 𝜑 → ( ( 𝐶 · - 𝐷 ) / 𝑅 ) = ( 𝐶 · ( - 𝐷 / 𝑅 ) ) )
59 56 58 eqtr4d ( 𝜑 → ( 𝐶 · - ( 𝐷 / 𝑅 ) ) = ( ( 𝐶 · - 𝐷 ) / 𝑅 ) )
60 54 59 oveq12d ( 𝜑 → ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) = ( ( ( 𝐴 · - 𝐵 ) / 𝑅 ) − ( ( 𝐶 · - 𝐷 ) / 𝑅 ) ) )
61 4 52 mulcld ( 𝜑 → ( 𝐴 · - 𝐵 ) ∈ ℂ )
62 6 57 mulcld ( 𝜑 → ( 𝐶 · - 𝐷 ) ∈ ℂ )
63 61 62 16 49 divsubdird ( 𝜑 → ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) / 𝑅 ) = ( ( ( 𝐴 · - 𝐵 ) / 𝑅 ) − ( ( 𝐶 · - 𝐷 ) / 𝑅 ) ) )
64 60 63 eqtr4d ( 𝜑 → ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) = ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) / 𝑅 ) )
65 16 49 reccld ( 𝜑 → ( 1 / 𝑅 ) ∈ ℂ )
66 65 27 1 itgmulc2 ( 𝜑 → ( ( 1 / 𝑅 ) · ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) = ∫ 𝐼 ( ( 1 / 𝑅 ) · ( 𝐹 · - 𝐺 ) ) d 𝑥 )
67 28 16 49 divrec2d ( 𝜑 → ( ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 / 𝑅 ) = ( ( 1 / 𝑅 ) · ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) )
68 16 adantr ( ( 𝜑𝑥𝐼 ) → 𝑅 ∈ ℂ )
69 49 adantr ( ( 𝜑𝑥𝐼 ) → 𝑅 ≠ 0 )
70 3 68 69 divnegd ( ( 𝜑𝑥𝐼 ) → - ( 𝐺 / 𝑅 ) = ( - 𝐺 / 𝑅 ) )
71 70 oveq2d ( ( 𝜑𝑥𝐼 ) → ( 𝐹 · - ( 𝐺 / 𝑅 ) ) = ( 𝐹 · ( - 𝐺 / 𝑅 ) ) )
72 2 26 68 69 divassd ( ( 𝜑𝑥𝐼 ) → ( ( 𝐹 · - 𝐺 ) / 𝑅 ) = ( 𝐹 · ( - 𝐺 / 𝑅 ) ) )
73 27 68 69 divrec2d ( ( 𝜑𝑥𝐼 ) → ( ( 𝐹 · - 𝐺 ) / 𝑅 ) = ( ( 1 / 𝑅 ) · ( 𝐹 · - 𝐺 ) ) )
74 71 72 73 3eqtr2d ( ( 𝜑𝑥𝐼 ) → ( 𝐹 · - ( 𝐺 / 𝑅 ) ) = ( ( 1 / 𝑅 ) · ( 𝐹 · - 𝐺 ) ) )
75 74 itgeq2dv ( 𝜑 → ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 = ∫ 𝐼 ( ( 1 / 𝑅 ) · ( 𝐹 · - 𝐺 ) ) d 𝑥 )
76 66 67 75 3eqtr4rd ( 𝜑 → ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 = ( ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 / 𝑅 ) )
77 64 76 oveq12d ( 𝜑 → ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) = ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) / 𝑅 ) − ( ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 / 𝑅 ) ) )
78 61 62 subcld ( 𝜑 → ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ∈ ℂ )
79 78 28 16 49 divsubdird ( 𝜑 → ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) / 𝑅 ) = ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) / 𝑅 ) − ( ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 / 𝑅 ) ) )
80 77 79 eqtr4d ( 𝜑 → ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) = ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) / 𝑅 ) )
81 80 fveq2d ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) ) = ( abs ‘ ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) / 𝑅 ) ) )
82 78 28 subcld ( 𝜑 → ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ∈ ℂ )
83 82 16 49 absdivd ( 𝜑 → ( abs ‘ ( ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) / 𝑅 ) ) = ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( abs ‘ 𝑅 ) ) )
84 17 10 48 ltled ( 𝜑 → 0 ≤ 𝑅 )
85 10 84 absidd ( 𝜑 → ( abs ‘ 𝑅 ) = 𝑅 )
86 85 oveq2d ( 𝜑 → ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( abs ‘ 𝑅 ) ) = ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) )
87 81 83 86 3eqtrd ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) ) = ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) )
88 82 abscld ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ∈ ℝ )
89 88 10 49 redivcld ( 𝜑 → ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) ∈ ℝ )
90 21 23 readdcld ( 𝜑 → ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) ∈ ℝ )
91 90 29 readdcld ( 𝜑 → ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ∈ ℝ )
92 91 10 49 redivcld ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) ∈ ℝ )
93 10 48 elrpd ( 𝜑𝑅 ∈ ℝ+ )
94 78 abscld ( 𝜑 → ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) ∈ ℝ )
95 94 29 readdcld ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ∈ ℝ )
96 78 28 abs2dif2d ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ≤ ( ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) )
97 61 abscld ( 𝜑 → ( abs ‘ ( 𝐴 · - 𝐵 ) ) ∈ ℝ )
98 62 abscld ( 𝜑 → ( abs ‘ ( 𝐶 · - 𝐷 ) ) ∈ ℝ )
99 97 98 readdcld ( 𝜑 → ( ( abs ‘ ( 𝐴 · - 𝐵 ) ) + ( abs ‘ ( 𝐶 · - 𝐷 ) ) ) ∈ ℝ )
100 61 62 abs2dif2d ( 𝜑 → ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) ≤ ( ( abs ‘ ( 𝐴 · - 𝐵 ) ) + ( abs ‘ ( 𝐶 · - 𝐷 ) ) ) )
101 4 52 absmuld ( 𝜑 → ( abs ‘ ( 𝐴 · - 𝐵 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ - 𝐵 ) ) )
102 52 abscld ( 𝜑 → ( abs ‘ - 𝐵 ) ∈ ℝ )
103 12 absnegd ( 𝜑 → ( abs ‘ - 𝐵 ) = ( abs ‘ 𝐵 ) )
104 103 13 eqbrtrd ( 𝜑 → ( abs ‘ - 𝐵 ) ≤ 1 )
105 102 18 21 36 104 lemul2ad ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( abs ‘ - 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) · 1 ) )
106 21 recnd ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℂ )
107 106 mulid1d ( 𝜑 → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
108 105 107 breqtrd ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( abs ‘ - 𝐵 ) ) ≤ ( abs ‘ 𝐴 ) )
109 101 108 eqbrtrd ( 𝜑 → ( abs ‘ ( 𝐴 · - 𝐵 ) ) ≤ ( abs ‘ 𝐴 ) )
110 6 57 absmuld ( 𝜑 → ( abs ‘ ( 𝐶 · - 𝐷 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ - 𝐷 ) ) )
111 57 abscld ( 𝜑 → ( abs ‘ - 𝐷 ) ∈ ℝ )
112 14 absnegd ( 𝜑 → ( abs ‘ - 𝐷 ) = ( abs ‘ 𝐷 ) )
113 112 15 eqbrtrd ( 𝜑 → ( abs ‘ - 𝐷 ) ≤ 1 )
114 111 18 23 38 113 lemul2ad ( 𝜑 → ( ( abs ‘ 𝐶 ) · ( abs ‘ - 𝐷 ) ) ≤ ( ( abs ‘ 𝐶 ) · 1 ) )
115 23 recnd ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
116 115 mulid1d ( 𝜑 → ( ( abs ‘ 𝐶 ) · 1 ) = ( abs ‘ 𝐶 ) )
117 114 116 breqtrd ( 𝜑 → ( ( abs ‘ 𝐶 ) · ( abs ‘ - 𝐷 ) ) ≤ ( abs ‘ 𝐶 ) )
118 110 117 eqbrtrd ( 𝜑 → ( abs ‘ ( 𝐶 · - 𝐷 ) ) ≤ ( abs ‘ 𝐶 ) )
119 97 98 21 23 109 118 le2addd ( 𝜑 → ( ( abs ‘ ( 𝐴 · - 𝐵 ) ) + ( abs ‘ ( 𝐶 · - 𝐷 ) ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) )
120 94 99 90 100 119 letrd ( 𝜑 → ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) )
121 94 90 29 120 leadd1dd ( 𝜑 → ( ( abs ‘ ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ≤ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) )
122 88 95 91 96 121 letrd ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) ≤ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) )
123 88 91 93 122 lediv1dd ( 𝜑 → ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) ≤ ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) )
124 34 ltp1d ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) < ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) )
125 17 34 35 44 124 lelttrd ( 𝜑 → 0 < ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) )
126 125 gt0ne0d ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ≠ 0 )
127 91 35 126 redivcld ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) ∈ ℝ )
128 34 44 ge0p1rpd ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ+ )
129 5 eqcomi ( abs ‘ 𝐴 ) = 𝑋
130 7 eqcomi ( abs ‘ 𝐶 ) = 𝑌
131 129 130 oveq12i ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) = ( 𝑋 + 𝑌 )
132 8 eqcomi ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) = 𝑍
133 131 132 oveq12i ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 )
134 43 133 breqtrrdi ( 𝜑 → 0 ≤ ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) )
135 128 93 91 134 11 lediv2ad ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) ≤ ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
136 133 oveq1i ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) )
137 oveq1 ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( 0 / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
138 137 adantl ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = ( 0 / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) )
139 34 recnd ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℂ )
140 18 recnd ( 𝜑 → 1 ∈ ℂ )
141 139 140 addcld ( 𝜑 → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℂ )
142 141 adantr ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℂ )
143 oveq1 ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) = ( 0 / 𝐸 ) )
144 143 adantl ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) = ( 0 / 𝐸 ) )
145 9 rpcnd ( 𝜑𝐸 ∈ ℂ )
146 145 adantr ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 𝐸 ∈ ℂ )
147 33 adantr ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 𝐸 ≠ 0 )
148 146 147 div0d ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( 0 / 𝐸 ) = 0 )
149 144 148 eqtrd ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) = 0 )
150 149 oveq1d ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) = ( 0 + 1 ) )
151 0p1e1 ( 0 + 1 ) = 1
152 150 151 eqtrdi ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) = 1 )
153 ax-1ne0 1 ≠ 0
154 153 a1i ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 1 ≠ 0 )
155 152 154 eqnetrd ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ≠ 0 )
156 142 155 div0d ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( 0 / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = 0 )
157 138 156 eqtrd ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) = 0 )
158 9 rpgt0d ( 𝜑 → 0 < 𝐸 )
159 158 adantr ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 0 < 𝐸 )
160 157 159 eqbrtrd ( ( 𝜑 ∧ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) < 𝐸 )
161 31 adantr ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ )
162 9 adantr ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 𝐸 ∈ ℝ+ )
163 43 adantr ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 0 ≤ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
164 neqne ( ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ≠ 0 )
165 164 adantl ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ≠ 0 )
166 161 163 165 ne0gt0d ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 0 < ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
167 161 166 elrpd ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ+ )
168 167 162 rpdivcld ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) ∈ ℝ+ )
169 1rp 1 ∈ ℝ+
170 169 a1i ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → 1 ∈ ℝ+ )
171 168 170 rpaddcld ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ∈ ℝ+ )
172 124 adantr ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) < ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) )
173 161 162 171 172 ltdiv23d ( ( 𝜑 ∧ ¬ ( ( 𝑋 + 𝑌 ) + 𝑍 ) = 0 ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) < 𝐸 )
174 160 173 pm2.61dan ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) < 𝐸 )
175 136 174 eqbrtrid ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / ( ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 𝐸 ) + 1 ) ) < 𝐸 )
176 92 127 32 135 175 lelttrd ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐶 ) ) + ( abs ‘ ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) < 𝐸 )
177 89 92 32 123 176 lelttrd ( 𝜑 → ( ( abs ‘ ( ( ( 𝐴 · - 𝐵 ) − ( 𝐶 · - 𝐷 ) ) − ∫ 𝐼 ( 𝐹 · - 𝐺 ) d 𝑥 ) ) / 𝑅 ) < 𝐸 )
178 87 177 eqbrtrd ( 𝜑 → ( abs ‘ ( ( ( 𝐴 · - ( 𝐵 / 𝑅 ) ) − ( 𝐶 · - ( 𝐷 / 𝑅 ) ) ) − ∫ 𝐼 ( 𝐹 · - ( 𝐺 / 𝑅 ) ) d 𝑥 ) ) < 𝐸 )