Step | Hyp | Ref
| Expression |
1 | | reex 11150 |
. . . 4
β’ β
β V |
2 | | elssuni 4902 |
. . . . 5
β’ (π΄ β (topGenβran (,))
β π΄ β βͺ (topGenβran (,))) |
3 | | uniretop 24149 |
. . . . 5
β’ β =
βͺ (topGenβran (,)) |
4 | 2, 3 | sseqtrrdi 3999 |
. . . 4
β’ (π΄ β (topGenβran (,))
β π΄ β
β) |
5 | | ssdomg 8946 |
. . . 4
β’ (β
β V β (π΄ β
β β π΄ βΌ
β)) |
6 | 1, 4, 5 | mpsyl 68 |
. . 3
β’ (π΄ β (topGenβran (,))
β π΄ βΌ
β) |
7 | | rpnnen 16117 |
. . 3
β’ β
β π« β |
8 | | domentr 8959 |
. . 3
β’ ((π΄ βΌ β β§ β
β π« β) β π΄ βΌ π« β) |
9 | 6, 7, 8 | sylancl 587 |
. 2
β’ (π΄ β (topGenβran (,))
β π΄ βΌ π«
β) |
10 | | n0 4310 |
. . . 4
β’ (π΄ β β
β
βπ₯ π₯ β π΄) |
11 | 4 | sselda 3948 |
. . . . . . . . 9
β’ ((π΄ β (topGenβran (,))
β§ π₯ β π΄) β π₯ β β) |
12 | | rpnnen2 16116 |
. . . . . . . . . . . 12
β’ π«
β βΌ (0[,]1) |
13 | | rphalfcl 12950 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β+
β (π¦ / 2) β
β+) |
14 | 13 | rpred 12965 |
. . . . . . . . . . . . . 14
β’ (π¦ β β+
β (π¦ / 2) β
β) |
15 | | resubcl 11473 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ (π¦ / 2) β β) β
(π₯ β (π¦ / 2)) β
β) |
16 | 14, 15 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β (π¦ / 2)) β
β) |
17 | | readdcl 11142 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ (π¦ / 2) β β) β
(π₯ + (π¦ / 2)) β β) |
18 | 14, 17 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + (π¦ / 2)) β
β) |
19 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β π₯ β
β) |
20 | | ltsubrp 12959 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ (π¦ / 2) β
β+) β (π₯ β (π¦ / 2)) < π₯) |
21 | 13, 20 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β (π¦ / 2)) < π₯) |
22 | | ltaddrp 12960 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ (π¦ / 2) β
β+) β π₯ < (π₯ + (π¦ / 2))) |
23 | 13, 22 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β π₯ < (π₯ + (π¦ / 2))) |
24 | 16, 19, 18, 21, 23 | lttrd 11324 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β (π¦ / 2)) < (π₯ + (π¦ / 2))) |
25 | | iccen 13423 |
. . . . . . . . . . . . 13
β’ (((π₯ β (π¦ / 2)) β β β§ (π₯ + (π¦ / 2)) β β β§ (π₯ β (π¦ / 2)) < (π₯ + (π¦ / 2))) β (0[,]1) β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2)))) |
26 | 16, 18, 24, 25 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β+)
β (0[,]1) β ((π₯
β (π¦ / 2))[,](π₯ + (π¦ / 2)))) |
27 | | domentr 8959 |
. . . . . . . . . . . 12
β’
((π« β βΌ (0[,]1) β§ (0[,]1) β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2)))) β π« β βΌ
((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2)))) |
28 | 12, 26, 27 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β+)
β π« β βΌ ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2)))) |
29 | | ovex 7394 |
. . . . . . . . . . . 12
β’ ((π₯ β π¦)(,)(π₯ + π¦)) β V |
30 | | rpre 12931 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β+
β π¦ β
β) |
31 | | resubcl 11473 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β (π₯ β π¦) β β) |
32 | 30, 31 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β π¦) β
β) |
33 | 32 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β π¦) β
β*) |
34 | | readdcl 11142 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
35 | 30, 34 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + π¦) β
β) |
36 | 35 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + π¦) β
β*) |
37 | 19 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β+)
β π₯ β
β) |
38 | 14 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β+)
β (π¦ / 2) β
β) |
39 | 38 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β+)
β (π¦ / 2) β
β) |
40 | 37, 39, 39 | subsub4d 11551 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ β (π¦ / 2)) β (π¦ / 2)) = (π₯ β ((π¦ / 2) + (π¦ / 2)))) |
41 | 30 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π¦ β β+)
β π¦ β
β) |
42 | 41 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β+)
β π¦ β
β) |
43 | 42 | 2halvesd 12407 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β+)
β ((π¦ / 2) + (π¦ / 2)) = π¦) |
44 | 43 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β ((π¦ / 2) + (π¦ / 2))) = (π₯ β π¦)) |
45 | 40, 44 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ β (π¦ / 2)) β (π¦ / 2)) = (π₯ β π¦)) |
46 | 13 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β+)
β (π¦ / 2) β
β+) |
47 | 16, 46 | ltsubrpd 12997 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ β (π¦ / 2)) β (π¦ / 2)) < (π₯ β (π¦ / 2))) |
48 | 45, 47 | eqbrtrrd 5133 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ β π¦) < (π₯ β (π¦ / 2))) |
49 | 18, 46 | ltaddrpd 12998 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + (π¦ / 2)) < ((π₯ + (π¦ / 2)) + (π¦ / 2))) |
50 | 37, 39, 39 | addassd 11185 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ + (π¦ / 2)) + (π¦ / 2)) = (π₯ + ((π¦ / 2) + (π¦ / 2)))) |
51 | 43 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + ((π¦ / 2) + (π¦ / 2))) = (π₯ + π¦)) |
52 | 50, 51 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ + (π¦ / 2)) + (π¦ / 2)) = (π₯ + π¦)) |
53 | 49, 52 | breqtrd 5135 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π¦ β β+)
β (π₯ + (π¦ / 2)) < (π₯ + π¦)) |
54 | | iccssioo 13342 |
. . . . . . . . . . . . 13
β’ ((((π₯ β π¦) β β* β§ (π₯ + π¦) β β*) β§ ((π₯ β π¦) < (π₯ β (π¦ / 2)) β§ (π₯ + (π¦ / 2)) < (π₯ + π¦))) β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) β ((π₯ β π¦)(,)(π₯ + π¦))) |
55 | 33, 36, 48, 53, 54 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) β ((π₯ β π¦)(,)(π₯ + π¦))) |
56 | | ssdomg 8946 |
. . . . . . . . . . . 12
β’ (((π₯ β π¦)(,)(π₯ + π¦)) β V β (((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) β ((π₯ β π¦)(,)(π₯ + π¦)) β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) βΌ ((π₯ β π¦)(,)(π₯ + π¦)))) |
57 | 29, 55, 56 | mpsyl 68 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β+)
β ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) βΌ ((π₯ β π¦)(,)(π₯ + π¦))) |
58 | | domtr 8953 |
. . . . . . . . . . 11
β’
((π« β βΌ ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) β§ ((π₯ β (π¦ / 2))[,](π₯ + (π¦ / 2))) βΌ ((π₯ β π¦)(,)(π₯ + π¦))) β π« β βΌ ((π₯ β π¦)(,)(π₯ + π¦))) |
59 | 28, 57, 58 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β+)
β π« β βΌ ((π₯ β π¦)(,)(π₯ + π¦))) |
60 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
61 | 60 | bl2ioo 24178 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) = ((π₯ β π¦)(,)(π₯ + π¦))) |
62 | 30, 61 | sylan2 594 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β+)
β (π₯(ballβ((abs
β β ) βΎ (β Γ β)))π¦) = ((π₯ β π¦)(,)(π₯ + π¦))) |
63 | 59, 62 | breqtrrd 5137 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β+)
β π« β βΌ (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦)) |
64 | 11, 63 | sylan 581 |
. . . . . . . 8
β’ (((π΄ β (topGenβran (,))
β§ π₯ β π΄) β§ π¦ β β+) β π«
β βΌ (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦)) |
65 | | simplll 774 |
. . . . . . . . 9
β’ ((((π΄ β (topGenβran (,))
β§ π₯ β π΄) β§ π¦ β β+) β§ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) β π΄ β (topGenβran
(,))) |
66 | | simpr 486 |
. . . . . . . . 9
β’ ((((π΄ β (topGenβran (,))
β§ π₯ β π΄) β§ π¦ β β+) β§ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) β (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦) β π΄) |
67 | | ssdomg 8946 |
. . . . . . . . 9
β’ (π΄ β (topGenβran (,))
β ((π₯(ballβ((abs
β β ) βΎ (β Γ β)))π¦) β π΄ β (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦) βΌ π΄)) |
68 | 65, 66, 67 | sylc 65 |
. . . . . . . 8
β’ ((((π΄ β (topGenβran (,))
β§ π₯ β π΄) β§ π¦ β β+) β§ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) β (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦) βΌ π΄) |
69 | | domtr 8953 |
. . . . . . . 8
β’
((π« β βΌ (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦) β§ (π₯(ballβ((abs β β ) βΎ
(β Γ β)))π¦) βΌ π΄) β π« β βΌ π΄) |
70 | 64, 68, 69 | syl2an2r 684 |
. . . . . . 7
β’ ((((π΄ β (topGenβran (,))
β§ π₯ β π΄) β§ π¦ β β+) β§ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) β π« β βΌ π΄) |
71 | | eqid 2733 |
. . . . . . . . . 10
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
72 | 60, 71 | tgioo 24182 |
. . . . . . . . 9
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
73 | 72 | eleq2i 2826 |
. . . . . . . 8
β’ (π΄ β (topGenβran (,))
β π΄ β
(MetOpenβ((abs β β ) βΎ (β Γ
β)))) |
74 | 60 | rexmet 24177 |
. . . . . . . . 9
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
75 | 71 | mopni2 23872 |
. . . . . . . . 9
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ π΄ β (MetOpenβ((abs β β
) βΎ (β Γ β))) β§ π₯ β π΄) β βπ¦ β β+ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) |
76 | 74, 75 | mp3an1 1449 |
. . . . . . . 8
β’ ((π΄ β (MetOpenβ((abs
β β ) βΎ (β Γ β))) β§ π₯ β π΄) β βπ¦ β β+ (π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) |
77 | 73, 76 | sylanb 582 |
. . . . . . 7
β’ ((π΄ β (topGenβran (,))
β§ π₯ β π΄) β βπ¦ β β+
(π₯(ballβ((abs β
β ) βΎ (β Γ β)))π¦) β π΄) |
78 | 70, 77 | r19.29a 3156 |
. . . . . 6
β’ ((π΄ β (topGenβran (,))
β§ π₯ β π΄) β π« β
βΌ π΄) |
79 | 78 | ex 414 |
. . . . 5
β’ (π΄ β (topGenβran (,))
β (π₯ β π΄ β π« β
βΌ π΄)) |
80 | 79 | exlimdv 1937 |
. . . 4
β’ (π΄ β (topGenβran (,))
β (βπ₯ π₯ β π΄ β π« β βΌ π΄)) |
81 | 10, 80 | biimtrid 241 |
. . 3
β’ (π΄ β (topGenβran (,))
β (π΄ β β
β π« β βΌ π΄)) |
82 | 81 | imp 408 |
. 2
β’ ((π΄ β (topGenβran (,))
β§ π΄ β β
)
β π« β βΌ π΄) |
83 | | sbth 9043 |
. 2
β’ ((π΄ βΌ π« β β§
π« β βΌ π΄) β π΄ β π« β) |
84 | 9, 82, 83 | syl2an2r 684 |
1
β’ ((π΄ β (topGenβran (,))
β§ π΄ β β
)
β π΄ β π«
β) |