Step | Hyp | Ref
| Expression |
1 | | anandi3r 1104 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π΄ β€ 1 β§ π₯ < π΄) β ((π₯ β β β§ π΄ β€ 1) β§ (π₯ < π΄ β§ π΄ β€ 1))) |
2 | | rexr 11208 |
. . . . . . . . . . . 12
β’ (π₯ β β β π₯ β
β*) |
3 | | lerelxr 11225 |
. . . . . . . . . . . . . 14
β’ β€
β (β* Γ β*) |
4 | 3 | brel 5702 |
. . . . . . . . . . . . 13
β’ (π΄ β€ 1 β (π΄ β β*
β§ 1 β β*)) |
5 | 4 | simpld 496 |
. . . . . . . . . . . 12
β’ (π΄ β€ 1 β π΄ β
β*) |
6 | | 1xr 11221 |
. . . . . . . . . . . . 13
β’ 1 β
β* |
7 | | xrltletr 13083 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β*
β§ π΄ β
β* β§ 1 β β*) β ((π₯ < π΄ β§ π΄ β€ 1) β π₯ < 1)) |
8 | | xrltle 13075 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ 1 β β*) β (π₯ < 1 β π₯ β€ 1)) |
9 | 8 | 3adant2 1132 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β*
β§ π΄ β
β* β§ 1 β β*) β (π₯ < 1 β π₯ β€ 1)) |
10 | 7, 9 | syld 47 |
. . . . . . . . . . . . 13
β’ ((π₯ β β*
β§ π΄ β
β* β§ 1 β β*) β ((π₯ < π΄ β§ π΄ β€ 1) β π₯ β€ 1)) |
11 | 6, 10 | mp3an3 1451 |
. . . . . . . . . . . 12
β’ ((π₯ β β*
β§ π΄ β
β*) β ((π₯ < π΄ β§ π΄ β€ 1) β π₯ β€ 1)) |
12 | 2, 5, 11 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π΄ β€ 1) β ((π₯ < π΄ β§ π΄ β€ 1) β π₯ β€ 1)) |
13 | 12 | imp 408 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π΄ β€ 1) β§ (π₯ < π΄ β§ π΄ β€ 1)) β π₯ β€ 1) |
14 | 1, 13 | sylbi 216 |
. . . . . . . . 9
β’ ((π₯ β β β§ π΄ β€ 1 β§ π₯ < π΄) β π₯ β€ 1) |
15 | 14 | 3com12 1124 |
. . . . . . . 8
β’ ((π΄ β€ 1 β§ π₯ β β β§ π₯ < π΄) β π₯ β€ 1) |
16 | 15 | 3expib 1123 |
. . . . . . 7
β’ (π΄ β€ 1 β ((π₯ β β β§ π₯ < π΄) β π₯ β€ 1)) |
17 | 16 | pm4.71d 563 |
. . . . . 6
β’ (π΄ β€ 1 β ((π₯ β β β§ π₯ < π΄) β ((π₯ β β β§ π₯ < π΄) β§ π₯ β€ 1))) |
18 | 17 | anbi1d 631 |
. . . . 5
β’ (π΄ β€ 1 β (((π₯ β β β§ π₯ < π΄) β§ 0 β€ π₯) β (((π₯ β β β§ π₯ < π΄) β§ π₯ β€ 1) β§ 0 β€ π₯))) |
19 | | 3anan32 1098 |
. . . . 5
β’ ((π₯ β β β§ 0 β€
π₯ β§ π₯ < π΄) β ((π₯ β β β§ π₯ < π΄) β§ 0 β€ π₯)) |
20 | | 3anass 1096 |
. . . . . . 7
β’ ((π₯ β β β§ 0 β€
π₯ β§ π₯ β€ 1) β (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1))) |
21 | 20 | anbi2i 624 |
. . . . . 6
β’ (((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β ((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
22 | | anandi 675 |
. . . . . 6
β’ ((π₯ β β β§ (π₯ < π΄ β§ (0 β€ π₯ β§ π₯ β€ 1))) β ((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
23 | | 3anass 1096 |
. . . . . . 7
β’ (((π₯ β β β§ π₯ < π΄) β§ 0 β€ π₯ β§ π₯ β€ 1) β ((π₯ β β β§ π₯ < π΄) β§ (0 β€ π₯ β§ π₯ β€ 1))) |
24 | | 3anan32 1098 |
. . . . . . 7
β’ (((π₯ β β β§ π₯ < π΄) β§ 0 β€ π₯ β§ π₯ β€ 1) β (((π₯ β β β§ π₯ < π΄) β§ π₯ β€ 1) β§ 0 β€ π₯)) |
25 | | anass 470 |
. . . . . . 7
β’ (((π₯ β β β§ π₯ < π΄) β§ (0 β€ π₯ β§ π₯ β€ 1)) β (π₯ β β β§ (π₯ < π΄ β§ (0 β€ π₯ β§ π₯ β€ 1)))) |
26 | 23, 24, 25 | 3bitr3ri 302 |
. . . . . 6
β’ ((π₯ β β β§ (π₯ < π΄ β§ (0 β€ π₯ β§ π₯ β€ 1))) β (((π₯ β β β§ π₯ < π΄) β§ π₯ β€ 1) β§ 0 β€ π₯)) |
27 | 21, 22, 26 | 3bitr2i 299 |
. . . . 5
β’ (((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β (((π₯ β β β§ π₯ < π΄) β§ π₯ β€ 1) β§ 0 β€ π₯)) |
28 | 18, 19, 27 | 3bitr4g 314 |
. . . 4
β’ (π΄ β€ 1 β ((π₯ β β β§ 0 β€
π₯ β§ π₯ < π΄) β ((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
29 | | 0re 11164 |
. . . . 5
β’ 0 β
β |
30 | | elico2 13335 |
. . . . 5
β’ ((0
β β β§ π΄
β β*) β (π₯ β (0[,)π΄) β (π₯ β β β§ 0 β€ π₯ β§ π₯ < π΄))) |
31 | 29, 5, 30 | sylancr 588 |
. . . 4
β’ (π΄ β€ 1 β (π₯ β (0[,)π΄) β (π₯ β β β§ 0 β€ π₯ β§ π₯ < π΄))) |
32 | | elin 3931 |
. . . . . 6
β’ (π₯ β ((-β(,)π΄) β© (0[,]1)) β (π₯ β (-β(,)π΄) β§ π₯ β (0[,]1))) |
33 | | elicc01 13390 |
. . . . . . 7
β’ (π₯ β (0[,]1) β (π₯ β β β§ 0 β€
π₯ β§ π₯ β€ 1)) |
34 | 33 | anbi2i 624 |
. . . . . 6
β’ ((π₯ β (-β(,)π΄) β§ π₯ β (0[,]1)) β (π₯ β (-β(,)π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1))) |
35 | 32, 34 | bitri 275 |
. . . . 5
β’ (π₯ β ((-β(,)π΄) β© (0[,]1)) β (π₯ β (-β(,)π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1))) |
36 | | elioomnf 13368 |
. . . . . . 7
β’ (π΄ β β*
β (π₯ β
(-β(,)π΄) β
(π₯ β β β§
π₯ < π΄))) |
37 | 5, 36 | syl 17 |
. . . . . 6
β’ (π΄ β€ 1 β (π₯ β (-β(,)π΄) β (π₯ β β β§ π₯ < π΄))) |
38 | 37 | anbi1d 631 |
. . . . 5
β’ (π΄ β€ 1 β ((π₯ β (-β(,)π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)) β ((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
39 | 35, 38 | bitrid 283 |
. . . 4
β’ (π΄ β€ 1 β (π₯ β ((-β(,)π΄) β© (0[,]1)) β ((π₯ β β β§ π₯ < π΄) β§ (π₯ β β β§ 0 β€ π₯ β§ π₯ β€ 1)))) |
40 | 28, 31, 39 | 3bitr4rd 312 |
. . 3
β’ (π΄ β€ 1 β (π₯ β ((-β(,)π΄) β© (0[,]1)) β π₯ β (0[,)π΄))) |
41 | 40 | eqrdv 2735 |
. 2
β’ (π΄ β€ 1 β
((-β(,)π΄) β©
(0[,]1)) = (0[,)π΄)) |
42 | | fvex 6860 |
. . . 4
β’
(topGenβran (,)) β V |
43 | | ovex 7395 |
. . . 4
β’ (0[,]1)
β V |
44 | | iooretop 24145 |
. . . 4
β’
(-β(,)π΄)
β (topGenβran (,)) |
45 | | elrestr 17317 |
. . . 4
β’
(((topGenβran (,)) β V β§ (0[,]1) β V β§
(-β(,)π΄) β
(topGenβran (,))) β ((-β(,)π΄) β© (0[,]1)) β ((topGenβran
(,)) βΎt (0[,]1))) |
46 | 42, 43, 44, 45 | mp3an 1462 |
. . 3
β’
((-β(,)π΄)
β© (0[,]1)) β ((topGenβran (,)) βΎt
(0[,]1)) |
47 | | dfii2 24261 |
. . 3
β’ II =
((topGenβran (,)) βΎt (0[,]1)) |
48 | 46, 47 | eleqtrri 2837 |
. 2
β’
((-β(,)π΄)
β© (0[,]1)) β II |
49 | 41, 48 | eqeltrrdi 2847 |
1
β’ (π΄ β€ 1 β (0[,)π΄) β II) |