Step | Hyp | Ref
| Expression |
1 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
2 | | lerelxr 11225 |
. . . . . . . . . . . . 13
β’ β€
β (β* Γ β*) |
3 | 2 | brel 5702 |
. . . . . . . . . . . 12
β’ (0 β€
π΄ β (0 β
β* β§ π΄
β β*)) |
4 | 3 | simprd 497 |
. . . . . . . . . . 11
β’ (0 β€
π΄ β π΄ β
β*) |
5 | | rexr 11208 |
. . . . . . . . . . 11
β’ (π₯ β β β π₯ β
β*) |
6 | | xrlelttr 13082 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ π΄ β β* β§ π₯ β β*)
β ((0 β€ π΄ β§
π΄ < π₯) β 0 < π₯)) |
7 | | xrltle 13075 |
. . . . . . . . . . . . 13
β’ ((0
β β* β§ π₯ β β*) β (0 <
π₯ β 0 β€ π₯)) |
8 | 7 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ π΄ β β* β§ π₯ β β*)
β (0 < π₯ β 0
β€ π₯)) |
9 | 6, 8 | syld 47 |
. . . . . . . . . . 11
β’ ((0
β β* β§ π΄ β β* β§ π₯ β β*)
β ((0 β€ π΄ β§
π΄ < π₯) β 0 β€ π₯)) |
10 | 1, 4, 5, 9 | mp3an3an 1468 |
. . . . . . . . . 10
β’ ((0 β€
π΄ β§ π₯ β β) β ((0 β€ π΄ β§ π΄ < π₯) β 0 β€ π₯)) |
11 | 10 | imp 408 |
. . . . . . . . 9
β’ (((0 β€
π΄ β§ π₯ β β) β§ (0 β€ π΄ β§ π΄ < π₯)) β 0 β€ π₯) |
12 | 11 | 3impdi 1351 |
. . . . . . . 8
β’ ((0 β€
π΄ β§ π₯ β β β§ π΄ < π₯) β 0 β€ π₯) |
13 | 12 | 3expib 1123 |
. . . . . . 7
β’ (0 β€
π΄ β ((π₯ β β β§ π΄ < π₯) β 0 β€ π₯)) |
14 | 13 | pm4.71d 563 |
. . . . . 6
β’ (0 β€
π΄ β ((π₯ β β β§ π΄ < π₯) β ((π₯ β β β§ π΄ < π₯) β§ 0 β€ π₯))) |
15 | 14 | anbi1d 631 |
. . . . 5
β’ (0 β€
π΄ β (((π₯ β β β§ π΄ < π₯) β§ π₯ β€ 1) β (((π₯ β β β§ π΄ < π₯) β§ 0 β€ π₯) β§ π₯ β€ 1))) |
16 | | df-3an 1090 |
. . . . 5
β’ ((π₯ β β β§ π΄ < π₯ β§ π₯ β€ 1) β ((π₯ β β β§ π΄ < π₯) β§ π₯ β€ 1)) |
17 | | 3anass 1096 |
. . . . . . 7
β’ ((π₯ β β β§ 0 β€
π₯ β§ π₯ β€ 1) β (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1))) |
18 | 17 | anbi2i 624 |
. . . . . 6
β’ (((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β ((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
19 | | anandi 675 |
. . . . . 6
β’ ((π₯ β β β§ (π΄ < π₯ β§ (0 β€ π₯ β§ π₯ β€ 1))) β ((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
20 | | anass 470 |
. . . . . . 7
β’ ((((π₯ β β β§ π΄ < π₯) β§ 0 β€ π₯) β§ π₯ β€ 1) β ((π₯ β β β§ π΄ < π₯) β§ (0 β€ π₯ β§ π₯ β€ 1))) |
21 | | anass 470 |
. . . . . . 7
β’ (((π₯ β β β§ π΄ < π₯) β§ (0 β€ π₯ β§ π₯ β€ 1)) β (π₯ β β β§ (π΄ < π₯ β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
22 | 20, 21 | bitr2i 276 |
. . . . . 6
β’ ((π₯ β β β§ (π΄ < π₯ β§ (0 β€ π₯ β§ π₯ β€ 1))) β (((π₯ β β β§ π΄ < π₯) β§ 0 β€ π₯) β§ π₯ β€ 1)) |
23 | 18, 19, 22 | 3bitr2i 299 |
. . . . 5
β’ (((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β (((π₯ β β β§ π΄ < π₯) β§ 0 β€ π₯) β§ π₯ β€ 1)) |
24 | 15, 16, 23 | 3bitr4g 314 |
. . . 4
β’ (0 β€
π΄ β ((π₯ β β β§ π΄ < π₯ β§ π₯ β€ 1) β ((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
25 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
26 | | elioc2 13334 |
. . . . 5
β’ ((π΄ β β*
β§ 1 β β) β (π₯ β (π΄(,]1) β (π₯ β β β§ π΄ < π₯ β§ π₯ β€ 1))) |
27 | 4, 25, 26 | sylancl 587 |
. . . 4
β’ (0 β€
π΄ β (π₯ β (π΄(,]1) β (π₯ β β β§ π΄ < π₯ β§ π₯ β€ 1))) |
28 | | elin 3931 |
. . . . . 6
β’ (π₯ β ((π΄(,)+β) β© (0[,]1)) β (π₯ β (π΄(,)+β) β§ π₯ β (0[,]1))) |
29 | | elicc01 13390 |
. . . . . . 7
β’ (π₯ β (0[,]1) β (π₯ β β β§ 0 β€
π₯ β§ π₯ β€ 1)) |
30 | 29 | anbi2i 624 |
. . . . . 6
β’ ((π₯ β (π΄(,)+β) β§ π₯ β (0[,]1)) β (π₯ β (π΄(,)+β) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1))) |
31 | 28, 30 | bitri 275 |
. . . . 5
β’ (π₯ β ((π΄(,)+β) β© (0[,]1)) β (π₯ β (π΄(,)+β) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1))) |
32 | | elioopnf 13367 |
. . . . . . 7
β’ (π΄ β β*
β (π₯ β (π΄(,)+β) β (π₯ β β β§ π΄ < π₯))) |
33 | 4, 32 | syl 17 |
. . . . . 6
β’ (0 β€
π΄ β (π₯ β (π΄(,)+β) β (π₯ β β β§ π΄ < π₯))) |
34 | 33 | anbi1d 631 |
. . . . 5
β’ (0 β€
π΄ β ((π₯ β (π΄(,)+β) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β ((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
35 | 31, 34 | bitrid 283 |
. . . 4
β’ (0 β€
π΄ β (π₯ β ((π΄(,)+β) β© (0[,]1)) β ((π₯ β β β§ π΄ < π₯) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
36 | 24, 27, 35 | 3bitr4rd 312 |
. . 3
β’ (0 β€
π΄ β (π₯ β ((π΄(,)+β) β© (0[,]1)) β π₯ β (π΄(,]1))) |
37 | 36 | eqrdv 2735 |
. 2
β’ (0 β€
π΄ β ((π΄(,)+β) β© (0[,]1)) =
(π΄(,]1)) |
38 | | fvex 6860 |
. . . 4
β’
(topGenβran (,)) β V |
39 | | ovex 7395 |
. . . 4
β’ (0[,]1)
β V |
40 | | iooretop 24145 |
. . . 4
β’ (π΄(,)+β) β
(topGenβran (,)) |
41 | | elrestr 17317 |
. . . 4
β’
(((topGenβran (,)) β V β§ (0[,]1) β V β§ (π΄(,)+β) β
(topGenβran (,))) β ((π΄(,)+β) β© (0[,]1)) β
((topGenβran (,)) βΎt (0[,]1))) |
42 | 38, 39, 40, 41 | mp3an 1462 |
. . 3
β’ ((π΄(,)+β) β© (0[,]1))
β ((topGenβran (,)) βΎt (0[,]1)) |
43 | | dfii2 24261 |
. . 3
β’ II =
((topGenβran (,)) βΎt (0[,]1)) |
44 | 42, 43 | eleqtrri 2837 |
. 2
β’ ((π΄(,)+β) β© (0[,]1))
β II |
45 | 37, 44 | eqeltrrdi 2847 |
1
β’ (0 β€
π΄ β (π΄(,]1) β II) |