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 mulridd ⊢ ( 𝜑 → ( ( 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 mulridd ⊢ ( 𝜑 → ( ( 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 𝑥 ) ) < 𝐸 )