Metamath Proof Explorer

Theorem smfmullem1

Description: The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfmullem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
smfmullem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
smfmullem1.v ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
smfmullem1.l ⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝐴 )
smfmullem1.x ⊢ 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
smfmullem1.y ⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
smfmullem1.p ⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
smfmullem1.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
smfmullem1.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
smfmullem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
smfmullem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 (,) 𝑅 ) )
smfmullem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝑆 (,) 𝑍 ) )
Assertion smfmullem1 ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 smfmullem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 smfmullem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
3 smfmullem1.v ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
4 smfmullem1.l ⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) < 𝐴 )
5 smfmullem1.x ⊢ 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
6 smfmullem1.y ⊢ 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 )
7 smfmullem1.p ⊢ ( 𝜑 → 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) )
8 smfmullem1.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) )
9 smfmullem1.s ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝑉 − 𝑌 ) (,) 𝑉 ) )
10 smfmullem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 (,) ( 𝑉 + 𝑌 ) ) )
11 smfmullem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 (,) 𝑅 ) )
12 smfmullem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 𝑆 (,) 𝑍 ) )
13 11 elioored ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
14 13 recnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
15 2 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
16 12 elioored ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
17 16 recnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
18 3 recnd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
19 14 15 17 18 mulsubd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) = ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) )
20 14 15 18 subdird ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) = ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) )
21 15 17 18 subdid ⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) = ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) )
22 20 21 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) )
23 14 18 mulcld ⊢ ( 𝜑 → ( 𝐻 · 𝑉 ) ∈ ℂ )
24 15 17 mulcld ⊢ ( 𝜑 → ( 𝑈 · 𝐼 ) ∈ ℂ )
25 15 18 mulcld ⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) ∈ ℂ )
26 23 24 25 25 addsub4d ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) )
27 26 eqcomd ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) − ( 𝑈 · 𝑉 ) ) + ( ( 𝑈 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
28 15 17 mulcomd ⊢ ( 𝜑 → ( 𝑈 · 𝐼 ) = ( 𝐼 · 𝑈 ) )
29 28 oveq2d ⊢ ( 𝜑 → ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) = ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) )
30 29 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝑉 ) + ( 𝑈 · 𝐼 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
31 22 27 30 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
32 19 31 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) )
33 14 17 mulcld ⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) ∈ ℂ )
34 18 15 mulcld ⊢ ( 𝜑 → ( 𝑉 · 𝑈 ) ∈ ℂ )
35 33 34 addcld ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) ∈ ℂ )
36 17 15 mulcld ⊢ ( 𝜑 → ( 𝐼 · 𝑈 ) ∈ ℂ )
37 23 36 addcld ⊢ ( 𝜑 → ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ∈ ℂ )
38 35 37 npcand ⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) )
39 18 15 mulcomd ⊢ ( 𝜑 → ( 𝑉 · 𝑈 ) = ( 𝑈 · 𝑉 ) )
40 39 oveq2d ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) )
41 38 40 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) = ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) )
42 41 eqcomd ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) )
43 42 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
44 35 37 subcld ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) ∈ ℂ )
45 25 25 addcld ⊢ ( 𝜑 → ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ∈ ℂ )
46 44 37 45 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) )
47 43 46 eqtr2d ⊢ ( 𝜑 → ( ( ( ( 𝐻 · 𝐼 ) + ( 𝑉 · 𝑈 ) ) − ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) ) + ( ( ( 𝐻 · 𝑉 ) + ( 𝐼 · 𝑈 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) ) = ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) )
48 33 25 25 pnpcan2d ⊢ ( 𝜑 → ( ( ( 𝐻 · 𝐼 ) + ( 𝑈 · 𝑉 ) ) − ( ( 𝑈 · 𝑉 ) + ( 𝑈 · 𝑉 ) ) ) = ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) )
49 32 47 48 3eqtrrd ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) = ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) )
50 13 2 jca ⊢ ( 𝜑 → ( 𝐻 ∈ ℝ ∧ 𝑈 ∈ ℝ ) )
51 resubcl ⊢ ( ( 𝐻 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐻 − 𝑈 ) ∈ ℝ )
52 50 51 syl ⊢ ( 𝜑 → ( 𝐻 − 𝑈 ) ∈ ℝ )
53 16 3 jca ⊢ ( 𝜑 → ( 𝐼 ∈ ℝ ∧ 𝑉 ∈ ℝ ) )
54 resubcl ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( 𝐼 − 𝑉 ) ∈ ℝ )
55 53 54 syl ⊢ ( 𝜑 → ( 𝐼 − 𝑉 ) ∈ ℝ )
56 52 55 jca ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) )
57 remulcl ⊢ ( ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
58 56 57 syl ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
59 52 3 jca ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ 𝑉 ∈ ℝ ) )
60 remulcl ⊢ ( ( ( 𝐻 − 𝑈 ) ∈ ℝ ∧ 𝑉 ∈ ℝ ) → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ )
61 59 60 syl ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ )
62 2 55 jca ⊢ ( 𝜑 → ( 𝑈 ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) )
63 remulcl ⊢ ( ( 𝑈 ∈ ℝ ∧ ( 𝐼 − 𝑉 ) ∈ ℝ ) → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
64 62 63 syl ⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ )
65 61 64 jca ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ ∧ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ ) )
66 readdcl ⊢ ( ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℝ ∧ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℝ ) → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
67 65 66 syl ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
68 58 67 jca ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ ∧ ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ ) )
69 readdcl ⊢ ( ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℝ ∧ ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ ) → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) ∈ ℝ )
70 68 69 syl ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) ∈ ℝ )
71 6 a1i ⊢ ( 𝜑 → 𝑌 = if ( 1 ≤ 𝑋 , 1 , 𝑋 ) )
72 1rp ⊢ 1 ∈ ℝ+
73 72 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
74 5 a1i ⊢ ( 𝜑 → 𝑋 = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
75 2 3 remulcld ⊢ ( 𝜑 → ( 𝑈 · 𝑉 ) ∈ ℝ )
76 difrp ⊢ ( ( ( 𝑈 · 𝑉 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑈 · 𝑉 ) < 𝐴 ↔ ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
77 75 1 76 syl2anc ⊢ ( 𝜑 → ( ( 𝑈 · 𝑉 ) < 𝐴 ↔ ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ ) )
78 4 77 mpbid ⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ+ )
79 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
80 15 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℝ )
81 18 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℝ )
82 80 81 readdcld ⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ∈ ℝ )
83 79 82 readdcld ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ )
84 0re ⊢ 0 ∈ ℝ
85 84 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
86 73 rpgt0d ⊢ ( 𝜑 → 0 < 1 )
87 15 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑈 ) )
88 18 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑉 ) )
89 80 81 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ 𝑉 ) ↔ ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
90 88 89 mpbid ⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
91 85 80 82 87 90 letrd ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) )
92 79 82 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ↔ 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) )
93 91 92 mpbid ⊢ ( 𝜑 → 1 ≤ ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
94 85 79 83 86 93 ltletrd ⊢ ( 𝜑 → 0 < ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) )
95 83 94 elrpd ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ∈ ℝ+ )
96 78 95 rpdivcld ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) ∈ ℝ+ )
97 74 96 eqeltrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
98 73 97 ifcld ⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ∈ ℝ+ )
99 71 98 eqeltrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
100 99 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
101 resqcl ⊢ ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℝ )
102 100 101 syl ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℝ )
103 100 81 remulcld ⊢ ( 𝜑 → ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ )
104 100 80 remulcld ⊢ ( 𝜑 → ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ )
105 103 104 jca ⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ ∧ ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ ) )
106 readdcl ⊢ ( ( ( 𝑌 · ( abs ‘ 𝑉 ) ) ∈ ℝ ∧ ( 𝑌 · ( abs ‘ 𝑈 ) ) ∈ ℝ ) → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
107 105 106 syl ⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
108 102 107 jca ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ ) )
109 readdcl ⊢ ( ( ( 𝑌 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ ) → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
110 108 109 syl ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
111 1 75 resubcld ⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℝ )
112 100 resqcld ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℝ )
113 103 104 readdcld ⊢ ( 𝜑 → ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
114 19 44 eqeltrd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ∈ ℂ )
115 114 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
116 100 100 remulcld ⊢ ( 𝜑 → ( 𝑌 · 𝑌 ) ∈ ℝ )
117 58 leabsd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ≤ ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) )
118 52 recnd ⊢ ( 𝜑 → ( 𝐻 − 𝑈 ) ∈ ℂ )
119 55 recnd ⊢ ( 𝜑 → ( 𝐼 − 𝑉 ) ∈ ℂ )
120 118 119 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) )
121 118 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) ∈ ℝ )
122 119 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ∈ ℝ )
123 118 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐻 − 𝑈 ) ) )
124 2 100 resubcld ⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ )
125 7 elioored ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
126 124 rexrd ⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) ∈ ℝ* )
127 2 rexrd ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
128 ioogtlb ⊢ ( ( ( 𝑈 − 𝑌 ) ∈ ℝ* ∧ 𝑈 ∈ ℝ* ∧ 𝑃 ∈ ( ( 𝑈 − 𝑌 ) (,) 𝑈 ) ) → ( 𝑈 − 𝑌 ) < 𝑃 )
129 126 127 7 128 syl3anc ⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) < 𝑃 )
130 125 rexrd ⊢ ( 𝜑 → 𝑃 ∈ ℝ* )
131 8 elioored ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
132 131 rexrd ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
133 ioogtlb ⊢ ( ( 𝑃 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐻 ∈ ( 𝑃 (,) 𝑅 ) ) → 𝑃 < 𝐻 )
134 130 132 11 133 syl3anc ⊢ ( 𝜑 → 𝑃 < 𝐻 )
135 124 125 13 129 134 lttrd ⊢ ( 𝜑 → ( 𝑈 − 𝑌 ) < 𝐻 )
136 2 100 readdcld ⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ )
137 iooltub ⊢ ( ( 𝑃 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ 𝐻 ∈ ( 𝑃 (,) 𝑅 ) ) → 𝐻 < 𝑅 )
138 130 132 11 137 syl3anc ⊢ ( 𝜑 → 𝐻 < 𝑅 )
139 136 rexrd ⊢ ( 𝜑 → ( 𝑈 + 𝑌 ) ∈ ℝ* )
140 iooltub ⊢ ( ( 𝑈 ∈ ℝ* ∧ ( 𝑈 + 𝑌 ) ∈ ℝ* ∧ 𝑅 ∈ ( 𝑈 (,) ( 𝑈 + 𝑌 ) ) ) → 𝑅 < ( 𝑈 + 𝑌 ) )
141 127 139 8 140 syl3anc ⊢ ( 𝜑 → 𝑅 < ( 𝑈 + 𝑌 ) )
142 13 131 136 138 141 lttrd ⊢ ( 𝜑 → 𝐻 < ( 𝑈 + 𝑌 ) )
143 135 142 jca ⊢ ( 𝜑 → ( ( 𝑈 − 𝑌 ) < 𝐻 ∧ 𝐻 < ( 𝑈 + 𝑌 ) ) )
144 13 2 100 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) < 𝑌 ↔ ( ( 𝑈 − 𝑌 ) < 𝐻 ∧ 𝐻 < ( 𝑈 + 𝑌 ) ) ) )
145 143 144 mpbird ⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) < 𝑌 )
146 119 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐼 − 𝑉 ) ) )
147 3 100 resubcld ⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ )
148 9 elioored ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
149 147 rexrd ⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) ∈ ℝ* )
150 3 rexrd ⊢ ( 𝜑 → 𝑉 ∈ ℝ* )
151 149 150 9 ioogtlbd ⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) < 𝑆 )
152 148 rexrd ⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
153 10 elioored ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
154 153 rexrd ⊢ ( 𝜑 → 𝑍 ∈ ℝ* )
155 152 154 12 ioogtlbd ⊢ ( 𝜑 → 𝑆 < 𝐼 )
156 147 148 16 151 155 lttrd ⊢ ( 𝜑 → ( 𝑉 − 𝑌 ) < 𝐼 )
157 3 100 readdcld ⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ )
158 152 154 12 iooltubd ⊢ ( 𝜑 → 𝐼 < 𝑍 )
159 157 rexrd ⊢ ( 𝜑 → ( 𝑉 + 𝑌 ) ∈ ℝ* )
160 150 159 10 iooltubd ⊢ ( 𝜑 → 𝑍 < ( 𝑉 + 𝑌 ) )
161 16 153 157 158 160 lttrd ⊢ ( 𝜑 → 𝐼 < ( 𝑉 + 𝑌 ) )
162 156 161 jca ⊢ ( 𝜑 → ( ( 𝑉 − 𝑌 ) < 𝐼 ∧ 𝐼 < ( 𝑉 + 𝑌 ) ) )
163 16 3 100 absdifltd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐼 − 𝑉 ) ) < 𝑌 ↔ ( ( 𝑉 − 𝑌 ) < 𝐼 ∧ 𝐼 < ( 𝑉 + 𝑌 ) ) ) )
164 162 163 mpbird ⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) < 𝑌 )
165 121 100 122 100 123 145 146 164 ltmul12ad ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) < ( 𝑌 · 𝑌 ) )
166 120 165 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) ) < ( 𝑌 · 𝑌 ) )
167 58 115 116 117 166 lelttrd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) < ( 𝑌 · 𝑌 ) )
168 100 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
169 168 sqvald ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) = ( 𝑌 · 𝑌 ) )
170 169 eqcomd ⊢ ( 𝜑 → ( 𝑌 · 𝑌 ) = ( 𝑌 ↑ 2 ) )
171 167 170 breqtrd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) < ( 𝑌 ↑ 2 ) )
172 61 recnd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ∈ ℂ )
173 172 abscld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) ∈ ℝ )
174 61 leabsd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ≤ ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) )
175 118 18 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) = ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ 𝑉 ) ) )
176 121 100 145 ltled ⊢ ( 𝜑 → ( abs ‘ ( 𝐻 − 𝑈 ) ) ≤ 𝑌 )
177 121 100 81 88 176 lemul1ad ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐻 − 𝑈 ) ) · ( abs ‘ 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
178 175 177 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐻 − 𝑈 ) · 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
179 61 173 103 174 178 letrd ⊢ ( 𝜑 → ( ( 𝐻 − 𝑈 ) · 𝑉 ) ≤ ( 𝑌 · ( abs ‘ 𝑉 ) ) )
180 64 recnd ⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ∈ ℂ )
181 180 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ∈ ℝ )
182 64 leabsd ⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ≤ ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) )
183 15 119 absmuld ⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ 𝑈 ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) )
184 80 recnd ⊢ ( 𝜑 → ( abs ‘ 𝑈 ) ∈ ℂ )
185 122 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ∈ ℂ )
186 184 185 mulcomd ⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) · ( abs ‘ ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
187 183 186 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) = ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) )
188 122 100 164 ltled ⊢ ( 𝜑 → ( abs ‘ ( 𝐼 − 𝑉 ) ) ≤ 𝑌 )
189 122 100 80 87 188 lemul1ad ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐼 − 𝑉 ) ) · ( abs ‘ 𝑈 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
190 187 189 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
191 64 181 104 182 190 letrd ⊢ ( 𝜑 → ( 𝑈 · ( 𝐼 − 𝑉 ) ) ≤ ( 𝑌 · ( abs ‘ 𝑈 ) ) )
192 61 64 103 104 179 191 le2addd ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ≤ ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) )
193 58 67 112 113 171 192 ltleaddd ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) < ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
194 100 107 readdcld ⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ∈ ℝ )
195 85 121 100 123 176 letrd ⊢ ( 𝜑 → 0 ≤ 𝑌 )
196 97 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
197 min1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 1 )
198 79 196 197 syl2anc ⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 1 )
199 6 198 eqbrtrid ⊢ ( 𝜑 → 𝑌 ≤ 1 )
200 85 79 100 195 199 eliccd ⊢ ( 𝜑 → 𝑌 ∈ ( 0 [,] 1 ) )
201 100 sqrlearg ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) ≤ 𝑌 ↔ 𝑌 ∈ ( 0 [,] 1 ) ) )
202 200 201 mpbird ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ≤ 𝑌 )
203 102 100 107 202 leadd1dd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
204 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
205 81 recnd ⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ∈ ℂ )
206 205 184 addcld ⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ∈ ℂ )
207 168 204 206 adddid ⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( 𝑌 · 1 ) + ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
208 168 mulridd ⊢ ( 𝜑 → ( 𝑌 · 1 ) = 𝑌 )
209 168 205 184 adddid ⊢ ( 𝜑 → ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) = ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) )
210 208 209 oveq12d ⊢ ( 𝜑 → ( ( 𝑌 · 1 ) + ( 𝑌 · ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) )
211 207 210 eqtr2d ⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) = ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
212 81 80 readdcld ⊢ ( 𝜑 → ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ∈ ℝ )
213 79 212 readdcld ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ∈ ℝ )
214 81 80 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( abs ‘ 𝑈 ) ↔ ( abs ‘ 𝑉 ) ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
215 87 214 mpbid ⊢ ( 𝜑 → ( abs ‘ 𝑉 ) ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
216 85 81 212 88 215 letrd ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
217 79 212 addge01d ⊢ ( 𝜑 → ( 0 ≤ ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ↔ 1 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
218 216 217 mpbid ⊢ ( 𝜑 → 1 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
219 85 79 213 86 218 ltletrd ⊢ ( 𝜑 → 0 < ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
220 85 213 219 ltled ⊢ ( 𝜑 → 0 ≤ ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
221 min2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 𝑋 )
222 79 196 221 syl2anc ⊢ ( 𝜑 → if ( 1 ≤ 𝑋 , 1 , 𝑋 ) ≤ 𝑋 )
223 71 222 eqbrtrd ⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
224 100 196 213 220 223 lemul1ad ⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
225 74 oveq1d ⊢ ( 𝜑 → ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
226 184 205 addcomd ⊢ ( 𝜑 → ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) = ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) )
227 226 oveq2d ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) = ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) )
228 227 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) = ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
229 228 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑈 ) + ( abs ‘ 𝑉 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) )
230 111 recnd ⊢ ( 𝜑 → ( 𝐴 − ( 𝑈 · 𝑉 ) ) ∈ ℂ )
231 204 206 addcld ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ∈ ℂ )
232 85 219 gtned ⊢ ( 𝜑 → ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ≠ 0 )
233 230 231 232 divcan1d ⊢ ( 𝜑 → ( ( ( 𝐴 − ( 𝑈 · 𝑉 ) ) / ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
234 225 229 233 3eqtrd ⊢ ( 𝜑 → ( 𝑋 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) = ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
235 224 234 breqtrd ⊢ ( 𝜑 → ( 𝑌 · ( 1 + ( ( abs ‘ 𝑉 ) + ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
236 211 235 eqbrtrd ⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
237 110 194 111 203 236 letrd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑌 · ( abs ‘ 𝑉 ) ) + ( 𝑌 · ( abs ‘ 𝑈 ) ) ) ) ≤ ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
238 70 110 111 193 237 ltletrd ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝑈 ) · ( 𝐼 − 𝑉 ) ) + ( ( ( 𝐻 − 𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼 − 𝑉 ) ) ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
239 49 238 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) )
240 13 16 remulcld ⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) ∈ ℝ )
241 240 1 75 ltsub1d ⊢ ( 𝜑 → ( ( 𝐻 · 𝐼 ) < 𝐴 ↔ ( ( 𝐻 · 𝐼 ) − ( 𝑈 · 𝑉 ) ) < ( 𝐴 − ( 𝑈 · 𝑉 ) ) ) )
242 239 241 mpbird ⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 )