Step | Hyp | Ref
| Expression |
1 | | sincn 25956 |
. . . . . . . . . . 11
β’ sin
β (ββcnββ) |
2 | 1 | a1i 11 |
. . . . . . . . . 10
β’ (π β sin β
(ββcnββ)) |
3 | | ioosscn 13386 |
. . . . . . . . . . . . 13
β’ (πΆ(,)πΈ) β β |
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (πΆ(,)πΈ) β β) |
5 | | dirkercncflem4.n |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
6 | 5 | nncnd 12228 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
7 | | 1cnd 11209 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
8 | 7 | halfcld 12457 |
. . . . . . . . . . . . 13
β’ (π β (1 / 2) β
β) |
9 | 6, 8 | addcld 11233 |
. . . . . . . . . . . 12
β’ (π β (π + (1 / 2)) β β) |
10 | | ssid 4005 |
. . . . . . . . . . . . 13
β’ β
β β |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
12 | 4, 9, 11 | constcncfg 44588 |
. . . . . . . . . . 11
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (π + (1 / 2))) β ((πΆ(,)πΈ)βcnββ)) |
13 | 4, 11 | idcncfg 44589 |
. . . . . . . . . . 11
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ π¦) β ((πΆ(,)πΈ)βcnββ)) |
14 | 12, 13 | mulcncf 24963 |
. . . . . . . . . 10
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((π + (1 / 2)) Β· π¦)) β ((πΆ(,)πΈ)βcnββ)) |
15 | 2, 14 | cncfmpt1f 24430 |
. . . . . . . . 9
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (sinβ((π + (1 / 2)) Β· π¦))) β ((πΆ(,)πΈ)βcnββ)) |
16 | | 2cnd 12290 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β 2 β β) |
17 | | pirp 25971 |
. . . . . . . . . . . . . . . 16
β’ Ο
β β+ |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Ο β
β+) |
19 | 18 | rpcnd 13018 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Ο β
β) |
20 | 16, 19 | mulcld 11234 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (2 Β· Ο) β
β) |
21 | | ioossre 13385 |
. . . . . . . . . . . . . . . . . 18
β’ (πΆ(,)πΈ) β β |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΆ(,)πΈ) β β) |
23 | 22 | sselda 3983 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β π¦ β β) |
24 | 23 | recnd 11242 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β π¦ β β) |
25 | 24 | halfcld 12457 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ / 2) β β) |
26 | 25 | sincld 16073 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (sinβ(π¦ / 2)) β β) |
27 | 20, 26 | mulcld 11234 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
β) |
28 | | 2rp 12979 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β+ |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β 2 β
β+) |
30 | 29 | rpne0d 13021 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β 2 β 0) |
31 | 18 | rpne0d 13021 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Ο β 0) |
32 | 16, 19, 30, 31 | mulne0d 11866 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (2 Β· Ο) β
0) |
33 | 24, 16, 19, 30, 31 | divdiv1d 12021 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((π¦ / 2) / Ο) = (π¦ / (2 Β· Ο))) |
34 | | dirkercncflem4.c |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ πΆ = (π΄ Β· (2 Β·
Ο)) |
35 | | dirkercncflem4.a |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π΄ = (ββ(π / (2 Β·
Ο))) |
36 | 35 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ Β· (2 Β· Ο)) =
((ββ(π / (2
Β· Ο))) Β· (2 Β· Ο)) |
37 | 34, 36 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ πΆ = ((ββ(π / (2 Β· Ο))) Β·
(2 Β· Ο)) |
38 | 37 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΆ / (2 Β· Ο)) =
(((ββ(π / (2
Β· Ο))) Β· (2 Β· Ο)) / (2 Β·
Ο)) |
39 | | dirkercncflem4.y |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β β) |
40 | | 2re 12286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 2 β
β |
41 | | pire 25968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ Ο
β β |
42 | 40, 41 | remulcli 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (2
Β· Ο) β β |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (2 Β· Ο) β
β) |
44 | | 0re 11216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 0 β
β |
45 | | 2pos 12315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 0 <
2 |
46 | | pipos 25970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 0 <
Ο |
47 | 40, 41, 45, 46 | mulgt0ii 11347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 0 < (2
Β· Ο) |
48 | 44, 47 | gtneii 11326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (2
Β· Ο) β 0 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (2 Β· Ο) β
0) |
50 | 39, 43, 49 | redivcld 12042 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π / (2 Β· Ο)) β
β) |
51 | 50 | flcld 13763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (ββ(π / (2 Β· Ο))) β
β€) |
52 | 51 | zred 12666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (ββ(π / (2 Β· Ο))) β
β) |
53 | 52 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (ββ(π / (2 Β· Ο))) β
β) |
54 | 43 | recnd 11242 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (2 Β· Ο) β
β) |
55 | 53, 54, 49 | divcan4d 11996 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((ββ(π / (2 Β· Ο))) Β·
(2 Β· Ο)) / (2 Β· Ο)) = (ββ(π / (2 Β· Ο)))) |
56 | 38, 55 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΆ / (2 Β· Ο)) =
(ββ(π / (2
Β· Ο)))) |
57 | 56, 51 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΆ / (2 Β· Ο)) β
β€) |
58 | 57 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (πΆ / (2 Β· Ο)) β
β€) |
59 | 52, 43 | remulcld 11244 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((ββ(π / (2 Β· Ο))) Β·
(2 Β· Ο)) β β) |
60 | 37, 59 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΆ β β) |
61 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β πΆ β β) |
62 | 29, 18 | rpmulcld 13032 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (2 Β· Ο) β
β+) |
63 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β π¦ β (πΆ(,)πΈ)) |
64 | 60 | rexrd 11264 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΆ β
β*) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β πΆ β
β*) |
66 | 35 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(ββ(π /
(2 Β· Ο))) = π΄ |
67 | 66 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((ββ(π /
(2 Β· Ο))) + 1) = (π΄ + 1) |
68 | | dirkercncflem4.b |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ π΅ = (π΄ + 1) |
69 | 67, 68 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((ββ(π /
(2 Β· Ο))) + 1) = π΅ |
70 | 69 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((ββ(π
/ (2 Β· Ο))) + 1) Β· (2 Β· Ο)) = (π΅ Β· (2 Β·
Ο)) |
71 | | dirkercncflem4.e |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ πΈ = (π΅ Β· (2 Β·
Ο)) |
72 | 70, 71 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((ββ(π
/ (2 Β· Ο))) + 1) Β· (2 Β· Ο)) = πΈ |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (((ββ(π / (2 Β· Ο))) + 1)
Β· (2 Β· Ο)) = πΈ) |
74 | | 1red 11215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β 1 β
β) |
75 | 52, 74 | readdcld 11243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((ββ(π / (2 Β· Ο))) + 1)
β β) |
76 | 75, 43 | remulcld 11244 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (((ββ(π / (2 Β· Ο))) + 1)
Β· (2 Β· Ο)) β β) |
77 | 73, 76 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΈ β β) |
78 | 77 | rexrd 11264 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΈ β
β*) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β πΈ β
β*) |
80 | | elioo2 13365 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΆ β β*
β§ πΈ β
β*) β (π¦ β (πΆ(,)πΈ) β (π¦ β β β§ πΆ < π¦ β§ π¦ < πΈ))) |
81 | 65, 79, 80 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ β (πΆ(,)πΈ) β (π¦ β β β§ πΆ < π¦ β§ π¦ < πΈ))) |
82 | 63, 81 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ β β β§ πΆ < π¦ β§ π¦ < πΈ)) |
83 | 82 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β πΆ < π¦) |
84 | 61, 23, 62, 83 | ltdiv1dd 13073 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (πΆ / (2 Β· Ο)) < (π¦ / (2 Β·
Ο))) |
85 | 77 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β πΈ β β) |
86 | 82 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β π¦ < πΈ) |
87 | 23, 85, 62, 86 | ltdiv1dd 13073 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ / (2 Β· Ο)) < (πΈ / (2 Β· Ο))) |
88 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΆ = (π΄ Β· (2 Β·
Ο))) |
89 | 88 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (πΆ / (2 Β· Ο)) = ((π΄ Β· (2 Β· Ο)) / (2 Β·
Ο))) |
90 | 89 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πΆ / (2 Β· Ο)) + 1) = (((π΄ Β· (2 Β· Ο)) /
(2 Β· Ο)) + 1)) |
91 | 35, 53 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π΄ β β) |
92 | 91, 54, 49 | divcan4d 11996 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π΄ Β· (2 Β· Ο)) / (2 Β·
Ο)) = π΄) |
93 | 92 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((π΄ Β· (2 Β· Ο)) / (2 Β·
Ο)) + 1) = (π΄ +
1)) |
94 | 68 | oveq1i 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π΅ Β· (2 Β· Ο)) =
((π΄ + 1) Β· (2
Β· Ο)) |
95 | 71, 94 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ πΈ = ((π΄ + 1) Β· (2 Β·
Ο)) |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΈ = ((π΄ + 1) Β· (2 Β·
Ο))) |
97 | 96 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (πΈ / (2 Β· Ο)) = (((π΄ + 1) Β· (2 Β· Ο)) / (2
Β· Ο))) |
98 | 91, 7 | addcld 11233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π΄ + 1) β β) |
99 | 98, 54, 49 | divcan4d 11996 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((π΄ + 1) Β· (2 Β· Ο)) / (2
Β· Ο)) = (π΄ +
1)) |
100 | 97, 99 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΄ + 1) = (πΈ / (2 Β· Ο))) |
101 | 90, 93, 100 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΈ / (2 Β· Ο)) = ((πΆ / (2 Β· Ο)) + 1)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (πΈ / (2 Β· Ο)) = ((πΆ / (2 Β· Ο)) + 1)) |
103 | 87, 102 | breqtrd 5175 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ / (2 Β· Ο)) < ((πΆ / (2 Β· Ο)) +
1)) |
104 | | btwnnz 12638 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΆ / (2 Β· Ο)) β
β€ β§ (πΆ / (2
Β· Ο)) < (π¦ /
(2 Β· Ο)) β§ (π¦
/ (2 Β· Ο)) < ((πΆ / (2 Β· Ο)) + 1)) β Β¬
(π¦ / (2 Β· Ο))
β β€) |
105 | 58, 84, 103, 104 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ (π¦ / (2 Β· Ο)) β
β€) |
106 | 33, 105 | eqneltrd 2854 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ ((π¦ / 2) / Ο) β
β€) |
107 | | sineq0 26033 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ / 2) β β β
((sinβ(π¦ / 2)) = 0
β ((π¦ / 2) / Ο)
β β€)) |
108 | 25, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((sinβ(π¦ / 2)) = 0 β ((π¦ / 2) / Ο) β
β€)) |
109 | 106, 108 | mtbird 325 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ (sinβ(π¦ / 2)) = 0) |
110 | 109 | neqned 2948 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (sinβ(π¦ / 2)) β 0) |
111 | 20, 26, 32, 110 | mulne0d 11866 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
0) |
112 | 111 | neneqd 2946 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) =
0) |
113 | 40 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β 2 β β) |
114 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Ο β
β) |
115 | 113, 114 | remulcld 11244 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (2 Β· Ο) β
β) |
116 | 23 | rehalfcld 12459 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ / 2) β β) |
117 | 116 | resincld 16086 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (sinβ(π¦ / 2)) β β) |
118 | 115, 117 | remulcld 11244 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
β) |
119 | | elsng 4643 |
. . . . . . . . . . . . . 14
β’ (((2
Β· Ο) Β· (sinβ(π¦ / 2))) β β β (((2 Β·
Ο) Β· (sinβ(π¦ / 2))) β {0} β ((2 Β· Ο)
Β· (sinβ(π¦ /
2))) = 0)) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
{0} β ((2 Β· Ο) Β· (sinβ(π¦ / 2))) = 0)) |
121 | 112, 120 | mtbird 325 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
{0}) |
122 | 27, 121 | eldifd 3960 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
(β β {0})) |
123 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))) =
(π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))) |
124 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π β (π₯ β (β β {0}) β¦ (1 /
π₯)) = (π₯ β (β β {0}) β¦ (1 /
π₯))) |
125 | | oveq2 7417 |
. . . . . . . . . . 11
β’ (π₯ = ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) β
(1 / π₯) = (1 / ((2 Β·
Ο) Β· (sinβ(π¦ / 2))))) |
126 | 122, 123,
124, 125 | fmptco 7127 |
. . . . . . . . . 10
β’ (π β ((π₯ β (β β {0}) β¦ (1 /
π₯)) β (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))) =
(π¦ β (πΆ(,)πΈ) β¦ (1 / ((2 Β· Ο) Β·
(sinβ(π¦ /
2)))))) |
127 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))) =
(π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ /
2)))) |
128 | | 2cnd 12290 |
. . . . . . . . . . . . . . 15
β’ (π β 2 β
β) |
129 | 4, 128, 11 | constcncfg 44588 |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ 2) β ((πΆ(,)πΈ)βcnββ)) |
130 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β
β+) |
131 | 130 | rpcnd 13018 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β
β) |
132 | 4, 131, 11 | constcncfg 44588 |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ Ο) β ((πΆ(,)πΈ)βcnββ)) |
133 | 129, 132 | mulcncf 24963 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (2 Β· Ο)) β ((πΆ(,)πΈ)βcnββ)) |
134 | 24, 16, 30 | divrecd 11993 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π¦ / 2) = (π¦ Β· (1 / 2))) |
135 | 134 | mpteq2dva 5249 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (π¦ / 2)) = (π¦ β (πΆ(,)πΈ) β¦ (π¦ Β· (1 / 2)))) |
136 | 4, 8, 11 | constcncfg 44588 |
. . . . . . . . . . . . . . . 16
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (1 / 2)) β ((πΆ(,)πΈ)βcnββ)) |
137 | 13, 136 | mulcncf 24963 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (π¦ Β· (1 / 2))) β ((πΆ(,)πΈ)βcnββ)) |
138 | 135, 137 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (π¦ / 2)) β ((πΆ(,)πΈ)βcnββ)) |
139 | 2, 138 | cncfmpt1f 24430 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (sinβ(π¦ / 2))) β ((πΆ(,)πΈ)βcnββ)) |
140 | 133, 139 | mulcncf 24963 |
. . . . . . . . . . . 12
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))
β ((πΆ(,)πΈ)βcnββ)) |
141 | | ssid 4005 |
. . . . . . . . . . . . 13
β’ (πΆ(,)πΈ) β (πΆ(,)πΈ) |
142 | 141 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (πΆ(,)πΈ) β (πΆ(,)πΈ)) |
143 | | difssd 4133 |
. . . . . . . . . . . 12
β’ (π β (β β {0})
β β) |
144 | 127, 140,
142, 143, 122 | cncfmptssg 44587 |
. . . . . . . . . . 11
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))
β ((πΆ(,)πΈ)βcnβ(β β {0}))) |
145 | | ax-1cn 11168 |
. . . . . . . . . . . 12
β’ 1 β
β |
146 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π₯ β (β β {0})
β¦ (1 / π₯)) = (π₯ β (β β {0})
β¦ (1 / π₯)) |
147 | 146 | cdivcncf 24437 |
. . . . . . . . . . . 12
β’ (1 β
β β (π₯ β
(β β {0}) β¦ (1 / π₯)) β ((β β {0})βcnββ)) |
148 | 145, 147 | mp1i 13 |
. . . . . . . . . . 11
β’ (π β (π₯ β (β β {0}) β¦ (1 /
π₯)) β ((β
β {0})βcnββ)) |
149 | 144, 148 | cncfco 24423 |
. . . . . . . . . 10
β’ (π β ((π₯ β (β β {0}) β¦ (1 /
π₯)) β (π¦ β (πΆ(,)πΈ) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))))
β ((πΆ(,)πΈ)βcnββ)) |
150 | 126, 149 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ (1 / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))))
β ((πΆ(,)πΈ)βcnββ)) |
151 | 15, 150 | mulcncf 24963 |
. . . . . . . 8
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) Β· (1 / ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))))
β ((πΆ(,)πΈ)βcnββ)) |
152 | | dirkercncflem4.d |
. . . . . . . . . . . 12
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
153 | 152 | dirkerval 44807 |
. . . . . . . . . . 11
β’ (π β β β (π·βπ) = (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
154 | 5, 153 | syl 17 |
. . . . . . . . . 10
β’ (π β (π·βπ) = (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
155 | 154 | reseq1d 5981 |
. . . . . . . . 9
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)) = ((π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))))
βΎ (πΆ(,)πΈ))) |
156 | 22 | resmptd 6041 |
. . . . . . . . 9
β’ (π β ((π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))))
βΎ (πΆ(,)πΈ)) = (π¦ β (πΆ(,)πΈ) β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π¦)) / ((2
Β· Ο) Β· (sinβ(π¦ / 2))))))) |
157 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β 2 β
β+) |
158 | 157, 130 | rpmulcld 13032 |
. . . . . . . . . . . . . . 15
β’ (π β (2 Β· Ο) β
β+) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (2 Β· Ο) β
β+) |
160 | | mod0 13841 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ (2
Β· Ο) β β+) β ((π¦ mod (2 Β· Ο)) = 0 β (π¦ / (2 Β· Ο)) β
β€)) |
161 | 23, 159, 160 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((π¦ mod (2 Β· Ο)) = 0 β (π¦ / (2 Β· Ο)) β
β€)) |
162 | 105, 161 | mtbird 325 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β Β¬ (π¦ mod (2 Β· Ο)) = 0) |
163 | 162 | iffalsed 4540 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β if((π¦ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π¦)) / ((2
Β· Ο) Β· (sinβ(π¦ / 2))))) = ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))) |
164 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β π β β) |
165 | | 1cnd 11209 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β 1 β β) |
166 | 165 | halfcld 12457 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (1 / 2) β
β) |
167 | 164, 166 | addcld 11233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (π + (1 / 2)) β β) |
168 | 167, 24 | mulcld 11234 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((π + (1 / 2)) Β· π¦) β β) |
169 | 168 | sincld 16073 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β (sinβ((π + (1 / 2)) Β· π¦)) β β) |
170 | 169, 27, 111 | divrecd 11993 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))) =
((sinβ((π + (1 / 2))
Β· π¦)) Β· (1 /
((2 Β· Ο) Β· (sinβ(π¦ / 2)))))) |
171 | 163, 170 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (πΆ(,)πΈ)) β if((π¦ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π¦)) / ((2
Β· Ο) Β· (sinβ(π¦ / 2))))) = ((sinβ((π + (1 / 2)) Β· π¦)) Β· (1 / ((2 Β· Ο) Β·
(sinβ(π¦ /
2)))))) |
172 | 171 | mpteq2dva 5249 |
. . . . . . . . 9
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ if((π¦ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π¦)) / ((2
Β· Ο) Β· (sinβ(π¦ / 2)))))) = (π¦ β (πΆ(,)πΈ) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) Β· (1 / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
173 | 155, 156,
172 | 3eqtrrd 2778 |
. . . . . . . 8
β’ (π β (π¦ β (πΆ(,)πΈ) β¦ ((sinβ((π + (1 / 2)) Β· π¦)) Β· (1 / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))))) =
((π·βπ) βΎ (πΆ(,)πΈ))) |
174 | | eqid 2733 |
. . . . . . . . . 10
β’
(TopOpenββfld) =
(TopOpenββfld) |
175 | 174 | tgioo2 24319 |
. . . . . . . . . . . 12
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
176 | 175 | oveq1i 7419 |
. . . . . . . . . . 11
β’
((topGenβran (,)) βΎt (πΆ(,)πΈ)) = (((TopOpenββfld)
βΎt β) βΎt (πΆ(,)πΈ)) |
177 | 174 | cnfldtop 24300 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) β Top |
178 | | reex 11201 |
. . . . . . . . . . . 12
β’ β
β V |
179 | | restabs 22669 |
. . . . . . . . . . . 12
β’
(((TopOpenββfld) β Top β§ (πΆ(,)πΈ) β β β§ β β V)
β (((TopOpenββfld) βΎt β)
βΎt (πΆ(,)πΈ)) = ((TopOpenββfld)
βΎt (πΆ(,)πΈ))) |
180 | 177, 21, 178, 179 | mp3an 1462 |
. . . . . . . . . . 11
β’
(((TopOpenββfld) βΎt β)
βΎt (πΆ(,)πΈ)) = ((TopOpenββfld)
βΎt (πΆ(,)πΈ)) |
181 | 176, 180 | eqtri 2761 |
. . . . . . . . . 10
β’
((topGenβran (,)) βΎt (πΆ(,)πΈ)) = ((TopOpenββfld)
βΎt (πΆ(,)πΈ)) |
182 | | unicntop 24302 |
. . . . . . . . . . . . 13
β’ β =
βͺ
(TopOpenββfld) |
183 | 182 | restid 17379 |
. . . . . . . . . . . 12
β’
((TopOpenββfld) β Top β
((TopOpenββfld) βΎt β) =
(TopOpenββfld)) |
184 | 177, 183 | ax-mp 5 |
. . . . . . . . . . 11
β’
((TopOpenββfld) βΎt β) =
(TopOpenββfld) |
185 | 184 | eqcomi 2742 |
. . . . . . . . . 10
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
186 | 174, 181,
185 | cncfcn 24426 |
. . . . . . . . 9
β’ (((πΆ(,)πΈ) β β β§ β β
β) β ((πΆ(,)πΈ)βcnββ) = (((topGenβran (,))
βΎt (πΆ(,)πΈ)) Cn
(TopOpenββfld))) |
187 | 4, 11, 186 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((πΆ(,)πΈ)βcnββ) = (((topGenβran (,))
βΎt (πΆ(,)πΈ)) Cn
(TopOpenββfld))) |
188 | 151, 173,
187 | 3eltr3d 2848 |
. . . . . . 7
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)) β (((topGenβran (,))
βΎt (πΆ(,)πΈ)) Cn
(TopOpenββfld))) |
189 | | retopon 24280 |
. . . . . . . . . 10
β’
(topGenβran (,)) β (TopOnββ) |
190 | 189 | a1i 11 |
. . . . . . . . 9
β’ (π β (topGenβran (,))
β (TopOnββ)) |
191 | | resttopon 22665 |
. . . . . . . . 9
β’
(((topGenβran (,)) β (TopOnββ) β§ (πΆ(,)πΈ) β β) β ((topGenβran
(,)) βΎt (πΆ(,)πΈ)) β (TopOnβ(πΆ(,)πΈ))) |
192 | 190, 22, 191 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((topGenβran (,))
βΎt (πΆ(,)πΈ)) β (TopOnβ(πΆ(,)πΈ))) |
193 | 174 | cnfldtopon 24299 |
. . . . . . . . 9
β’
(TopOpenββfld) β
(TopOnββ) |
194 | 193 | a1i 11 |
. . . . . . . 8
β’ (π β
(TopOpenββfld) β
(TopOnββ)) |
195 | | cncnp 22784 |
. . . . . . . 8
β’
((((topGenβran (,)) βΎt (πΆ(,)πΈ)) β (TopOnβ(πΆ(,)πΈ)) β§
(TopOpenββfld) β (TopOnββ)) β
(((π·βπ) βΎ (πΆ(,)πΈ)) β (((topGenβran (,))
βΎt (πΆ(,)πΈ)) Cn (TopOpenββfld))
β (((π·βπ) βΎ (πΆ(,)πΈ)):(πΆ(,)πΈ)βΆβ β§ βπ¦ β (πΆ(,)πΈ)((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦)))) |
196 | 192, 194,
195 | syl2anc 585 |
. . . . . . 7
β’ (π β (((π·βπ) βΎ (πΆ(,)πΈ)) β (((topGenβran (,))
βΎt (πΆ(,)πΈ)) Cn (TopOpenββfld))
β (((π·βπ) βΎ (πΆ(,)πΈ)):(πΆ(,)πΈ)βΆβ β§ βπ¦ β (πΆ(,)πΈ)((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦)))) |
197 | 188, 196 | mpbid 231 |
. . . . . 6
β’ (π β (((π·βπ) βΎ (πΆ(,)πΈ)):(πΆ(,)πΈ)βΆβ β§ βπ¦ β (πΆ(,)πΈ)((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦))) |
198 | 197 | simprd 497 |
. . . . 5
β’ (π β βπ¦ β (πΆ(,)πΈ)((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦)) |
199 | | dirkercncflem4.ymod0 |
. . . . . . . . . . . 12
β’ (π β (π mod (2 Β· Ο)) β
0) |
200 | 199 | neneqd 2946 |
. . . . . . . . . . 11
β’ (π β Β¬ (π mod (2 Β· Ο)) =
0) |
201 | | mod0 13841 |
. . . . . . . . . . . 12
β’ ((π β β β§ (2
Β· Ο) β β+) β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
202 | 39, 158, 201 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((π mod (2 Β· Ο)) = 0 β (π / (2 Β· Ο)) β
β€)) |
203 | 200, 202 | mtbid 324 |
. . . . . . . . . 10
β’ (π β Β¬ (π / (2 Β· Ο)) β
β€) |
204 | | flltnz 13776 |
. . . . . . . . . 10
β’ (((π / (2 Β· Ο)) β
β β§ Β¬ (π / (2
Β· Ο)) β β€) β (ββ(π / (2 Β· Ο))) < (π / (2 Β·
Ο))) |
205 | 50, 203, 204 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (ββ(π / (2 Β· Ο))) <
(π / (2 Β·
Ο))) |
206 | 52, 50, 158, 205 | ltmul1dd 13071 |
. . . . . . . 8
β’ (π β ((ββ(π / (2 Β· Ο))) Β·
(2 Β· Ο)) < ((π
/ (2 Β· Ο)) Β· (2 Β· Ο))) |
207 | 39 | recnd 11242 |
. . . . . . . . 9
β’ (π β π β β) |
208 | 207, 54, 49 | divcan1d 11991 |
. . . . . . . 8
β’ (π β ((π / (2 Β· Ο)) Β· (2 Β·
Ο)) = π) |
209 | 206, 208 | breqtrd 5175 |
. . . . . . 7
β’ (π β ((ββ(π / (2 Β· Ο))) Β·
(2 Β· Ο)) < π) |
210 | 37, 209 | eqbrtrid 5184 |
. . . . . 6
β’ (π β πΆ < π) |
211 | | fllelt 13762 |
. . . . . . . . . 10
β’ ((π / (2 Β· Ο)) β
β β ((ββ(π / (2 Β· Ο))) β€ (π / (2 Β· Ο)) β§
(π / (2 Β· Ο))
< ((ββ(π /
(2 Β· Ο))) + 1))) |
212 | 50, 211 | syl 17 |
. . . . . . . . 9
β’ (π β ((ββ(π / (2 Β· Ο))) β€
(π / (2 Β· Ο))
β§ (π / (2 Β·
Ο)) < ((ββ(π / (2 Β· Ο))) +
1))) |
213 | 212 | simprd 497 |
. . . . . . . 8
β’ (π β (π / (2 Β· Ο)) <
((ββ(π / (2
Β· Ο))) + 1)) |
214 | 50, 75, 158, 213 | ltmul1dd 13071 |
. . . . . . 7
β’ (π β ((π / (2 Β· Ο)) Β· (2 Β·
Ο)) < (((ββ(π / (2 Β· Ο))) + 1) Β· (2
Β· Ο))) |
215 | 214, 208,
73 | 3brtr3d 5180 |
. . . . . 6
β’ (π β π < πΈ) |
216 | 64, 78, 39, 210, 215 | eliood 44211 |
. . . . 5
β’ (π β π β (πΆ(,)πΈ)) |
217 | | fveq2 6892 |
. . . . . . 7
β’ (π¦ = π β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦) = ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ)) |
218 | 217 | eleq2d 2820 |
. . . . . 6
β’ (π¦ = π β (((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ))) |
219 | 218 | rspccva 3612 |
. . . . 5
β’
((βπ¦ β
(πΆ(,)πΈ)((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ¦) β§ π β (πΆ(,)πΈ)) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ)) |
220 | 198, 216,
219 | syl2anc 585 |
. . . 4
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ)) |
221 | 177 | a1i 11 |
. . . . 5
β’ (π β
(TopOpenββfld) β Top) |
222 | 152 | dirkerf 44813 |
. . . . . . 7
β’ (π β β β (π·βπ):ββΆβ) |
223 | 5, 222 | syl 17 |
. . . . . 6
β’ (π β (π·βπ):ββΆβ) |
224 | 223, 22 | fssresd 6759 |
. . . . 5
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)):(πΆ(,)πΈ)βΆβ) |
225 | | ax-resscn 11167 |
. . . . . 6
β’ β
β β |
226 | 225 | a1i 11 |
. . . . 5
β’ (π β β β
β) |
227 | | retop 24278 |
. . . . . . 7
β’
(topGenβran (,)) β Top |
228 | | uniretop 24279 |
. . . . . . . 8
β’ β =
βͺ (topGenβran (,)) |
229 | 228 | restuni 22666 |
. . . . . . 7
β’
(((topGenβran (,)) β Top β§ (πΆ(,)πΈ) β β) β (πΆ(,)πΈ) = βͺ
((topGenβran (,)) βΎt (πΆ(,)πΈ))) |
230 | 227, 21, 229 | mp2an 691 |
. . . . . 6
β’ (πΆ(,)πΈ) = βͺ
((topGenβran (,)) βΎt (πΆ(,)πΈ)) |
231 | 230, 182 | cnprest2 22794 |
. . . . 5
β’
(((TopOpenββfld) β Top β§ ((π·βπ) βΎ (πΆ(,)πΈ)):(πΆ(,)πΈ)βΆβ β§ β β
β) β (((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
((TopOpenββfld) βΎt
β))βπ))) |
232 | 221, 224,
226, 231 | syl3anc 1372 |
. . . 4
β’ (π β (((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
(TopOpenββfld))βπ) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
((TopOpenββfld) βΎt
β))βπ))) |
233 | 220, 232 | mpbid 231 |
. . 3
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
((TopOpenββfld) βΎt
β))βπ)) |
234 | 175 | eqcomi 2742 |
. . . . . 6
β’
((TopOpenββfld) βΎt β) =
(topGenβran (,)) |
235 | 234 | a1i 11 |
. . . . 5
β’ (π β
((TopOpenββfld) βΎt β) =
(topGenβran (,))) |
236 | 235 | oveq2d 7425 |
. . . 4
β’ (π β (((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
((TopOpenββfld) βΎt β)) =
(((topGenβran (,)) βΎt (πΆ(,)πΈ)) CnP (topGenβran
(,)))) |
237 | 236 | fveq1d 6894 |
. . 3
β’ (π β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP
((TopOpenββfld) βΎt
β))βπ) =
((((topGenβran (,)) βΎt (πΆ(,)πΈ)) CnP (topGenβran (,)))βπ)) |
238 | 233, 237 | eleqtrd 2836 |
. 2
β’ (π β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP (topGenβran (,)))βπ)) |
239 | 227 | a1i 11 |
. . 3
β’ (π β (topGenβran (,))
β Top) |
240 | | iooretop 24282 |
. . . . . . 7
β’ (πΆ(,)πΈ) β (topGenβran
(,)) |
241 | 228 | isopn3 22570 |
. . . . . . 7
β’
(((topGenβran (,)) β Top β§ (πΆ(,)πΈ) β β) β ((πΆ(,)πΈ) β (topGenβran (,)) β
((intβ(topGenβran (,)))β(πΆ(,)πΈ)) = (πΆ(,)πΈ))) |
242 | 240, 241 | mpbii 232 |
. . . . . 6
β’
(((topGenβran (,)) β Top β§ (πΆ(,)πΈ) β β) β
((intβ(topGenβran (,)))β(πΆ(,)πΈ)) = (πΆ(,)πΈ)) |
243 | 239, 22, 242 | syl2anc 585 |
. . . . 5
β’ (π β
((intβ(topGenβran (,)))β(πΆ(,)πΈ)) = (πΆ(,)πΈ)) |
244 | 243 | eqcomd 2739 |
. . . 4
β’ (π β (πΆ(,)πΈ) = ((intβ(topGenβran
(,)))β(πΆ(,)πΈ))) |
245 | 216, 244 | eleqtrd 2836 |
. . 3
β’ (π β π β ((intβ(topGenβran
(,)))β(πΆ(,)πΈ))) |
246 | 228, 228 | cnprest 22793 |
. . 3
β’
((((topGenβran (,)) β Top β§ (πΆ(,)πΈ) β β) β§ (π β ((intβ(topGenβran
(,)))β(πΆ(,)πΈ)) β§ (π·βπ):ββΆβ)) β ((π·βπ) β (((topGenβran (,)) CnP
(topGenβran (,)))βπ) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP (topGenβran (,)))βπ))) |
247 | 239, 22, 245, 223, 246 | syl22anc 838 |
. 2
β’ (π β ((π·βπ) β (((topGenβran (,)) CnP
(topGenβran (,)))βπ) β ((π·βπ) βΎ (πΆ(,)πΈ)) β ((((topGenβran (,))
βΎt (πΆ(,)πΈ)) CnP (topGenβran (,)))βπ))) |
248 | 238, 247 | mpbird 257 |
1
β’ (π β (π·βπ) β (((topGenβran (,)) CnP
(topGenβran (,)))βπ)) |