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 leadd12dd ( 𝜑 → ( ( ( 𝐻𝑈 ) · 𝑉 ) + ( 𝑈 · ( 𝐼𝑉 ) ) ) ≤ ( ( 𝑌 · ( 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 mulid1d ( 𝜑 → ( 𝑌 · 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 ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 )