Step | Hyp | Ref
| Expression |
1 | | sepfsepc.1 |
. 2
β’ (π β βπ β (π½ Cn II)(π β (β‘π β {0}) β§ π β (β‘π β {1}))) |
2 | | simpl 484 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β π β (π½ Cn II)) |
3 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
4 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
5 | | 0le0 12261 |
. . . . . . . 8
β’ 0 β€
0 |
6 | | 3re 12240 |
. . . . . . . . . 10
β’ 3 β
β |
7 | | 3ne0 12266 |
. . . . . . . . . 10
β’ 3 β
0 |
8 | 6, 7 | rereccli 11927 |
. . . . . . . . 9
β’ (1 / 3)
β β |
9 | | 1lt3 12333 |
. . . . . . . . . . 11
β’ 1 <
3 |
10 | | recgt1i 12059 |
. . . . . . . . . . 11
β’ ((3
β β β§ 1 < 3) β (0 < (1 / 3) β§ (1 / 3) <
1)) |
11 | 6, 9, 10 | mp2an 691 |
. . . . . . . . . 10
β’ (0 <
(1 / 3) β§ (1 / 3) < 1) |
12 | 11 | simpri 487 |
. . . . . . . . 9
β’ (1 / 3)
< 1 |
13 | 8, 4, 12 | ltleii 11285 |
. . . . . . . 8
β’ (1 / 3)
β€ 1 |
14 | | iccss 13339 |
. . . . . . . 8
β’ (((0
β β β§ 1 β β) β§ (0 β€ 0 β§ (1 / 3) β€ 1))
β (0[,](1 / 3)) β (0[,]1)) |
15 | 3, 4, 5, 13, 14 | mp4an 692 |
. . . . . . 7
β’ (0[,](1 /
3)) β (0[,]1) |
16 | | i0oii 47026 |
. . . . . . . . 9
β’ ((1 / 3)
β€ 1 β (0[,)(1 / 3)) β II) |
17 | 13, 16 | ax-mp 5 |
. . . . . . . 8
β’ (0[,)(1 /
3)) β II |
18 | 11 | simpli 485 |
. . . . . . . . . 10
β’ 0 < (1
/ 3) |
19 | 8 | rexri 11220 |
. . . . . . . . . . . . 13
β’ (1 / 3)
β β* |
20 | | elico2 13335 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ (1 / 3) β β*) β (0 β
(0[,)(1 / 3)) β (0 β β β§ 0 β€ 0 β§ 0 < (1 /
3)))) |
21 | 3, 19, 20 | mp2an 691 |
. . . . . . . . . . . 12
β’ (0 β
(0[,)(1 / 3)) β (0 β β β§ 0 β€ 0 β§ 0 < (1 /
3))) |
22 | 21 | biimpri 227 |
. . . . . . . . . . 11
β’ ((0
β β β§ 0 β€ 0 β§ 0 < (1 / 3)) β 0 β (0[,)(1 /
3))) |
23 | 22 | snssd 4774 |
. . . . . . . . . 10
β’ ((0
β β β§ 0 β€ 0 β§ 0 < (1 / 3)) β {0} β (0[,)(1
/ 3))) |
24 | 3, 5, 18, 23 | mp3an 1462 |
. . . . . . . . 9
β’ {0}
β (0[,)(1 / 3)) |
25 | | icossicc 13360 |
. . . . . . . . 9
β’ (0[,)(1 /
3)) β (0[,](1 / 3)) |
26 | 24, 25 | pm3.2i 472 |
. . . . . . . 8
β’ ({0}
β (0[,)(1 / 3)) β§ (0[,)(1 / 3)) β (0[,](1 /
3))) |
27 | | sseq2 3975 |
. . . . . . . . . 10
β’ (π = (0[,)(1 / 3)) β ({0}
β π β {0}
β (0[,)(1 / 3)))) |
28 | | sseq1 3974 |
. . . . . . . . . 10
β’ (π = (0[,)(1 / 3)) β (π β (0[,](1 / 3)) β
(0[,)(1 / 3)) β (0[,](1 / 3)))) |
29 | 27, 28 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (0[,)(1 / 3)) β (({0}
β π β§ π β (0[,](1 / 3))) β
({0} β (0[,)(1 / 3)) β§ (0[,)(1 / 3)) β (0[,](1 /
3))))) |
30 | 29 | rspcev 3584 |
. . . . . . . 8
β’ (((0[,)(1
/ 3)) β II β§ ({0} β (0[,)(1 / 3)) β§ (0[,)(1 / 3)) β
(0[,](1 / 3)))) β βπ β II ({0} β π β§ π β (0[,](1 / 3)))) |
31 | 17, 26, 30 | mp2an 691 |
. . . . . . 7
β’
βπ β II
({0} β π β§ π β (0[,](1 /
3))) |
32 | | iitop 24259 |
. . . . . . . 8
β’ II β
Top |
33 | 24, 25 | sstri 3958 |
. . . . . . . . 9
β’ {0}
β (0[,](1 / 3)) |
34 | 33, 15 | sstri 3958 |
. . . . . . . 8
β’ {0}
β (0[,]1) |
35 | | iiuni 24260 |
. . . . . . . . 9
β’ (0[,]1) =
βͺ II |
36 | 35 | isnei 22470 |
. . . . . . . 8
β’ ((II
β Top β§ {0} β (0[,]1)) β ((0[,](1 / 3)) β
((neiβII)β{0}) β ((0[,](1 / 3)) β (0[,]1) β§
βπ β II ({0}
β π β§ π β (0[,](1 /
3)))))) |
37 | 32, 34, 36 | mp2an 691 |
. . . . . . 7
β’ ((0[,](1
/ 3)) β ((neiβII)β{0}) β ((0[,](1 / 3)) β (0[,]1)
β§ βπ β II
({0} β π β§ π β (0[,](1 /
3))))) |
38 | 15, 31, 37 | mpbir2an 710 |
. . . . . 6
β’ (0[,](1 /
3)) β ((neiβII)β{0}) |
39 | 38 | a1i 11 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (0[,](1 / 3)) β
((neiβII)β{0})) |
40 | | simprl 770 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β π β (β‘π β {0})) |
41 | 2, 39, 40 | cnneiima 47023 |
. . . 4
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β (0[,](1 / 3))) β
((neiβπ½)βπ)) |
42 | | halfge0 12377 |
. . . . . . . 8
β’ 0 β€ (1
/ 2) |
43 | | 1le1 11790 |
. . . . . . . 8
β’ 1 β€
1 |
44 | | iccss 13339 |
. . . . . . . 8
β’ (((0
β β β§ 1 β β) β§ (0 β€ (1 / 2) β§ 1 β€ 1))
β ((1 / 2)[,]1) β (0[,]1)) |
45 | 3, 4, 42, 43, 44 | mp4an 692 |
. . . . . . 7
β’ ((1 /
2)[,]1) β (0[,]1) |
46 | | io1ii 47027 |
. . . . . . . . 9
β’ (0 β€
(1 / 2) β ((1 / 2)(,]1) β II) |
47 | 42, 46 | ax-mp 5 |
. . . . . . . 8
β’ ((1 /
2)(,]1) β II |
48 | | halflt1 12378 |
. . . . . . . . . 10
β’ (1 / 2)
< 1 |
49 | | halfre 12374 |
. . . . . . . . . . . . . 14
β’ (1 / 2)
β β |
50 | 49 | rexri 11220 |
. . . . . . . . . . . . 13
β’ (1 / 2)
β β* |
51 | | elioc2 13334 |
. . . . . . . . . . . . 13
β’ (((1 / 2)
β β* β§ 1 β β) β (1 β ((1 /
2)(,]1) β (1 β β β§ (1 / 2) < 1 β§ 1 β€
1))) |
52 | 50, 4, 51 | mp2an 691 |
. . . . . . . . . . . 12
β’ (1 β
((1 / 2)(,]1) β (1 β β β§ (1 / 2) < 1 β§ 1 β€
1)) |
53 | 52 | biimpri 227 |
. . . . . . . . . . 11
β’ ((1
β β β§ (1 / 2) < 1 β§ 1 β€ 1) β 1 β ((1 /
2)(,]1)) |
54 | 53 | snssd 4774 |
. . . . . . . . . 10
β’ ((1
β β β§ (1 / 2) < 1 β§ 1 β€ 1) β {1} β ((1 /
2)(,]1)) |
55 | 4, 48, 43, 54 | mp3an 1462 |
. . . . . . . . 9
β’ {1}
β ((1 / 2)(,]1) |
56 | | iocssicc 13361 |
. . . . . . . . 9
β’ ((1 /
2)(,]1) β ((1 / 2)[,]1) |
57 | 55, 56 | pm3.2i 472 |
. . . . . . . 8
β’ ({1}
β ((1 / 2)(,]1) β§ ((1 / 2)(,]1) β ((1 /
2)[,]1)) |
58 | | sseq2 3975 |
. . . . . . . . . 10
β’ (β = ((1 / 2)(,]1) β ({1}
β β β {1} β
((1 / 2)(,]1))) |
59 | | sseq1 3974 |
. . . . . . . . . 10
β’ (β = ((1 / 2)(,]1) β (β β ((1 / 2)[,]1) β ((1
/ 2)(,]1) β ((1 / 2)[,]1))) |
60 | 58, 59 | anbi12d 632 |
. . . . . . . . 9
β’ (β = ((1 / 2)(,]1) β (({1}
β β β§ β β ((1 / 2)[,]1)) β
({1} β ((1 / 2)(,]1) β§ ((1 / 2)(,]1) β ((1 /
2)[,]1)))) |
61 | 60 | rspcev 3584 |
. . . . . . . 8
β’ ((((1 /
2)(,]1) β II β§ ({1} β ((1 / 2)(,]1) β§ ((1 / 2)(,]1) β
((1 / 2)[,]1))) β ββ β II ({1} β β β§ β β ((1 / 2)[,]1))) |
62 | 47, 57, 61 | mp2an 691 |
. . . . . . 7
β’
ββ β II
({1} β β β§ β β ((1 /
2)[,]1)) |
63 | 55, 56 | sstri 3958 |
. . . . . . . . 9
β’ {1}
β ((1 / 2)[,]1) |
64 | 63, 45 | sstri 3958 |
. . . . . . . 8
β’ {1}
β (0[,]1) |
65 | 35 | isnei 22470 |
. . . . . . . 8
β’ ((II
β Top β§ {1} β (0[,]1)) β (((1 / 2)[,]1) β
((neiβII)β{1}) β (((1 / 2)[,]1) β (0[,]1) β§
ββ β II ({1}
β β β§ β β ((1 /
2)[,]1))))) |
66 | 32, 64, 65 | mp2an 691 |
. . . . . . 7
β’ (((1 /
2)[,]1) β ((neiβII)β{1}) β (((1 / 2)[,]1) β (0[,]1)
β§ ββ β II
({1} β β β§ β β ((1 /
2)[,]1)))) |
67 | 45, 62, 66 | mpbir2an 710 |
. . . . . 6
β’ ((1 /
2)[,]1) β ((neiβII)β{1}) |
68 | 67 | a1i 11 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β ((1 / 2)[,]1) β
((neiβII)β{1})) |
69 | | simprr 772 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β π β (β‘π β {1})) |
70 | 2, 68, 69 | cnneiima 47023 |
. . . 4
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β ((1 / 2)[,]1)) β
((neiβπ½)βπ)) |
71 | | icccldii 47025 |
. . . . . 6
β’ ((0 β€
0 β§ (1 / 3) β€ 1) β (0[,](1 / 3)) β
(ClsdβII)) |
72 | 5, 13, 71 | mp2an 691 |
. . . . 5
β’ (0[,](1 /
3)) β (ClsdβII) |
73 | | cnclima 22635 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (0[,](1 / 3)) β
(ClsdβII)) β (β‘π β (0[,](1 / 3))) β
(Clsdβπ½)) |
74 | 2, 72, 73 | sylancl 587 |
. . . 4
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β (0[,](1 / 3))) β
(Clsdβπ½)) |
75 | | icccldii 47025 |
. . . . . 6
β’ ((0 β€
(1 / 2) β§ 1 β€ 1) β ((1 / 2)[,]1) β
(ClsdβII)) |
76 | 42, 43, 75 | mp2an 691 |
. . . . 5
β’ ((1 /
2)[,]1) β (ClsdβII) |
77 | | cnclima 22635 |
. . . . 5
β’ ((π β (π½ Cn II) β§ ((1 / 2)[,]1) β
(ClsdβII)) β (β‘π β ((1 / 2)[,]1)) β
(Clsdβπ½)) |
78 | 2, 76, 77 | sylancl 587 |
. . . 4
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β ((1 / 2)[,]1)) β
(Clsdβπ½)) |
79 | | eqid 2737 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
80 | 79, 35 | cnf 22613 |
. . . . . . 7
β’ (π β (π½ Cn II) β π:βͺ π½βΆ(0[,]1)) |
81 | 80 | ffund 6677 |
. . . . . 6
β’ (π β (π½ Cn II) β Fun π) |
82 | 2, 81 | syl 17 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β Fun π) |
83 | | 0xr 11209 |
. . . . . . 7
β’ 0 β
β* |
84 | | 1xr 11221 |
. . . . . . 7
β’ 1 β
β* |
85 | | 2lt3 12332 |
. . . . . . . 8
β’ 2 <
3 |
86 | | 2re 12234 |
. . . . . . . . 9
β’ 2 β
β |
87 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
88 | | 3pos 12265 |
. . . . . . . . 9
β’ 0 <
3 |
89 | 86, 6, 87, 88 | ltrecii 12078 |
. . . . . . . 8
β’ (2 < 3
β (1 / 3) < (1 / 2)) |
90 | 85, 89 | mpbi 229 |
. . . . . . 7
β’ (1 / 3)
< (1 / 2) |
91 | | iccdisj2 47004 |
. . . . . . 7
β’ ((0
β β* β§ 1 β β* β§ (1 / 3)
< (1 / 2)) β ((0[,](1 / 3)) β© ((1 / 2)[,]1)) =
β
) |
92 | 83, 84, 90, 91 | mp3an 1462 |
. . . . . 6
β’ ((0[,](1
/ 3)) β© ((1 / 2)[,]1)) = β
|
93 | 92 | a1i 11 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β ((0[,](1 / 3)) β©
((1 / 2)[,]1)) = β
) |
94 | | ssidd 3972 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β (0[,](1 / 3))) β (β‘π β (0[,](1 / 3)))) |
95 | | ssidd 3972 |
. . . . 5
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β (β‘π β ((1 / 2)[,]1)) β (β‘π β ((1 / 2)[,]1))) |
96 | 82, 93, 94, 95 | predisj 46969 |
. . . 4
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β ((β‘π β (0[,](1 / 3))) β© (β‘π β ((1 / 2)[,]1))) =
β
) |
97 | | eleq1 2826 |
. . . . . 6
β’ (π = (β‘π β (0[,](1 / 3))) β (π β (Clsdβπ½) β (β‘π β (0[,](1 / 3))) β
(Clsdβπ½))) |
98 | | ineq1 4170 |
. . . . . . 7
β’ (π = (β‘π β (0[,](1 / 3))) β (π β© π) = ((β‘π β (0[,](1 / 3))) β© π)) |
99 | 98 | eqeq1d 2739 |
. . . . . 6
β’ (π = (β‘π β (0[,](1 / 3))) β ((π β© π) = β
β ((β‘π β (0[,](1 / 3))) β© π) = β
)) |
100 | 97, 99 | 3anbi13d 1439 |
. . . . 5
β’ (π = (β‘π β (0[,](1 / 3))) β ((π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β
) β ((β‘π β (0[,](1 / 3))) β
(Clsdβπ½) β§ π β (Clsdβπ½) β§ ((β‘π β (0[,](1 / 3))) β© π) = β
))) |
101 | | eleq1 2826 |
. . . . . 6
β’ (π = (β‘π β ((1 / 2)[,]1)) β (π β (Clsdβπ½) β (β‘π β ((1 / 2)[,]1)) β
(Clsdβπ½))) |
102 | | ineq2 4171 |
. . . . . . 7
β’ (π = (β‘π β ((1 / 2)[,]1)) β ((β‘π β (0[,](1 / 3))) β© π) = ((β‘π β (0[,](1 / 3))) β© (β‘π β ((1 / 2)[,]1)))) |
103 | 102 | eqeq1d 2739 |
. . . . . 6
β’ (π = (β‘π β ((1 / 2)[,]1)) β (((β‘π β (0[,](1 / 3))) β© π) = β
β ((β‘π β (0[,](1 / 3))) β© (β‘π β ((1 / 2)[,]1))) =
β
)) |
104 | 101, 103 | 3anbi23d 1440 |
. . . . 5
β’ (π = (β‘π β ((1 / 2)[,]1)) β (((β‘π β (0[,](1 / 3))) β
(Clsdβπ½) β§ π β (Clsdβπ½) β§ ((β‘π β (0[,](1 / 3))) β© π) = β
) β ((β‘π β (0[,](1 / 3))) β
(Clsdβπ½) β§ (β‘π β ((1 / 2)[,]1)) β
(Clsdβπ½) β§
((β‘π β (0[,](1 / 3))) β© (β‘π β ((1 / 2)[,]1))) =
β
))) |
105 | 100, 104 | rspc2ev 3595 |
. . . 4
β’ (((β‘π β (0[,](1 / 3))) β
((neiβπ½)βπ) β§ (β‘π β ((1 / 2)[,]1)) β
((neiβπ½)βπ) β§ ((β‘π β (0[,](1 / 3))) β
(Clsdβπ½) β§ (β‘π β ((1 / 2)[,]1)) β
(Clsdβπ½) β§
((β‘π β (0[,](1 / 3))) β© (β‘π β ((1 / 2)[,]1))) = β
)) β
βπ β
((neiβπ½)βπ)βπ β ((neiβπ½)βπ)(π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β
)) |
106 | 41, 70, 74, 78, 96, 105 | syl113anc 1383 |
. . 3
β’ ((π β (π½ Cn II) β§ (π β (β‘π β {0}) β§ π β (β‘π β {1}))) β βπ β ((neiβπ½)βπ)βπ β ((neiβπ½)βπ)(π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β
)) |
107 | 106 | rexlimiva 3145 |
. 2
β’
(βπ β
(π½ Cn II)(π β (β‘π β {0}) β§ π β (β‘π β {1})) β βπ β ((neiβπ½)βπ)βπ β ((neiβπ½)βπ)(π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β
)) |
108 | 1, 107 | syl 17 |
1
β’ (π β βπ β ((neiβπ½)βπ)βπ β ((neiβπ½)βπ)(π β (Clsdβπ½) β§ π β (Clsdβπ½) β§ (π β© π) = β
)) |