Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . . . . 9
β’ (π§ = π€ β ([,]βπ§) = ([,]βπ€)) |
2 | 1 | sseq1d 3980 |
. . . . . . . 8
β’ (π§ = π€ β (([,]βπ§) β π΄ β ([,]βπ€) β π΄)) |
3 | 2 | elrab 3650 |
. . . . . . 7
β’ (π€ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β (π€ β ran πΉ β§ ([,]βπ€) β π΄)) |
4 | | simprr 772 |
. . . . . . . 8
β’ ((π΄ β (topGenβran (,))
β§ (π€ β ran πΉ β§ ([,]βπ€) β π΄)) β ([,]βπ€) β π΄) |
5 | | fvex 6860 |
. . . . . . . . 9
β’
([,]βπ€) β
V |
6 | 5 | elpw 4569 |
. . . . . . . 8
β’
(([,]βπ€)
β π« π΄ β
([,]βπ€) β π΄) |
7 | 4, 6 | sylibr 233 |
. . . . . . 7
β’ ((π΄ β (topGenβran (,))
β§ (π€ β ran πΉ β§ ([,]βπ€) β π΄)) β ([,]βπ€) β π« π΄) |
8 | 3, 7 | sylan2b 595 |
. . . . . 6
β’ ((π΄ β (topGenβran (,))
β§ π€ β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β ([,]βπ€) β π« π΄) |
9 | 8 | ralrimiva 3144 |
. . . . 5
β’ (π΄ β (topGenβran (,))
β βπ€ β
{π§ β ran πΉ β£ ([,]βπ§) β π΄} ([,]βπ€) β π« π΄) |
10 | | iccf 13372 |
. . . . . . 7
β’
[,]:(β* Γ β*)βΆπ«
β* |
11 | | ffun 6676 |
. . . . . . 7
β’
([,]:(β* Γ β*)βΆπ«
β* β Fun [,]) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
β’ Fun
[,] |
13 | | ssrab2 4042 |
. . . . . . . 8
β’ {π§ β ran πΉ β£ ([,]βπ§) β π΄} β ran πΉ |
14 | | dyadmbl.1 |
. . . . . . . . . . 11
β’ πΉ = (π₯ β β€, π¦ β β0 β¦
β¨(π₯ / (2βπ¦)), ((π₯ + 1) / (2βπ¦))β©) |
15 | 14 | dyadf 24971 |
. . . . . . . . . 10
β’ πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ
β)) |
16 | | frn 6680 |
. . . . . . . . . 10
β’ (πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ β)) β ran
πΉ β ( β€ β©
(β Γ β))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
β’ ran πΉ β ( β€ β© (β
Γ β)) |
18 | | inss2 4194 |
. . . . . . . . . 10
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
19 | | rexpssxrxp 11207 |
. . . . . . . . . 10
β’ (β
Γ β) β (β* Γ
β*) |
20 | 18, 19 | sstri 3958 |
. . . . . . . . 9
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
21 | 17, 20 | sstri 3958 |
. . . . . . . 8
β’ ran πΉ β (β*
Γ β*) |
22 | 13, 21 | sstri 3958 |
. . . . . . 7
β’ {π§ β ran πΉ β£ ([,]βπ§) β π΄} β (β* Γ
β*) |
23 | 10 | fdmi 6685 |
. . . . . . 7
β’ dom [,] =
(β* Γ β*) |
24 | 22, 23 | sseqtrri 3986 |
. . . . . 6
β’ {π§ β ran πΉ β£ ([,]βπ§) β π΄} β dom [,] |
25 | | funimass4 6912 |
. . . . . 6
β’ ((Fun [,]
β§ {π§ β ran πΉ β£ ([,]βπ§) β π΄} β dom [,]) β (([,] β
{π§ β ran πΉ β£ ([,]βπ§) β π΄}) β π« π΄ β βπ€ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} ([,]βπ€) β π« π΄)) |
26 | 12, 24, 25 | mp2an 691 |
. . . . 5
β’ (([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β π« π΄ β βπ€ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} ([,]βπ€) β π« π΄) |
27 | 9, 26 | sylibr 233 |
. . . 4
β’ (π΄ β (topGenβran (,))
β ([,] β {π§
β ran πΉ β£
([,]βπ§) β π΄}) β π« π΄) |
28 | | sspwuni 5065 |
. . . 4
β’ (([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β π« π΄ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β π΄) |
29 | 27, 28 | sylib 217 |
. . 3
β’ (π΄ β (topGenβran (,))
β βͺ ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β π΄) |
30 | | eqid 2737 |
. . . . . 6
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
31 | 30 | rexmet 24170 |
. . . . 5
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
32 | | eqid 2737 |
. . . . . . 7
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
33 | 30, 32 | tgioo 24175 |
. . . . . 6
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
34 | 33 | mopni2 23865 |
. . . . 5
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ π΄ β (topGenβran (,)) β§ π€ β π΄) β βπ β β+ (π€(ballβ((abs β
β ) βΎ (β Γ β)))π) β π΄) |
35 | 31, 34 | mp3an1 1449 |
. . . 4
β’ ((π΄ β (topGenβran (,))
β§ π€ β π΄) β βπ β β+
(π€(ballβ((abs β
β ) βΎ (β Γ β)))π) β π΄) |
36 | | elssuni 4903 |
. . . . . . . . . 10
β’ (π΄ β (topGenβran (,))
β π΄ β βͺ (topGenβran (,))) |
37 | | uniretop 24142 |
. . . . . . . . . 10
β’ β =
βͺ (topGenβran (,)) |
38 | 36, 37 | sseqtrrdi 4000 |
. . . . . . . . 9
β’ (π΄ β (topGenβran (,))
β π΄ β
β) |
39 | 38 | sselda 3949 |
. . . . . . . 8
β’ ((π΄ β (topGenβran (,))
β§ π€ β π΄) β π€ β β) |
40 | | rpre 12930 |
. . . . . . . 8
β’ (π β β+
β π β
β) |
41 | 30 | bl2ioo 24171 |
. . . . . . . 8
β’ ((π€ β β β§ π β β) β (π€(ballβ((abs β
β ) βΎ (β Γ β)))π) = ((π€ β π)(,)(π€ + π))) |
42 | 39, 40, 41 | syl2an 597 |
. . . . . . 7
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ π β β+) β (π€(ballβ((abs β
β ) βΎ (β Γ β)))π) = ((π€ β π)(,)(π€ + π))) |
43 | 42 | sseq1d 3980 |
. . . . . 6
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ π β β+) β ((π€(ballβ((abs β
β ) βΎ (β Γ β)))π) β π΄ β ((π€ β π)(,)(π€ + π)) β π΄)) |
44 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
45 | | 1lt2 12331 |
. . . . . . . . . 10
β’ 1 <
2 |
46 | | expnlbnd 14143 |
. . . . . . . . . 10
β’ ((π β β+
β§ 2 β β β§ 1 < 2) β βπ β β (1 / (2βπ)) < π) |
47 | 44, 45, 46 | mp3an23 1454 |
. . . . . . . . 9
β’ (π β β+
β βπ β
β (1 / (2βπ))
< π) |
48 | 47 | ad2antrl 727 |
. . . . . . . 8
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β βπ β β (1 / (2βπ)) < π) |
49 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ β β) |
50 | | 2nn 12233 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
51 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β0) |
52 | 51 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π β β0) |
53 | | nnexpcl 13987 |
. . . . . . . . . . . . . . . . 17
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
54 | 50, 52, 53 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (2βπ) β β) |
55 | 54 | nnred 12175 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (2βπ) β β) |
56 | 49, 55 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ Β· (2βπ)) β β) |
57 | | fllelt 13709 |
. . . . . . . . . . . . . 14
β’ ((π€ Β· (2βπ)) β β β
((ββ(π€ Β·
(2βπ))) β€ (π€ Β· (2βπ)) β§ (π€ Β· (2βπ)) < ((ββ(π€ Β· (2βπ))) + 1))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ))) β€ (π€ Β· (2βπ)) β§ (π€ Β· (2βπ)) < ((ββ(π€ Β· (2βπ))) + 1))) |
59 | 58 | simpld 496 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (ββ(π€ Β· (2βπ))) β€ (π€ Β· (2βπ))) |
60 | | reflcl 13708 |
. . . . . . . . . . . . . 14
β’ ((π€ Β· (2βπ)) β β β
(ββ(π€ Β·
(2βπ))) β
β) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (ββ(π€ Β· (2βπ))) β β) |
62 | 54 | nngt0d 12209 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β 0 < (2βπ)) |
63 | | ledivmul2 12041 |
. . . . . . . . . . . . 13
β’
(((ββ(π€
Β· (2βπ)))
β β β§ π€
β β β§ ((2βπ) β β β§ 0 < (2βπ))) β
(((ββ(π€
Β· (2βπ))) /
(2βπ)) β€ π€ β (ββ(π€ Β· (2βπ))) β€ (π€ Β· (2βπ)))) |
64 | 61, 49, 55, 62, 63 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) / (2βπ)) β€ π€ β (ββ(π€ Β· (2βπ))) β€ (π€ Β· (2βπ)))) |
65 | 59, 64 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ))) / (2βπ)) β€ π€) |
66 | | peano2re 11335 |
. . . . . . . . . . . . . 14
β’
((ββ(π€
Β· (2βπ)))
β β β ((ββ(π€ Β· (2βπ))) + 1) β β) |
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ))) + 1) β β) |
68 | 67, 54 | nndivred 12214 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) β
β) |
69 | 58 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ Β· (2βπ)) < ((ββ(π€ Β· (2βπ))) + 1)) |
70 | | ltmuldiv 12035 |
. . . . . . . . . . . . . 14
β’ ((π€ β β β§
((ββ(π€ Β·
(2βπ))) + 1) β
β β§ ((2βπ)
β β β§ 0 < (2βπ))) β ((π€ Β· (2βπ)) < ((ββ(π€ Β· (2βπ))) + 1) β π€ < (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)))) |
71 | 49, 67, 55, 62, 70 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((π€ Β· (2βπ)) < ((ββ(π€ Β· (2βπ))) + 1) β π€ < (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)))) |
72 | 69, 71 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ < (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) |
73 | 49, 68, 72 | ltled 11310 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ β€ (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) |
74 | 61, 54 | nndivred 12214 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ))) / (2βπ)) β β) |
75 | | elicc2 13336 |
. . . . . . . . . . . 12
β’
((((ββ(π€
Β· (2βπ))) /
(2βπ)) β β
β§ (((ββ(π€
Β· (2βπ))) + 1)
/ (2βπ)) β
β) β (π€ β
(((ββ(π€
Β· (2βπ))) /
(2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) β (π€ β β β§ ((ββ(π€ Β· (2βπ))) / (2βπ)) β€ π€ β§ π€ β€ (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))))) |
76 | 74, 68, 75 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ β (((ββ(π€ Β· (2βπ))) / (2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) β (π€ β β β§ ((ββ(π€ Β· (2βπ))) / (2βπ)) β€ π€ β§ π€ β€ (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))))) |
77 | 49, 65, 73, 76 | mpbir3and 1343 |
. . . . . . . . . 10
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ β (((ββ(π€ Β· (2βπ))) / (2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ)))) |
78 | 56 | flcld 13710 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (ββ(π€ Β· (2βπ))) β β€) |
79 | 14 | dyadval 24972 |
. . . . . . . . . . . . 13
β’
(((ββ(π€
Β· (2βπ)))
β β€ β§ π
β β0) β ((ββ(π€ Β· (2βπ)))πΉπ) = β¨((ββ(π€ Β· (2βπ))) / (2βπ)), (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))β©) |
80 | 78, 52, 79 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ)))πΉπ) = β¨((ββ(π€ Β· (2βπ))) / (2βπ)), (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))β©) |
81 | 80 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) = ([,]ββ¨((ββ(π€ Β· (2βπ))) / (2βπ)), (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))β©)) |
82 | | df-ov 7365 |
. . . . . . . . . . 11
β’
(((ββ(π€
Β· (2βπ))) /
(2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) = ([,]ββ¨((ββ(π€ Β· (2βπ))) / (2βπ)), (((ββ(π€ Β· (2βπ))) + 1) / (2βπ))β©) |
83 | 81, 82 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) = (((ββ(π€ Β· (2βπ))) / (2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ)))) |
84 | 77, 83 | eleqtrrd 2841 |
. . . . . . . . 9
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ β ([,]β((ββ(π€ Β· (2βπ)))πΉπ))) |
85 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π§ = ((ββ(π€ Β· (2βπ)))πΉπ) β ([,]βπ§) = ([,]β((ββ(π€ Β· (2βπ)))πΉπ))) |
86 | 85 | sseq1d 3980 |
. . . . . . . . . . 11
β’ (π§ = ((ββ(π€ Β· (2βπ)))πΉπ) β (([,]βπ§) β π΄ β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β π΄)) |
87 | | ffn 6673 |
. . . . . . . . . . . . 13
β’ (πΉ:(β€ Γ
β0)βΆ( β€ β© (β Γ β)) β
πΉ Fn (β€ Γ
β0)) |
88 | 15, 87 | ax-mp 5 |
. . . . . . . . . . . 12
β’ πΉ Fn (β€ Γ
β0) |
89 | | fnovrn 7534 |
. . . . . . . . . . . 12
β’ ((πΉ Fn (β€ Γ
β0) β§ (ββ(π€ Β· (2βπ))) β β€ β§ π β β0) β
((ββ(π€ Β·
(2βπ)))πΉπ) β ran πΉ) |
90 | 88, 78, 52, 89 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ)))πΉπ) β ran πΉ) |
91 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π β β+) |
92 | 91 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π β β) |
93 | 49, 92 | resubcld 11590 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ β π) β β) |
94 | 93 | rexrd 11212 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ β π) β
β*) |
95 | 49, 92 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ + π) β β) |
96 | 95 | rexrd 11212 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ + π) β
β*) |
97 | 74, 92 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) / (2βπ)) + π) β β) |
98 | 61 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (ββ(π€ Β· (2βπ))) β β) |
99 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β 1 β β) |
100 | 55 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (2βπ) β β) |
101 | 54 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (2βπ) β 0) |
102 | 98, 99, 100, 101 | divdird 11976 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) = (((ββ(π€ Β· (2βπ))) / (2βπ)) + (1 / (2βπ)))) |
103 | 54 | nnrecred 12211 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (1 / (2βπ)) β β) |
104 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (1 / (2βπ)) < π) |
105 | 103, 92, 74, 104 | ltadd2dd 11321 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) / (2βπ)) + (1 / (2βπ))) < (((ββ(π€ Β· (2βπ))) / (2βπ)) + π)) |
106 | 102, 105 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) < (((ββ(π€ Β· (2βπ))) / (2βπ)) + π)) |
107 | 49, 68, 97, 72, 106 | lttrd 11323 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ < (((ββ(π€ Β· (2βπ))) / (2βπ)) + π)) |
108 | 49, 92, 74 | ltsubaddd 11758 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((π€ β π) < ((ββ(π€ Β· (2βπ))) / (2βπ)) β π€ < (((ββ(π€ Β· (2βπ))) / (2βπ)) + π))) |
109 | 107, 108 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ β π) < ((ββ(π€ Β· (2βπ))) / (2βπ))) |
110 | 49, 103 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ + (1 / (2βπ))) β β) |
111 | 74, 49, 103, 65 | leadd1dd 11776 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) / (2βπ)) + (1 / (2βπ))) β€ (π€ + (1 / (2βπ)))) |
112 | 102, 111 | eqbrtrd 5132 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) β€ (π€ + (1 / (2βπ)))) |
113 | 103, 92, 49, 104 | ltadd2dd 11321 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (π€ + (1 / (2βπ))) < (π€ + π)) |
114 | 68, 110, 95, 112, 113 | lelttrd 11320 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) < (π€ + π)) |
115 | | iccssioo 13340 |
. . . . . . . . . . . . . 14
β’ ((((π€ β π) β β* β§ (π€ + π) β β*) β§ ((π€ β π) < ((ββ(π€ Β· (2βπ))) / (2βπ)) β§ (((ββ(π€ Β· (2βπ))) + 1) / (2βπ)) < (π€ + π))) β (((ββ(π€ Β· (2βπ))) / (2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) β ((π€ β π)(,)(π€ + π))) |
116 | 94, 96, 109, 114, 115 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β (((ββ(π€ Β· (2βπ))) / (2βπ))[,](((ββ(π€ Β· (2βπ))) + 1) / (2βπ))) β ((π€ β π)(,)(π€ + π))) |
117 | 83, 116 | eqsstrd 3987 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β ((π€ β π)(,)(π€ + π))) |
118 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((π€ β π)(,)(π€ + π)) β π΄) |
119 | 117, 118 | sstrd 3959 |
. . . . . . . . . . 11
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β π΄) |
120 | 86, 90, 119 | elrabd 3652 |
. . . . . . . . . 10
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ((ββ(π€ Β· (2βπ)))πΉπ) β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) |
121 | | funfvima2 7186 |
. . . . . . . . . . 11
β’ ((Fun [,]
β§ {π§ β ran πΉ β£ ([,]βπ§) β π΄} β dom [,]) β
(((ββ(π€
Β· (2βπ)))πΉπ) β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄}))) |
122 | 12, 24, 121 | mp2an 691 |
. . . . . . . . . 10
β’
(((ββ(π€
Β· (2βπ)))πΉπ) β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
123 | 120, 122 | syl 17 |
. . . . . . . . 9
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
124 | | elunii 4875 |
. . . . . . . . 9
β’ ((π€ β
([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β§ ([,]β((ββ(π€ Β· (2βπ)))πΉπ)) β ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
125 | 84, 123, 124 | syl2anc 585 |
. . . . . . . 8
β’ ((((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β§ (π β β β§ (1 / (2βπ)) < π)) β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
126 | 48, 125 | rexlimddv 3159 |
. . . . . . 7
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ (π β β+ β§ ((π€ β π)(,)(π€ + π)) β π΄)) β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
127 | 126 | expr 458 |
. . . . . 6
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ π β β+) β (((π€ β π)(,)(π€ + π)) β π΄ β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}))) |
128 | 43, 127 | sylbid 239 |
. . . . 5
β’ (((π΄ β (topGenβran (,))
β§ π€ β π΄) β§ π β β+) β ((π€(ballβ((abs β
β ) βΎ (β Γ β)))π) β π΄ β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}))) |
129 | 128 | rexlimdva 3153 |
. . . 4
β’ ((π΄ β (topGenβran (,))
β§ π€ β π΄) β (βπ β β+
(π€(ballβ((abs β
β ) βΎ (β Γ β)))π) β π΄ β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄}))) |
130 | 35, 129 | mpd 15 |
. . 3
β’ ((π΄ β (topGenβran (,))
β§ π€ β π΄) β π€ β βͺ ([,]
β {π§ β ran πΉ β£ ([,]βπ§) β π΄})) |
131 | 29, 130 | eqelssd 3970 |
. 2
β’ (π΄ β (topGenβran (,))
β βͺ ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) = π΄) |
132 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β ([,]βπ) = ([,]βπ)) |
133 | 132 | sseq1d 3980 |
. . . . . 6
β’ (π = π β (([,]βπ) β ([,]βπ) β ([,]βπ) β ([,]βπ))) |
134 | | equequ1 2029 |
. . . . . 6
β’ (π = π β (π = π β π = π)) |
135 | 133, 134 | imbi12d 345 |
. . . . 5
β’ (π = π β ((([,]βπ) β ([,]βπ) β π = π) β (([,]βπ) β ([,]βπ) β π = π))) |
136 | 135 | ralbidv 3175 |
. . . 4
β’ (π = π β (βπ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} (([,]βπ) β ([,]βπ) β π = π) β βπ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} (([,]βπ) β ([,]βπ) β π = π))) |
137 | 136 | cbvrabv 3420 |
. . 3
β’ {π β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β£ βπ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} (([,]βπ) β ([,]βπ) β π = π)} = {π β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β£ βπ β {π§ β ran πΉ β£ ([,]βπ§) β π΄} (([,]βπ) β ([,]βπ) β π = π)} |
138 | 13 | a1i 11 |
. . 3
β’ (π΄ β (topGenβran (,))
β {π§ β ran πΉ β£ ([,]βπ§) β π΄} β ran πΉ) |
139 | 14, 137, 138 | dyadmbl 24980 |
. 2
β’ (π΄ β (topGenβran (,))
β βͺ ([,] β {π§ β ran πΉ β£ ([,]βπ§) β π΄}) β dom vol) |
140 | 131, 139 | eqeltrrd 2839 |
1
β’ (π΄ β (topGenβran (,))
β π΄ β dom
vol) |