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