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 
|- ( ph -> A e. RR )
smfmullem1.u 
|- ( ph -> U e. RR )
smfmullem1.v 
|- ( ph -> V e. RR )
smfmullem1.l 
|- ( ph -> ( U x. V ) < A )
smfmullem1.x 
|- X = ( ( A - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
smfmullem1.y 
|- Y = if ( 1 <_ X , 1 , X )
smfmullem1.p 
|- ( ph -> P e. ( ( U - Y ) (,) U ) )
smfmullem1.r 
|- ( ph -> R e. ( U (,) ( U + Y ) ) )
smfmullem1.s 
|- ( ph -> S e. ( ( V - Y ) (,) V ) )
smfmullem1.z 
|- ( ph -> Z e. ( V (,) ( V + Y ) ) )
smfmullem1.h 
|- ( ph -> H e. ( P (,) R ) )
smfmullem1.i 
|- ( ph -> I e. ( S (,) Z ) )
Assertion smfmullem1 
|- ( ph -> ( H x. I ) < A )

Proof

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