Step | Hyp | Ref
| Expression |
1 | | dirkercncflem3.d |
. . 3
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
2 | | oveq2 7366 |
. . . . 5
β’ (π€ = π¦ β ((π + (1 / 2)) Β· π€) = ((π + (1 / 2)) Β· π¦)) |
3 | 2 | fveq2d 6847 |
. . . 4
β’ (π€ = π¦ β (sinβ((π + (1 / 2)) Β· π€)) = (sinβ((π + (1 / 2)) Β· π¦))) |
4 | 3 | cbvmptv 5219 |
. . 3
β’ (π€ β ((π΄(,)π΅) β {π}) β¦ (sinβ((π + (1 / 2)) Β· π€))) = (π¦ β ((π΄(,)π΅) β {π}) β¦ (sinβ((π + (1 / 2)) Β· π¦))) |
5 | | fvoveq1 7381 |
. . . . 5
β’ (π€ = π¦ β (sinβ(π€ / 2)) = (sinβ(π¦ / 2))) |
6 | 5 | oveq2d 7374 |
. . . 4
β’ (π€ = π¦ β ((2 Β· Ο) Β·
(sinβ(π€ / 2))) = ((2
Β· Ο) Β· (sinβ(π¦ / 2)))) |
7 | 6 | cbvmptv 5219 |
. . 3
β’ (π€ β ((π΄(,)π΅) β {π}) β¦ ((2 Β· Ο) Β·
(sinβ(π€ / 2)))) =
(π¦ β ((π΄(,)π΅) β {π}) β¦ ((2 Β· Ο) Β·
(sinβ(π¦ /
2)))) |
8 | | dirkercncflem3.a |
. . . . . . . 8
β’ π΄ = (π β Ο) |
9 | | dirkercncflem3.b |
. . . . . . . 8
β’ π΅ = (π + Ο) |
10 | | dirkercncflem3.yr |
. . . . . . . 8
β’ (π β π β β) |
11 | | dirkercncflem3.yod |
. . . . . . . 8
β’ (π β (π mod (2 Β· Ο)) =
0) |
12 | 8, 9, 10, 11 | dirkercncflem1 44430 |
. . . . . . 7
β’ (π β (π β (π΄(,)π΅) β§ βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β
0))) |
13 | 12 | simprd 497 |
. . . . . 6
β’ (π β βπ¦ β ((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0)) |
14 | | r19.26 3111 |
. . . . . 6
β’
(βπ¦ β
((π΄(,)π΅) β {π})((sinβ(π¦ / 2)) β 0 β§ (cosβ(π¦ / 2)) β 0) β
(βπ¦ β ((π΄(,)π΅) β {π})(sinβ(π¦ / 2)) β 0 β§ βπ¦ β ((π΄(,)π΅) β {π})(cosβ(π¦ / 2)) β 0)) |
15 | 13, 14 | sylib 217 |
. . . . 5
β’ (π β (βπ¦ β ((π΄(,)π΅) β {π})(sinβ(π¦ / 2)) β 0 β§ βπ¦ β ((π΄(,)π΅) β {π})(cosβ(π¦ / 2)) β 0)) |
16 | 15 | simpld 496 |
. . . 4
β’ (π β βπ¦ β ((π΄(,)π΅) β {π})(sinβ(π¦ / 2)) β 0) |
17 | 16 | r19.21bi 3233 |
. . 3
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (sinβ(π¦ / 2)) β 0) |
18 | 2 | fveq2d 6847 |
. . . . 5
β’ (π€ = π¦ β (cosβ((π + (1 / 2)) Β· π€)) = (cosβ((π + (1 / 2)) Β· π¦))) |
19 | 18 | oveq2d 7374 |
. . . 4
β’ (π€ = π¦ β ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π€))) = ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π¦)))) |
20 | 19 | cbvmptv 5219 |
. . 3
β’ (π€ β ((π΄(,)π΅) β {π}) β¦ ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π€)))) = (π¦ β ((π΄(,)π΅) β {π}) β¦ ((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π¦)))) |
21 | | fvoveq1 7381 |
. . . . 5
β’ (π€ = π¦ β (cosβ(π€ / 2)) = (cosβ(π¦ / 2))) |
22 | 21 | oveq2d 7374 |
. . . 4
β’ (π€ = π¦ β (Ο Β· (cosβ(π€ / 2))) = (Ο Β·
(cosβ(π¦ /
2)))) |
23 | 22 | cbvmptv 5219 |
. . 3
β’ (π€ β ((π΄(,)π΅) β {π}) β¦ (Ο Β· (cosβ(π€ / 2)))) = (π¦ β ((π΄(,)π΅) β {π}) β¦ (Ο Β· (cosβ(π¦ / 2)))) |
24 | | eqid 2733 |
. . 3
β’ (π§ β (π΄(,)π΅) β¦ (((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π§))) / (Ο Β·
(cosβ(π§ / 2))))) =
(π§ β (π΄(,)π΅) β¦ (((π + (1 / 2)) Β· (cosβ((π + (1 / 2)) Β· π§))) / (Ο Β·
(cosβ(π§ /
2))))) |
25 | | dirkercncflem3.n |
. . 3
β’ (π β π β β) |
26 | 12 | simpld 496 |
. . 3
β’ (π β π β (π΄(,)π΅)) |
27 | 15 | simprd 497 |
. . . 4
β’ (π β βπ¦ β ((π΄(,)π΅) β {π})(cosβ(π¦ / 2)) β 0) |
28 | 27 | r19.21bi 3233 |
. . 3
β’ ((π β§ π¦ β ((π΄(,)π΅) β {π})) β (cosβ(π¦ / 2)) β 0) |
29 | 1, 4, 7, 17, 20, 23, 24, 25, 26, 11, 28 | dirkercncflem2 44431 |
. 2
β’ (π β ((π·βπ)βπ) β (((π·βπ) βΎ ((π΄(,)π΅) β {π})) limβ π)) |
30 | 1 | dirkerf 44424 |
. . . . 5
β’ (π β β β (π·βπ):ββΆβ) |
31 | 25, 30 | syl 17 |
. . . 4
β’ (π β (π·βπ):ββΆβ) |
32 | | ax-resscn 11113 |
. . . . 5
β’ β
β β |
33 | 32 | a1i 11 |
. . . 4
β’ (π β β β
β) |
34 | 31, 33 | fssd 6687 |
. . 3
β’ (π β (π·βπ):ββΆβ) |
35 | | ioossre 13331 |
. . . . 5
β’ (π΄(,)π΅) β β |
36 | 35 | a1i 11 |
. . . 4
β’ (π β (π΄(,)π΅) β β) |
37 | 36 | ssdifssd 4103 |
. . 3
β’ (π β ((π΄(,)π΅) β {π}) β β) |
38 | | eqid 2733 |
. . 3
β’
(TopOpenββfld) =
(TopOpenββfld) |
39 | | eqid 2733 |
. . 3
β’
((TopOpenββfld) βΎt (β
βͺ {π})) =
((TopOpenββfld) βΎt (β βͺ
{π})) |
40 | | iooretop 24145 |
. . . . . . 7
β’ (π΄(,)π΅) β (topGenβran
(,)) |
41 | | retop 24141 |
. . . . . . . 8
β’
(topGenβran (,)) β Top |
42 | | uniretop 24142 |
. . . . . . . . 9
β’ β =
βͺ (topGenβran (,)) |
43 | 42 | isopn3 22433 |
. . . . . . . 8
β’
(((topGenβran (,)) β Top β§ (π΄(,)π΅) β β) β ((π΄(,)π΅) β (topGenβran (,)) β
((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅))) |
44 | 41, 36, 43 | sylancr 588 |
. . . . . . 7
β’ (π β ((π΄(,)π΅) β (topGenβran (,)) β
((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅))) |
45 | 40, 44 | mpbii 232 |
. . . . . 6
β’ (π β
((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅)) |
46 | 26, 45 | eleqtrrd 2837 |
. . . . 5
β’ (π β π β ((intβ(topGenβran
(,)))β(π΄(,)π΅))) |
47 | 38 | tgioo2 24182 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
48 | 47 | a1i 11 |
. . . . . . 7
β’ (π β (topGenβran (,)) =
((TopOpenββfld) βΎt
β)) |
49 | 48 | fveq2d 6847 |
. . . . . 6
β’ (π β
(intβ(topGenβran (,))) =
(intβ((TopOpenββfld) βΎt
β))) |
50 | 49 | fveq1d 6845 |
. . . . 5
β’ (π β
((intβ(topGenβran (,)))β(π΄(,)π΅)) =
((intβ((TopOpenββfld) βΎt
β))β(π΄(,)π΅))) |
51 | 46, 50 | eleqtrd 2836 |
. . . 4
β’ (π β π β
((intβ((TopOpenββfld) βΎt
β))β(π΄(,)π΅))) |
52 | 10 | snssd 4770 |
. . . . . . . 8
β’ (π β {π} β β) |
53 | | ssequn2 4144 |
. . . . . . . 8
β’ ({π} β β β
(β βͺ {π}) =
β) |
54 | 52, 53 | sylib 217 |
. . . . . . 7
β’ (π β (β βͺ {π}) = β) |
55 | 54 | oveq2d 7374 |
. . . . . 6
β’ (π β
((TopOpenββfld) βΎt (β βͺ
{π})) =
((TopOpenββfld) βΎt
β)) |
56 | 55 | fveq2d 6847 |
. . . . 5
β’ (π β
(intβ((TopOpenββfld) βΎt (β
βͺ {π}))) =
(intβ((TopOpenββfld) βΎt
β))) |
57 | | uncom 4114 |
. . . . . 6
β’ (((π΄(,)π΅) β {π}) βͺ {π}) = ({π} βͺ ((π΄(,)π΅) β {π})) |
58 | 26 | snssd 4770 |
. . . . . . 7
β’ (π β {π} β (π΄(,)π΅)) |
59 | | undif 4442 |
. . . . . . 7
β’ ({π} β (π΄(,)π΅) β ({π} βͺ ((π΄(,)π΅) β {π})) = (π΄(,)π΅)) |
60 | 58, 59 | sylib 217 |
. . . . . 6
β’ (π β ({π} βͺ ((π΄(,)π΅) β {π})) = (π΄(,)π΅)) |
61 | 57, 60 | eqtrid 2785 |
. . . . 5
β’ (π β (((π΄(,)π΅) β {π}) βͺ {π}) = (π΄(,)π΅)) |
62 | 56, 61 | fveq12d 6850 |
. . . 4
β’ (π β
((intβ((TopOpenββfld) βΎt (β
βͺ {π})))β(((π΄(,)π΅) β {π}) βͺ {π})) =
((intβ((TopOpenββfld) βΎt
β))β(π΄(,)π΅))) |
63 | 51, 62 | eleqtrrd 2837 |
. . 3
β’ (π β π β
((intβ((TopOpenββfld) βΎt (β
βͺ {π})))β(((π΄(,)π΅) β {π}) βͺ {π}))) |
64 | 34, 37, 33, 38, 39, 63 | limcres 25266 |
. 2
β’ (π β (((π·βπ) βΎ ((π΄(,)π΅) β {π})) limβ π) = ((π·βπ) limβ π)) |
65 | 29, 64 | eleqtrd 2836 |
1
β’ (π β ((π·βπ)βπ) β ((π·βπ) limβ π)) |