Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
β’ β β V |
2 |
|
elssuni |
β’ ( π΄ β ( topGen β ran (,) ) β π΄ β βͺ ( topGen β ran (,) ) ) |
3 |
|
uniretop |
β’ β = βͺ ( topGen β ran (,) ) |
4 |
2 3
|
sseqtrrdi |
β’ ( π΄ β ( topGen β ran (,) ) β π΄ β β ) |
5 |
|
ssdomg |
β’ ( β β V β ( π΄ β β β π΄ βΌ β ) ) |
6 |
1 4 5
|
mpsyl |
β’ ( π΄ β ( topGen β ran (,) ) β π΄ βΌ β ) |
7 |
|
rpnnen |
β’ β β π« β |
8 |
|
domentr |
β’ ( ( π΄ βΌ β β§ β β π« β ) β π΄ βΌ π« β ) |
9 |
6 7 8
|
sylancl |
β’ ( π΄ β ( topGen β ran (,) ) β π΄ βΌ π« β ) |
10 |
|
n0 |
β’ ( π΄ β β
β β π₯ π₯ β π΄ ) |
11 |
4
|
sselda |
β’ ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β π₯ β β ) |
12 |
|
rpnnen2 |
β’ π« β βΌ ( 0 [,] 1 ) |
13 |
|
rphalfcl |
β’ ( π¦ β β+ β ( π¦ / 2 ) β β+ ) |
14 |
13
|
rpred |
β’ ( π¦ β β+ β ( π¦ / 2 ) β β ) |
15 |
|
resubcl |
β’ ( ( π₯ β β β§ ( π¦ / 2 ) β β ) β ( π₯ β ( π¦ / 2 ) ) β β ) |
16 |
14 15
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β ( π¦ / 2 ) ) β β ) |
17 |
|
readdcl |
β’ ( ( π₯ β β β§ ( π¦ / 2 ) β β ) β ( π₯ + ( π¦ / 2 ) ) β β ) |
18 |
14 17
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + ( π¦ / 2 ) ) β β ) |
19 |
|
simpl |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π₯ β β ) |
20 |
|
ltsubrp |
β’ ( ( π₯ β β β§ ( π¦ / 2 ) β β+ ) β ( π₯ β ( π¦ / 2 ) ) < π₯ ) |
21 |
13 20
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β ( π¦ / 2 ) ) < π₯ ) |
22 |
|
ltaddrp |
β’ ( ( π₯ β β β§ ( π¦ / 2 ) β β+ ) β π₯ < ( π₯ + ( π¦ / 2 ) ) ) |
23 |
13 22
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π₯ < ( π₯ + ( π¦ / 2 ) ) ) |
24 |
16 19 18 21 23
|
lttrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β ( π¦ / 2 ) ) < ( π₯ + ( π¦ / 2 ) ) ) |
25 |
|
iccen |
β’ ( ( ( π₯ β ( π¦ / 2 ) ) β β β§ ( π₯ + ( π¦ / 2 ) ) β β β§ ( π₯ β ( π¦ / 2 ) ) < ( π₯ + ( π¦ / 2 ) ) ) β ( 0 [,] 1 ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) ) |
26 |
16 18 24 25
|
syl3anc |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( 0 [,] 1 ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) ) |
27 |
|
domentr |
β’ ( ( π« β βΌ ( 0 [,] 1 ) β§ ( 0 [,] 1 ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) ) β π« β βΌ ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) ) |
28 |
12 26 27
|
sylancr |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π« β βΌ ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) ) |
29 |
|
ovex |
β’ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) β V |
30 |
|
rpre |
β’ ( π¦ β β+ β π¦ β β ) |
31 |
|
resubcl |
β’ ( ( π₯ β β β§ π¦ β β ) β ( π₯ β π¦ ) β β ) |
32 |
30 31
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β π¦ ) β β ) |
33 |
32
|
rexrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β π¦ ) β β* ) |
34 |
|
readdcl |
β’ ( ( π₯ β β β§ π¦ β β ) β ( π₯ + π¦ ) β β ) |
35 |
30 34
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + π¦ ) β β ) |
36 |
35
|
rexrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + π¦ ) β β* ) |
37 |
19
|
recnd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π₯ β β ) |
38 |
14
|
adantl |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π¦ / 2 ) β β ) |
39 |
38
|
recnd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π¦ / 2 ) β β ) |
40 |
37 39 39
|
subsub4d |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ β ( π¦ / 2 ) ) β ( π¦ / 2 ) ) = ( π₯ β ( ( π¦ / 2 ) + ( π¦ / 2 ) ) ) ) |
41 |
30
|
adantl |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π¦ β β ) |
42 |
41
|
recnd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π¦ β β ) |
43 |
42
|
2halvesd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π¦ / 2 ) + ( π¦ / 2 ) ) = π¦ ) |
44 |
43
|
oveq2d |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β ( ( π¦ / 2 ) + ( π¦ / 2 ) ) ) = ( π₯ β π¦ ) ) |
45 |
40 44
|
eqtrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ β ( π¦ / 2 ) ) β ( π¦ / 2 ) ) = ( π₯ β π¦ ) ) |
46 |
13
|
adantl |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π¦ / 2 ) β β+ ) |
47 |
16 46
|
ltsubrpd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ β ( π¦ / 2 ) ) β ( π¦ / 2 ) ) < ( π₯ β ( π¦ / 2 ) ) ) |
48 |
45 47
|
eqbrtrrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ β π¦ ) < ( π₯ β ( π¦ / 2 ) ) ) |
49 |
18 46
|
ltaddrpd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + ( π¦ / 2 ) ) < ( ( π₯ + ( π¦ / 2 ) ) + ( π¦ / 2 ) ) ) |
50 |
37 39 39
|
addassd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ + ( π¦ / 2 ) ) + ( π¦ / 2 ) ) = ( π₯ + ( ( π¦ / 2 ) + ( π¦ / 2 ) ) ) ) |
51 |
43
|
oveq2d |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + ( ( π¦ / 2 ) + ( π¦ / 2 ) ) ) = ( π₯ + π¦ ) ) |
52 |
50 51
|
eqtrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ + ( π¦ / 2 ) ) + ( π¦ / 2 ) ) = ( π₯ + π¦ ) ) |
53 |
49 52
|
breqtrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ + ( π¦ / 2 ) ) < ( π₯ + π¦ ) ) |
54 |
|
iccssioo |
β’ ( ( ( ( π₯ β π¦ ) β β* β§ ( π₯ + π¦ ) β β* ) β§ ( ( π₯ β π¦ ) < ( π₯ β ( π¦ / 2 ) ) β§ ( π₯ + ( π¦ / 2 ) ) < ( π₯ + π¦ ) ) ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) β ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
55 |
33 36 48 53 54
|
syl22anc |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) β ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
56 |
|
ssdomg |
β’ ( ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) β V β ( ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) β ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) βΌ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) ) |
57 |
29 55 56
|
mpsyl |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) βΌ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
58 |
|
domtr |
β’ ( ( π« β βΌ ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) β§ ( ( π₯ β ( π¦ / 2 ) ) [,] ( π₯ + ( π¦ / 2 ) ) ) βΌ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) β π« β βΌ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
59 |
28 57 58
|
syl2anc |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π« β βΌ ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
60 |
|
eqid |
β’ ( ( abs β β ) βΎ ( β Γ β ) ) = ( ( abs β β ) βΎ ( β Γ β ) ) |
61 |
60
|
bl2ioo |
β’ ( ( π₯ β β β§ π¦ β β ) β ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) = ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
62 |
30 61
|
sylan2 |
β’ ( ( π₯ β β β§ π¦ β β+ ) β ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) = ( ( π₯ β π¦ ) (,) ( π₯ + π¦ ) ) ) |
63 |
59 62
|
breqtrrd |
β’ ( ( π₯ β β β§ π¦ β β+ ) β π« β βΌ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) ) |
64 |
11 63
|
sylan |
β’ ( ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β§ π¦ β β+ ) β π« β βΌ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) ) |
65 |
|
simplll |
β’ ( ( ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β§ π¦ β β+ ) β§ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) β π΄ β ( topGen β ran (,) ) ) |
66 |
|
simpr |
β’ ( ( ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β§ π¦ β β+ ) β§ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) β ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) |
67 |
|
ssdomg |
β’ ( π΄ β ( topGen β ran (,) ) β ( ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ β ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) βΌ π΄ ) ) |
68 |
65 66 67
|
sylc |
β’ ( ( ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β§ π¦ β β+ ) β§ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) β ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) βΌ π΄ ) |
69 |
|
domtr |
β’ ( ( π« β βΌ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β§ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) βΌ π΄ ) β π« β βΌ π΄ ) |
70 |
64 68 69
|
syl2an2r |
β’ ( ( ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β§ π¦ β β+ ) β§ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) β π« β βΌ π΄ ) |
71 |
|
eqid |
β’ ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) = ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) |
72 |
60 71
|
tgioo |
β’ ( topGen β ran (,) ) = ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) |
73 |
72
|
eleq2i |
β’ ( π΄ β ( topGen β ran (,) ) β π΄ β ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) ) |
74 |
60
|
rexmet |
β’ ( ( abs β β ) βΎ ( β Γ β ) ) β ( βMet β β ) |
75 |
71
|
mopni2 |
β’ ( ( ( ( abs β β ) βΎ ( β Γ β ) ) β ( βMet β β ) β§ π΄ β ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) β§ π₯ β π΄ ) β β π¦ β β+ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) |
76 |
74 75
|
mp3an1 |
β’ ( ( π΄ β ( MetOpen β ( ( abs β β ) βΎ ( β Γ β ) ) ) β§ π₯ β π΄ ) β β π¦ β β+ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) |
77 |
73 76
|
sylanb |
β’ ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β β π¦ β β+ ( π₯ ( ball β ( ( abs β β ) βΎ ( β Γ β ) ) ) π¦ ) β π΄ ) |
78 |
70 77
|
r19.29a |
β’ ( ( π΄ β ( topGen β ran (,) ) β§ π₯ β π΄ ) β π« β βΌ π΄ ) |
79 |
78
|
ex |
β’ ( π΄ β ( topGen β ran (,) ) β ( π₯ β π΄ β π« β βΌ π΄ ) ) |
80 |
79
|
exlimdv |
β’ ( π΄ β ( topGen β ran (,) ) β ( β π₯ π₯ β π΄ β π« β βΌ π΄ ) ) |
81 |
10 80
|
biimtrid |
β’ ( π΄ β ( topGen β ran (,) ) β ( π΄ β β
β π« β βΌ π΄ ) ) |
82 |
81
|
imp |
β’ ( ( π΄ β ( topGen β ran (,) ) β§ π΄ β β
) β π« β βΌ π΄ ) |
83 |
|
sbth |
β’ ( ( π΄ βΌ π« β β§ π« β βΌ π΄ ) β π΄ β π« β ) |
84 |
9 82 83
|
syl2an2r |
β’ ( ( π΄ β ( topGen β ran (,) ) β§ π΄ β β
) β π΄ β π« β ) |