Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
|
simprr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( F ` A ) e. RR ) |
3 |
|
simprl |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) e. RR ) |
4 |
|
rexsub |
|- ( ( ( F ` A ) e. RR /\ ( A D B ) e. RR ) -> ( ( F ` A ) +e -e ( A D B ) ) = ( ( F ` A ) - ( A D B ) ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) +e -e ( A D B ) ) = ( ( F ` A ) - ( A D B ) ) ) |
6 |
5
|
oveq2d |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) ) |
7 |
|
simpll |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> D e. ( *Met ` X ) ) |
8 |
7
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> D e. ( *Met ` X ) ) |
9 |
|
simprr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> B e. X ) |
10 |
9
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> B e. X ) |
11 |
|
simprl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> A e. X ) |
12 |
11
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> A e. X ) |
13 |
2 3
|
resubcld |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) - ( A D B ) ) e. RR ) |
14 |
3
|
leidd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) <_ ( A D B ) ) |
15 |
|
xmetsym |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) ) |
16 |
7 11 9 15
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = ( B D A ) ) |
17 |
16
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) = ( B D A ) ) |
18 |
17
|
eqcomd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B D A ) = ( A D B ) ) |
19 |
2
|
recnd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( F ` A ) e. CC ) |
20 |
3
|
recnd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( A D B ) e. CC ) |
21 |
19 20
|
nncand |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) = ( A D B ) ) |
22 |
14 18 21
|
3brtr4d |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B D A ) <_ ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) ) |
23 |
|
blss2 |
|- ( ( ( D e. ( *Met ` X ) /\ B e. X /\ A e. X ) /\ ( ( ( F ` A ) - ( A D B ) ) e. RR /\ ( F ` A ) e. RR /\ ( B D A ) <_ ( ( F ` A ) - ( ( F ` A ) - ( A D B ) ) ) ) ) -> ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
24 |
8 10 12 13 2 22 23
|
syl33anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) - ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
25 |
6 24
|
eqsstrd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) e. RR ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
26 |
25
|
expr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) ) |
27 |
7
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> D e. ( *Met ` X ) ) |
28 |
9
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> B e. X ) |
29 |
1
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> F : X --> ( 0 [,] +oo ) ) |
30 |
29
|
adantr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> F : X --> ( 0 [,] +oo ) ) |
31 |
30 11
|
ffvelrnd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) e. ( 0 [,] +oo ) ) |
32 |
|
eliccxr |
|- ( ( F ` A ) e. ( 0 [,] +oo ) -> ( F ` A ) e. RR* ) |
33 |
31 32
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) e. RR* ) |
34 |
33
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( F ` A ) e. RR* ) |
35 |
|
xmetcl |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* ) |
36 |
7 11 9 35
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) e. RR* ) |
37 |
36
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( A D B ) e. RR* ) |
38 |
37
|
xnegcld |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> -e ( A D B ) e. RR* ) |
39 |
34 38
|
xaddcld |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) |
40 |
39
|
adantrr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) |
41 |
|
pnfxr |
|- +oo e. RR* |
42 |
41
|
a1i |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> +oo e. RR* ) |
43 |
|
pnfge |
|- ( ( ( F ` A ) +e -e ( A D B ) ) e. RR* -> ( ( F ` A ) +e -e ( A D B ) ) <_ +oo ) |
44 |
40 43
|
syl |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( ( F ` A ) +e -e ( A D B ) ) <_ +oo ) |
45 |
|
ssbl |
|- ( ( ( D e. ( *Met ` X ) /\ B e. X ) /\ ( ( ( F ` A ) +e -e ( A D B ) ) e. RR* /\ +oo e. RR* ) /\ ( ( F ` A ) +e -e ( A D B ) ) <_ +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( B ( ball ` D ) +oo ) ) |
46 |
27 28 40 42 44 45
|
syl221anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( B ( ball ` D ) +oo ) ) |
47 |
|
simprr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( F ` A ) = +oo ) |
48 |
47
|
oveq2d |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A ( ball ` D ) ( F ` A ) ) = ( A ( ball ` D ) +oo ) ) |
49 |
11
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> A e. X ) |
50 |
|
simprl |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A D B ) e. RR ) |
51 |
|
xblpnf |
|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( B e. ( A ( ball ` D ) +oo ) <-> ( B e. X /\ ( A D B ) e. RR ) ) ) |
52 |
27 49 51
|
syl2anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B e. ( A ( ball ` D ) +oo ) <-> ( B e. X /\ ( A D B ) e. RR ) ) ) |
53 |
28 50 52
|
mpbir2and |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> B e. ( A ( ball ` D ) +oo ) ) |
54 |
|
blpnfctr |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. ( A ( ball ` D ) +oo ) ) -> ( A ( ball ` D ) +oo ) = ( B ( ball ` D ) +oo ) ) |
55 |
27 49 53 54
|
syl3anc |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( A ( ball ` D ) +oo ) = ( B ( ball ` D ) +oo ) ) |
56 |
48 55
|
eqtr2d |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) +oo ) = ( A ( ball ` D ) ( F ` A ) ) ) |
57 |
46 56
|
sseqtrd |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( ( A D B ) e. RR /\ ( F ` A ) = +oo ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
58 |
57
|
expr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) = +oo -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) ) |
59 |
|
elxrge0 |
|- ( ( F ` A ) e. ( 0 [,] +oo ) <-> ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) ) |
60 |
59
|
simprbi |
|- ( ( F ` A ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` A ) ) |
61 |
31 60
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( F ` A ) ) |
62 |
|
ge0nemnf |
|- ( ( ( F ` A ) e. RR* /\ 0 <_ ( F ` A ) ) -> ( F ` A ) =/= -oo ) |
63 |
33 61 62
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) =/= -oo ) |
64 |
33 63
|
jca |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) ) |
65 |
64
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) ) |
66 |
|
xrnemnf |
|- ( ( ( F ` A ) e. RR* /\ ( F ` A ) =/= -oo ) <-> ( ( F ` A ) e. RR \/ ( F ` A ) = +oo ) ) |
67 |
65 66
|
sylib |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( ( F ` A ) e. RR \/ ( F ` A ) = +oo ) ) |
68 |
26 58 67
|
mpjaod |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) e. RR ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
69 |
|
pnfnlt |
|- ( ( F ` A ) e. RR* -> -. +oo < ( F ` A ) ) |
70 |
33 69
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> -. +oo < ( F ` A ) ) |
71 |
70
|
adantr |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> -. +oo < ( F ` A ) ) |
72 |
36
|
xnegcld |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> -e ( A D B ) e. RR* ) |
73 |
33 72
|
xaddcld |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) |
74 |
|
xbln0 |
|- ( ( D e. ( *Met ` X ) /\ B e. X /\ ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) ) |
75 |
7 9 73 74
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) ) |
76 |
|
xposdif |
|- ( ( ( A D B ) e. RR* /\ ( F ` A ) e. RR* ) -> ( ( A D B ) < ( F ` A ) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) ) |
77 |
36 33 76
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) < ( F ` A ) <-> 0 < ( ( F ` A ) +e -e ( A D B ) ) ) ) |
78 |
75 77
|
bitr4d |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> ( A D B ) < ( F ` A ) ) ) |
79 |
|
breq1 |
|- ( ( A D B ) = +oo -> ( ( A D B ) < ( F ` A ) <-> +oo < ( F ` A ) ) ) |
80 |
78 79
|
sylan9bb |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) =/= (/) <-> +oo < ( F ` A ) ) ) |
81 |
80
|
necon1bbid |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( -. +oo < ( F ` A ) <-> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = (/) ) ) |
82 |
71 81
|
mpbid |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) = (/) ) |
83 |
|
0ss |
|- (/) C_ ( A ( ball ` D ) ( F ` A ) ) |
84 |
82 83
|
eqsstrdi |
|- ( ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) /\ ( A D B ) = +oo ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
85 |
|
xmetge0 |
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) ) |
86 |
7 11 9 85
|
syl3anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( A D B ) ) |
87 |
|
ge0nemnf |
|- ( ( ( A D B ) e. RR* /\ 0 <_ ( A D B ) ) -> ( A D B ) =/= -oo ) |
88 |
36 86 87
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) =/= -oo ) |
89 |
36 88
|
jca |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. RR* /\ ( A D B ) =/= -oo ) ) |
90 |
|
xrnemnf |
|- ( ( ( A D B ) e. RR* /\ ( A D B ) =/= -oo ) <-> ( ( A D B ) e. RR \/ ( A D B ) = +oo ) ) |
91 |
89 90
|
sylib |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. RR \/ ( A D B ) = +oo ) ) |
92 |
68 84 91
|
mpjaodan |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) ) |
93 |
|
sslin |
|- ( ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) C_ ( A ( ball ` D ) ( F ` A ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) ) |
94 |
92 93
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) ) |
95 |
33
|
xrleidd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( F ` A ) ) |
96 |
|
simplr |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> S C_ X ) |
97 |
1
|
metdsge |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ A e. X ) /\ ( F ` A ) e. RR* ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) ) |
98 |
7 96 11 33 97
|
syl31anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) <_ ( F ` A ) <-> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) ) |
99 |
95 98
|
mpbid |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) |
100 |
|
sseq0 |
|- ( ( ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) C_ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) /\ ( S i^i ( A ( ball ` D ) ( F ` A ) ) ) = (/) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) |
101 |
94 99 100
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) |
102 |
1
|
metdsge |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ B e. X ) /\ ( ( F ` A ) +e -e ( A D B ) ) e. RR* ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) ) |
103 |
7 96 9 73 102
|
syl31anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( S i^i ( B ( ball ` D ) ( ( F ` A ) +e -e ( A D B ) ) ) ) = (/) ) ) |
104 |
101 103
|
mpbird |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) ) |
105 |
30 9
|
ffvelrnd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` B ) e. ( 0 [,] +oo ) ) |
106 |
|
eliccxr |
|- ( ( F ` B ) e. ( 0 [,] +oo ) -> ( F ` B ) e. RR* ) |
107 |
105 106
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` B ) e. RR* ) |
108 |
|
elxrge0 |
|- ( ( F ` B ) e. ( 0 [,] +oo ) <-> ( ( F ` B ) e. RR* /\ 0 <_ ( F ` B ) ) ) |
109 |
108
|
simprbi |
|- ( ( F ` B ) e. ( 0 [,] +oo ) -> 0 <_ ( F ` B ) ) |
110 |
105 109
|
syl |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( F ` B ) ) |
111 |
|
xlesubadd |
|- ( ( ( ( F ` A ) e. RR* /\ ( A D B ) e. RR* /\ ( F ` B ) e. RR* ) /\ ( 0 <_ ( F ` A ) /\ ( A D B ) =/= -oo /\ 0 <_ ( F ` B ) ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) ) ) |
112 |
33 36 107 61 88 110 111
|
syl33anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` A ) +e -e ( A D B ) ) <_ ( F ` B ) <-> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) ) ) |
113 |
104 112
|
mpbid |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( F ` B ) +e ( A D B ) ) ) |
114 |
|
xaddcom |
|- ( ( ( F ` B ) e. RR* /\ ( A D B ) e. RR* ) -> ( ( F ` B ) +e ( A D B ) ) = ( ( A D B ) +e ( F ` B ) ) ) |
115 |
107 36 114
|
syl2anc |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` B ) +e ( A D B ) ) = ( ( A D B ) +e ( F ` B ) ) ) |
116 |
113 115
|
breqtrd |
|- ( ( ( D e. ( *Met ` X ) /\ S C_ X ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) <_ ( ( A D B ) +e ( F ` B ) ) ) |