Step | Hyp | Ref
| Expression |
1 | | ptrecube.r |
. . . 4
β’ π
=
(βtβ((1...π) Γ {(topGenβran
(,))})) |
2 | | fzfi 13884 |
. . . . 5
β’
(1...π) β
Fin |
3 | | retop 24141 |
. . . . . 6
β’
(topGenβran (,)) β Top |
4 | | fnconstg 6735 |
. . . . . 6
β’
((topGenβran (,)) β Top β ((1...π) Γ {(topGenβran (,))}) Fn
(1...π)) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
β’
((1...π) Γ
{(topGenβran (,))}) Fn (1...π) |
6 | | eqid 2737 |
. . . . . 6
β’ {π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} = {π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} |
7 | 6 | ptval 22937 |
. . . . 5
β’
(((1...π) β Fin
β§ ((1...π) Γ
{(topGenβran (,))}) Fn (1...π)) β
(βtβ((1...π) Γ {(topGenβran (,))})) =
(topGenβ{π₯ β£
ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))})) |
8 | 2, 5, 7 | mp2an 691 |
. . . 4
β’
(βtβ((1...π) Γ {(topGenβran (,))})) =
(topGenβ{π₯ β£
ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))}) |
9 | 1, 8 | eqtri 2765 |
. . 3
β’ π
= (topGenβ{π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))}) |
10 | 9 | eleq2i 2830 |
. 2
β’ (π β π
β π β (topGenβ{π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))})) |
11 | | tg2 22331 |
. . 3
β’ ((π β (topGenβ{π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))}) β§ π β π) β βπ§ β {π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} (π β π§ β§ π§ β π)) |
12 | 6 | elpt 22939 |
. . . . 5
β’ (π§ β {π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} β βπ((π Fn (1...π) β§ βπ β (1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ§ β Fin
βπ β
((1...π) β π§)(πβπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π§ = Xπ β
(1...π)(πβπ))) |
13 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’
(topGenβran (,)) β V |
14 | 13 | fvconst2 7158 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (((1...π) Γ {(topGenβran
(,))})βπ) =
(topGenβran (,))) |
15 | 14 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β ((πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β
(πβπ) β (topGenβran
(,)))) |
16 | 15 | ralbiia 3095 |
. . . . . . . . . . . 12
β’
(βπ β
(1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β
βπ β (1...π)(πβπ) β (topGenβran
(,))) |
17 | | elixp2 8846 |
. . . . . . . . . . . . . 14
β’ (π β Xπ β
(1...π)(πβπ) β (π β V β§ π Fn (1...π) β§ βπ β (1...π)(πβπ) β (πβπ))) |
18 | 17 | simp3bi 1148 |
. . . . . . . . . . . . 13
β’ (π β Xπ β
(1...π)(πβπ) β βπ β (1...π)(πβπ) β (πβπ)) |
19 | | r19.26 3115 |
. . . . . . . . . . . . . 14
β’
(βπ β
(1...π)((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β (βπ β (1...π)(πβπ) β (topGenβran (,)) β§
βπ β (1...π)(πβπ) β (πβπ))) |
20 | | uniretop 24142 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
βͺ (topGenβran (,)) |
21 | 20 | eltopss 22272 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((topGenβran (,)) β Top β§ (πβπ) β (topGenβran (,))) β
(πβπ) β β) |
22 | 3, 21 | mpan 689 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) β (topGenβran (,)) β (πβπ) β β) |
23 | 22 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β (πβπ) β β) |
24 | | ptrecube.d |
. . . . . . . . . . . . . . . . . . . 20
β’ π· = ((abs β β )
βΎ (β Γ β)) |
25 | 24 | rexmet 24170 |
. . . . . . . . . . . . . . . . . . 19
β’ π· β
(βMetββ) |
26 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
27 | 24, 26 | tgioo 24175 |
. . . . . . . . . . . . . . . . . . . 20
β’
(topGenβran (,)) = (MetOpenβπ·) |
28 | 27 | mopni2 23865 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β
(βMetββ) β§ (πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β βπ¦ β β+ ((πβπ)(ballβπ·)π¦) β (πβπ)) |
29 | 25, 28 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β βπ¦ β β+ ((πβπ)(ballβπ·)π¦) β (πβπ)) |
30 | | r19.42v 3188 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ¦ β
β+ ((πβπ) β β β§ ((πβπ)(ballβπ·)π¦) β (πβπ)) β ((πβπ) β β β§ βπ¦ β β+
((πβπ)(ballβπ·)π¦) β (πβπ))) |
31 | 23, 29, 30 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β βπ¦ β β+ ((πβπ) β β β§ ((πβπ)(ballβπ·)π¦) β (πβπ))) |
32 | 31 | ralimi 3087 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(1...π)((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β βπ β (1...π)βπ¦ β β+ ((πβπ) β β β§ ((πβπ)(ballβπ·)π¦) β (πβπ))) |
33 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (ββπ) β ((πβπ)(ballβπ·)π¦) = ((πβπ)(ballβπ·)(ββπ))) |
34 | 33 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (ββπ) β (((πβπ)(ballβπ·)π¦) β (πβπ) β ((πβπ)(ballβπ·)(ββπ)) β (πβπ))) |
35 | 34 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (ββπ) β (((πβπ) β β β§ ((πβπ)(ballβπ·)π¦) β (πβπ)) β ((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ)))) |
36 | 35 | ac6sfi 9238 |
. . . . . . . . . . . . . . . 16
β’
(((1...π) β Fin
β§ βπ β
(1...π)βπ¦ β β+
((πβπ) β β β§ ((πβπ)(ballβπ·)π¦) β (πβπ))) β ββ(β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ)))) |
37 | 2, 32, 36 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(1...π)((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β ββ(β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ)))) |
38 | | 1rp 12926 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β+ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((β:(1...π)βΆβ+ β§
(1...π) = β
) β 1
β β+) |
40 | | frn 6680 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β:(1...π)βΆβ+ β ran
β β
β+) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
ran β β
β+) |
42 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β:(1...π)βΆβ+ β β Fn (1...π)) |
43 | | fnfi 9132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((β Fn (1...π) β§ (1...π) β Fin) β β β Fin) |
44 | 42, 2, 43 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β:(1...π)βΆβ+ β β β Fin) |
45 | | rnfi 9286 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β β Fin β ran β β Fin) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β:(1...π)βΆβ+ β ran
β β
Fin) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
ran β β
Fin) |
48 | | dm0rn0 5885 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (dom
β = β
β ran β = β
) |
49 | | fdm 6682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (β:(1...π)βΆβ+ β dom
β = (1...π)) |
50 | 49 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (β:(1...π)βΆβ+ β (dom
β = β
β
(1...π) =
β
)) |
51 | 48, 50 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β:(1...π)βΆβ+ β (ran
β = β
β
(1...π) =
β
)) |
52 | 51 | necon3abid 2981 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β:(1...π)βΆβ+ β (ran
β β β
β Β¬
(1...π) =
β
)) |
53 | 52 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
ran β β
β
) |
54 | | rpssre 12929 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β+ β β |
55 | 40, 54 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β:(1...π)βΆβ+ β ran
β β
β) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
ran β β
β) |
57 | | ltso 11242 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ < Or
β |
58 | | fiinfcl 9444 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (( <
Or β β§ (ran β
β Fin β§ ran β β
β
β§ ran β β
β)) β inf(ran β,
β, < ) β ran β) |
59 | 57, 58 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((ran
β β Fin β§ ran β β β
β§ ran β β β) β inf(ran
β, β, < ) β
ran β) |
60 | 47, 53, 56, 59 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
inf(ran β, β, < )
β ran β) |
61 | 41, 60 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . 19
β’ ((β:(1...π)βΆβ+ β§ Β¬
(1...π) = β
) β
inf(ran β, β, < )
β β+) |
62 | 39, 61 | ifclda 4526 |
. . . . . . . . . . . . . . . . . 18
β’ (β:(1...π)βΆβ+ β
if((1...π) = β
, 1,
inf(ran β, β, < ))
β β+) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ))) β if((1...π) = β
, 1, inf(ran β, β, < )) β
β+) |
64 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β if((1...π) = β
, 1, inf(ran β, β, < )) β
β+) |
65 | 64 | rpxrd 12965 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β if((1...π) = β
, 1, inf(ran β, β, < )) β
β*) |
66 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β (ββπ) β
β+) |
67 | 66 | rpxrd 12965 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β (ββπ) β
β*) |
68 | | ne0i 4299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...π) β (1...π) β β
) |
69 | | ifnefalse 4503 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((1...π) β
β
β if((1...π) =
β
, 1, inf(ran β,
β, < )) = inf(ran β, β, < )) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β if((1...π) = β
, 1, inf(ran β, β, < )) = inf(ran β, β, <
)) |
71 | 70 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β if((1...π) = β
, 1, inf(ran β, β, < )) = inf(ran β, β, <
)) |
72 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β ran β β β) |
73 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
β |
74 | | rpge0 12935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β β+
β 0 β€ π¦) |
75 | 74 | rgen 3067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
βπ¦ β
β+ 0 β€ π¦ |
76 | | ssralv 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (ran
β β
β+ β (βπ¦ β β+ 0 β€ π¦ β βπ¦ β ran β0 β€ π¦)) |
77 | 40, 75, 76 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β:(1...π)βΆβ+ β
βπ¦ β ran β0 β€ π¦) |
78 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π₯ = 0 β (π₯ β€ π¦ β 0 β€ π¦)) |
79 | 78 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ = 0 β (βπ¦ β ran β π₯ β€ π¦ β βπ¦ β ran β0 β€ π¦)) |
80 | 79 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((0
β β β§ βπ¦ β ran β0 β€ π¦) β βπ₯ β β βπ¦ β ran β π₯ β€ π¦) |
81 | 73, 77, 80 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (β:(1...π)βΆβ+ β
βπ₯ β β
βπ¦ β ran β π₯ β€ π¦) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β βπ₯ β β βπ¦ β ran β π₯ β€ π¦) |
83 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((β Fn (1...π) β§ π β (1...π)) β (ββπ) β ran β) |
84 | 42, 83 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β (ββπ) β ran β) |
85 | | infrelb 12147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((ran
β β β β§
βπ₯ β β
βπ¦ β ran β π₯ β€ π¦ β§ (ββπ) β ran β) β inf(ran β, β, < ) β€ (ββπ)) |
86 | 72, 82, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β inf(ran β, β, < ) β€ (ββπ)) |
87 | 71, 86 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β if((1...π) = β
, 1, inf(ran β, β, < )) β€ (ββπ)) |
88 | 65, 67, 87 | jca31 516 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β ((if((1...π) = β
, 1, inf(ran β, β, < )) β β*
β§ (ββπ) β β*)
β§ if((1...π) = β
,
1, inf(ran β, β, <
)) β€ (ββπ))) |
89 | | ssbl 23792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π· β
(βMetββ) β§ (πβπ) β β) β§ (if((1...π) = β
, 1, inf(ran β, β, < )) β
β* β§ (ββπ) β β*) β§
if((1...π) = β
, 1,
inf(ran β, β, < ))
β€ (ββπ)) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ))) |
90 | 89 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π· β
(βMetββ) β§ (πβπ) β β) β§ ((if((1...π) = β
, 1, inf(ran β, β, < )) β
β* β§ (ββπ) β β*) β§
if((1...π) = β
, 1,
inf(ran β, β, < ))
β€ (ββπ))) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ))) |
91 | 25, 90 | mpanl1 699 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ) β β β§ ((if((1...π) = β
, 1, inf(ran β, β, < )) β
β* β§ (ββπ) β β*) β§
if((1...π) = β
, 1,
inf(ran β, β, < ))
β€ (ββπ))) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ))) |
92 | 91 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((if((1...π) =
β
, 1, inf(ran β,
β, < )) β β* β§ (ββπ) β β*) β§
if((1...π) = β
, 1,
inf(ran β, β, < ))
β€ (ββπ)) β§ (πβπ) β β) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ))) |
93 | 88, 92 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((β:(1...π)βΆβ+ β§ π β (1...π)) β§ (πβπ) β β) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ))) |
94 | | sstr2 3956 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β ((πβπ)(ballβπ·)(ββπ)) β (((πβπ)(ballβπ·)(ββπ)) β (πβπ) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((β:(1...π)βΆβ+ β§ π β (1...π)) β§ (πβπ) β β) β (((πβπ)(ballβπ·)(ββπ)) β (πβπ) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
96 | 95 | expimpd 455 |
. . . . . . . . . . . . . . . . . . 19
β’ ((β:(1...π)βΆβ+ β§ π β (1...π)) β (((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ)) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
97 | 96 | ralimdva 3165 |
. . . . . . . . . . . . . . . . . 18
β’ (β:(1...π)βΆβ+ β
(βπ β
(1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ)) β βπ β (1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
98 | 97 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ ((β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ))) β βπ β (1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ)) |
99 | 24 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(ballβπ·) =
(ballβ((abs β β ) βΎ (β Γ
β))) |
100 | 99 | oveqi 7375 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) = ((πβπ)(ballβ((abs β β ) βΎ
(β Γ β)))if((1...π) = β
, 1, inf(ran β, β, < ))) |
101 | 100 | sseq1i 3977 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ) β ((πβπ)(ballβ((abs β β ) βΎ
(β Γ β)))if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ)) |
102 | 101 | ralbii 3097 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
(1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ) β βπ β (1...π)((πβπ)(ballβ((abs β β ) βΎ
(β Γ β)))if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ)) |
103 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβπ β (1...π)((πβπ)(ballβ((abs β β ) βΎ
(β Γ β)))if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ) |
104 | 102, 103 | nfxfr 1856 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβπ β (1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ) |
105 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = if((1...π) = β
, 1, inf(ran β, β, < )) β ((πβπ)(ballβπ·)π) = ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < )))) |
106 | 105 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = if((1...π) = β
, 1, inf(ran β, β, < )) β (((πβπ)(ballβπ·)π) β (πβπ) β ((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
107 | 106 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . 18
β’ (π = if((1...π) = β
, 1, inf(ran β, β, < )) β (βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ) β βπ β (1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ))) |
108 | 104, 107 | rspce 3573 |
. . . . . . . . . . . . . . . . 17
β’
((if((1...π) =
β
, 1, inf(ran β,
β, < )) β β+ β§ βπ β (1...π)((πβπ)(ballβπ·)if((1...π) = β
, 1, inf(ran β, β, < ))) β (πβπ)) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
109 | 63, 98, 108 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ))) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
110 | 109 | exlimiv 1934 |
. . . . . . . . . . . . . . 15
β’
(ββ(β:(1...π)βΆβ+ β§
βπ β (1...π)((πβπ) β β β§ ((πβπ)(ballβπ·)(ββπ)) β (πβπ))) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
111 | 37, 110 | syl 17 |
. . . . . . . . . . . . . 14
β’
(βπ β
(1...π)((πβπ) β (topGenβran (,)) β§ (πβπ) β (πβπ)) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
112 | 19, 111 | sylbir 234 |
. . . . . . . . . . . . 13
β’
((βπ β
(1...π)(πβπ) β (topGenβran (,)) β§
βπ β (1...π)(πβπ) β (πβπ)) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
113 | 18, 112 | sylan2 594 |
. . . . . . . . . . . 12
β’
((βπ β
(1...π)(πβπ) β (topGenβran (,)) β§ π β Xπ β
(1...π)(πβπ)) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
114 | 16, 113 | sylanb 582 |
. . . . . . . . . . 11
β’
((βπ β
(1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§ π β Xπ β
(1...π)(πβπ)) β βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ)) |
115 | | sstr2 3956 |
. . . . . . . . . . . . 13
β’ (Xπ β
(1...π)((πβπ)(ballβπ·)π) β Xπ β (1...π)(πβπ) β (Xπ β (1...π)(πβπ) β π β Xπ β (1...π)((πβπ)(ballβπ·)π) β π)) |
116 | | ss2ixp 8855 |
. . . . . . . . . . . . 13
β’
(βπ β
(1...π)((πβπ)(ballβπ·)π) β (πβπ) β Xπ β (1...π)((πβπ)(ballβπ·)π) β Xπ β (1...π)(πβπ)) |
117 | 115, 116 | syl11 33 |
. . . . . . . . . . . 12
β’ (Xπ β
(1...π)(πβπ) β π β (βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ) β Xπ β (1...π)((πβπ)(ballβπ·)π) β π)) |
118 | 117 | reximdv 3168 |
. . . . . . . . . . 11
β’ (Xπ β
(1...π)(πβπ) β π β (βπ β β+ βπ β (1...π)((πβπ)(ballβπ·)π) β (πβπ) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
119 | 114, 118 | syl5com 31 |
. . . . . . . . . 10
β’
((βπ β
(1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§ π β Xπ β
(1...π)(πβπ)) β (Xπ β (1...π)(πβπ) β π β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
120 | 119 | expimpd 455 |
. . . . . . . . 9
β’
(βπ β
(1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β
((π β Xπ β
(1...π)(πβπ) β§ Xπ β (1...π)(πβπ) β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
121 | | eleq2 2827 |
. . . . . . . . . . 11
β’ (π§ = Xπ β (1...π)(πβπ) β (π β π§ β π β Xπ β (1...π)(πβπ))) |
122 | | sseq1 3974 |
. . . . . . . . . . 11
β’ (π§ = Xπ β (1...π)(πβπ) β (π§ β π β Xπ β (1...π)(πβπ) β π)) |
123 | 121, 122 | anbi12d 632 |
. . . . . . . . . 10
β’ (π§ = Xπ β (1...π)(πβπ) β ((π β π§ β§ π§ β π) β (π β Xπ β (1...π)(πβπ) β§ Xπ β (1...π)(πβπ) β π))) |
124 | 123 | imbi1d 342 |
. . . . . . . . 9
β’ (π§ = Xπ β (1...π)(πβπ) β (((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π) β ((π β Xπ β (1...π)(πβπ) β§ Xπ β (1...π)(πβπ) β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π))) |
125 | 120, 124 | syl5ibrcom 247 |
. . . . . . . 8
β’
(βπ β
(1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β
(π§ = Xπ β
(1...π)(πβπ) β ((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π))) |
126 | 125 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π Fn (1...π) β§ βπ β (1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ§ β Fin
βπ β
((1...π) β π§)(πβπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β
(π§ = Xπ β
(1...π)(πβπ) β ((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π))) |
127 | 126 | imp 408 |
. . . . . 6
β’ (((π Fn (1...π) β§ βπ β (1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ§ β Fin
βπ β
((1...π) β π§)(πβπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π§ = Xπ β
(1...π)(πβπ)) β ((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
128 | 127 | exlimiv 1934 |
. . . . 5
β’
(βπ((π Fn (1...π) β§ βπ β (1...π)(πβπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ§ β Fin
βπ β
((1...π) β π§)(πβπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π§ = Xπ β
(1...π)(πβπ)) β ((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
129 | 12, 128 | sylbi 216 |
. . . 4
β’ (π§ β {π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} β ((π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π)) |
130 | 129 | rexlimiv 3146 |
. . 3
β’
(βπ§ β
{π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))} (π β π§ β§ π§ β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π) |
131 | 11, 130 | syl 17 |
. 2
β’ ((π β (topGenβ{π₯ β£ ββ((β Fn (1...π) β§ βπ β (1...π)(ββπ) β (((1...π) Γ {(topGenβran
(,))})βπ) β§
βπ€ β Fin
βπ β
((1...π) β π€)(ββπ) = βͺ (((1...π) Γ {(topGenβran
(,))})βπ)) β§
π₯ = Xπ β
(1...π)(ββπ))}) β§ π β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π) |
132 | 10, 131 | sylanb 582 |
1
β’ ((π β π
β§ π β π) β βπ β β+ Xπ β
(1...π)((πβπ)(ballβπ·)π) β π) |