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 |
⊢ ( 𝜑 → ( 𝐻 · 𝐼 ) < 𝐴 ) |