Step | Hyp | Ref
| Expression |
1 | | bndmet 36290 |
. . 3
β’ (π β (Bndβπ) β π β (Metβπ)) |
2 | | 0re 11165 |
. . . . . 6
β’ 0 β
β |
3 | 2 | ne0ii 4301 |
. . . . 5
β’ β
β β
|
4 | | metf 23706 |
. . . . . . . . . 10
β’ (π β (Metβπ) β π:(π Γ π)βΆβ) |
5 | 4 | ffnd 6673 |
. . . . . . . . 9
β’ (π β (Metβπ) β π Fn (π Γ π)) |
6 | 1, 5 | syl 17 |
. . . . . . . 8
β’ (π β (Bndβπ) β π Fn (π Γ π)) |
7 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β π Fn (π Γ π)) |
8 | 1, 4 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (Bndβπ) β π:(π Γ π)βΆβ) |
9 | 8 | fdmd 6683 |
. . . . . . . . . . 11
β’ (π β (Bndβπ) β dom π = (π Γ π)) |
10 | | xpeq2 5658 |
. . . . . . . . . . . 12
β’ (π = β
β (π Γ π) = (π Γ β
)) |
11 | | xp0 6114 |
. . . . . . . . . . . 12
β’ (π Γ β
) =
β
|
12 | 10, 11 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π = β
β (π Γ π) = β
) |
13 | 9, 12 | sylan9eq 2793 |
. . . . . . . . . 10
β’ ((π β (Bndβπ) β§ π = β
) β dom π = β
) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β dom π = β
) |
15 | | dm0rn0 5884 |
. . . . . . . . 9
β’ (dom
π = β
β ran
π =
β
) |
16 | 14, 15 | sylib 217 |
. . . . . . . 8
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β ran π = β
) |
17 | | 0ss 4360 |
. . . . . . . 8
β’ β
β (0[,]π₯) |
18 | 16, 17 | eqsstrdi 4002 |
. . . . . . 7
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β ran π β (0[,]π₯)) |
19 | | df-f 6504 |
. . . . . . 7
β’ (π:(π Γ π)βΆ(0[,]π₯) β (π Fn (π Γ π) β§ ran π β (0[,]π₯))) |
20 | 7, 18, 19 | sylanbrc 584 |
. . . . . 6
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β π:(π Γ π)βΆ(0[,]π₯)) |
21 | 20 | ralrimiva 3140 |
. . . . 5
β’ ((π β (Bndβπ) β§ π = β
) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
22 | | r19.2z 4456 |
. . . . 5
β’ ((β
β β
β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
23 | 3, 21, 22 | sylancr 588 |
. . . 4
β’ ((π β (Bndβπ) β§ π = β
) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
24 | | isbnd2 36292 |
. . . . . 6
β’ ((π β (Bndβπ) β§ π β β
) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
25 | 24 | simprbi 498 |
. . . . 5
β’ ((π β (Bndβπ) β§ π β β
) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)) |
26 | | 2re 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
27 | | simprlr 779 |
. . . . . . . . . . . 12
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π β β+) |
28 | 27 | rpred 12965 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π β β) |
29 | | remulcl 11144 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
30 | 26, 28, 29 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β (2 Β· π) β β) |
31 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π Fn (π Γ π)) |
32 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β (Metβπ)) |
33 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π₯ β π) |
34 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π§ β π) |
35 | | metcl 23708 |
. . . . . . . . . . . . . 14
β’ ((π β (Metβπ) β§ π₯ β π β§ π§ β π) β (π₯ππ§) β β) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β β) |
37 | | metge0 23721 |
. . . . . . . . . . . . . 14
β’ ((π β (Metβπ) β§ π₯ β π β§ π§ β π) β 0 β€ (π₯ππ§)) |
38 | 32, 33, 34, 37 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β 0 β€ (π₯ππ§)) |
39 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (2 Β· π) β β) |
40 | | simprll 778 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π¦ β π) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π¦ β π) |
42 | | metcl 23708 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (Metβπ) β§ π¦ β π β§ π₯ β π) β (π¦ππ₯) β β) |
43 | 32, 41, 33, 42 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ₯) β β) |
44 | | metcl 23708 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (Metβπ) β§ π¦ β π β§ π§ β π) β (π¦ππ§) β β) |
45 | 32, 41, 34, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ§) β β) |
46 | 43, 45 | readdcld 11192 |
. . . . . . . . . . . . . . 15
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) β β) |
47 | | mettri2 23717 |
. . . . . . . . . . . . . . . 16
β’ ((π β (Metβπ) β§ (π¦ β π β§ π₯ β π β§ π§ β π)) β (π₯ππ§) β€ ((π¦ππ₯) + (π¦ππ§))) |
48 | 32, 41, 33, 34, 47 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β€ ((π¦ππ₯) + (π¦ππ§))) |
49 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β β) |
50 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π = (π¦(ballβπ)π)) |
51 | 33, 50 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π₯ β (π¦(ballβπ)π)) |
52 | | metxmet 23710 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Metβπ) β π β (βMetβπ)) |
53 | 32, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β (βMetβπ)) |
54 | | rpxr 12932 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β π β
β*) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π)) β π β β*) |
56 | 55 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β β*) |
57 | | elbl2 23766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (βMetβπ) β§ π β β*) β§ (π¦ β π β§ π₯ β π)) β (π₯ β (π¦(ballβπ)π) β (π¦ππ₯) < π)) |
58 | 53, 56, 41, 33, 57 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ β (π¦(ballβπ)π) β (π¦ππ₯) < π)) |
59 | 51, 58 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ₯) < π) |
60 | 34, 50 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π§ β (π¦(ballβπ)π)) |
61 | | elbl2 23766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (βMetβπ) β§ π β β*) β§ (π¦ β π β§ π§ β π)) β (π§ β (π¦(ballβπ)π) β (π¦ππ§) < π)) |
62 | 53, 56, 41, 34, 61 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π§ β (π¦(ballβπ)π) β (π¦ππ§) < π)) |
63 | 60, 62 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ§) < π) |
64 | 43, 45, 49, 49, 59, 63 | lt2addd 11786 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) < (π + π)) |
65 | 49 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β β) |
66 | 65 | 2timesd 12404 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (2 Β· π) = (π + π)) |
67 | 64, 66 | breqtrrd 5137 |
. . . . . . . . . . . . . . 15
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) < (2 Β· π)) |
68 | 36, 46, 39, 48, 67 | lelttrd 11321 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) < (2 Β· π)) |
69 | 36, 39, 68 | ltled 11311 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β€ (2 Β· π)) |
70 | | elicc2 13338 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (2 Β· π) β β) β ((π₯ππ§) β (0[,](2 Β· π)) β ((π₯ππ§) β β β§ 0 β€ (π₯ππ§) β§ (π₯ππ§) β€ (2 Β· π)))) |
71 | 2, 39, 70 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π₯ππ§) β (0[,](2 Β· π)) β ((π₯ππ§) β β β§ 0 β€ (π₯ππ§) β§ (π₯ππ§) β€ (2 Β· π)))) |
72 | 36, 38, 69, 71 | mpbir3and 1343 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β (0[,](2 Β· π))) |
73 | 72 | ralrimivva 3194 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β βπ₯ β π βπ§ β π (π₯ππ§) β (0[,](2 Β· π))) |
74 | | ffnov 7487 |
. . . . . . . . . . 11
β’ (π:(π Γ π)βΆ(0[,](2 Β· π)) β (π Fn (π Γ π) β§ βπ₯ β π βπ§ β π (π₯ππ§) β (0[,](2 Β· π)))) |
75 | 31, 73, 74 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π:(π Γ π)βΆ(0[,](2 Β· π))) |
76 | | oveq2 7369 |
. . . . . . . . . . . 12
β’ (π₯ = (2 Β· π) β (0[,]π₯) = (0[,](2 Β· π))) |
77 | 76 | feq3d 6659 |
. . . . . . . . . . 11
β’ (π₯ = (2 Β· π) β (π:(π Γ π)βΆ(0[,]π₯) β π:(π Γ π)βΆ(0[,](2 Β· π)))) |
78 | 77 | rspcev 3583 |
. . . . . . . . . 10
β’ (((2
Β· π) β β
β§ π:(π Γ π)βΆ(0[,](2 Β· π))) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
79 | 30, 75, 78 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
80 | 79 | expr 458 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π¦ β π β§ π β β+)) β (π = (π¦(ballβπ)π) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
81 | 80 | rexlimdvva 3202 |
. . . . . . 7
β’ (π β (Metβπ) β (βπ¦ β π βπ β β+ π = (π¦(ballβπ)π) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
82 | 1, 81 | syl 17 |
. . . . . 6
β’ (π β (Bndβπ) β (βπ¦ β π βπ β β+ π = (π¦(ballβπ)π) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
83 | 82 | adantr 482 |
. . . . 5
β’ ((π β (Bndβπ) β§ π β β
) β (βπ¦ β π βπ β β+ π = (π¦(ballβπ)π) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
84 | 25, 83 | mpd 15 |
. . . 4
β’ ((π β (Bndβπ) β§ π β β
) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
85 | 23, 84 | pm2.61dane 3029 |
. . 3
β’ (π β (Bndβπ) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
86 | 1, 85 | jca 513 |
. 2
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |
87 | | simpll 766 |
. . . 4
β’ (((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β π β (Metβπ)) |
88 | | simpllr 775 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π₯ β β) |
89 | 87 | adantr 482 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π β (Metβπ)) |
90 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π¦ β π) |
91 | | met0 23719 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ π¦ β π) β (π¦ππ¦) = 0) |
92 | 89, 90, 91 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π¦ππ¦) = 0) |
93 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π:(π Γ π)βΆ(0[,]π₯)) |
94 | 93, 90, 90 | fovcdmd 7530 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π¦ππ¦) β (0[,]π₯)) |
95 | | elicc2 13338 |
. . . . . . . . . . 11
β’ ((0
β β β§ π₯
β β) β ((π¦ππ¦) β (0[,]π₯) β ((π¦ππ¦) β β β§ 0 β€ (π¦ππ¦) β§ (π¦ππ¦) β€ π₯))) |
96 | 2, 88, 95 | sylancr 588 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β ((π¦ππ¦) β (0[,]π₯) β ((π¦ππ¦) β β β§ 0 β€ (π¦ππ¦) β§ (π¦ππ¦) β€ π₯))) |
97 | 94, 96 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β ((π¦ππ¦) β β β§ 0 β€ (π¦ππ¦) β§ (π¦ππ¦) β€ π₯)) |
98 | 97 | simp3d 1145 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π¦ππ¦) β€ π₯) |
99 | 92, 98 | eqbrtrrd 5133 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β 0 β€ π₯) |
100 | 88, 99 | ge0p1rpd 12995 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π₯ + 1) β
β+) |
101 | | fovcdm 7528 |
. . . . . . . . . . . . . 14
β’ ((π:(π Γ π)βΆ(0[,]π₯) β§ π¦ β π β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
102 | 101 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π:(π Γ π)βΆ(0[,]π₯) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
103 | 102 | adantlll 717 |
. . . . . . . . . . . 12
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
104 | | elicc2 13338 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ π₯
β β) β ((π¦ππ§) β (0[,]π₯) β ((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯))) |
105 | 2, 88, 104 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β ((π¦ππ§) β (0[,]π₯) β ((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯))) |
106 | 105 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β ((π¦ππ§) β (0[,]π₯) β ((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯))) |
107 | 103, 106 | mpbid 231 |
. . . . . . . . . . 11
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β ((π¦ππ§) β β β§ 0 β€ (π¦ππ§) β§ (π¦ππ§) β€ π₯)) |
108 | 107 | simp1d 1143 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β β) |
109 | 88 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β π₯ β β) |
110 | | peano2re 11336 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯ + 1) β
β) |
111 | 88, 110 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π₯ + 1) β β) |
112 | 111 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π₯ + 1) β β) |
113 | 107 | simp3d 1145 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β€ π₯) |
114 | 109 | ltp1d 12093 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β π₯ < (π₯ + 1)) |
115 | 108, 109,
112, 113, 114 | lelttrd 11321 |
. . . . . . . . 9
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) < (π₯ + 1)) |
116 | 115 | ralrimiva 3140 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β βπ§ β π (π¦ππ§) < (π₯ + 1)) |
117 | | rabid2 3438 |
. . . . . . . 8
β’ (π = {π§ β π β£ (π¦ππ§) < (π₯ + 1)} β βπ§ β π (π¦ππ§) < (π₯ + 1)) |
118 | 116, 117 | sylibr 233 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π = {π§ β π β£ (π¦ππ§) < (π₯ + 1)}) |
119 | 89, 52 | syl 17 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π β (βMetβπ)) |
120 | 111 | rexrd 11213 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π₯ + 1) β
β*) |
121 | | blval 23762 |
. . . . . . . 8
β’ ((π β (βMetβπ) β§ π¦ β π β§ (π₯ + 1) β β*) β
(π¦(ballβπ)(π₯ + 1)) = {π§ β π β£ (π¦ππ§) < (π₯ + 1)}) |
122 | 119, 90, 120, 121 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π¦(ballβπ)(π₯ + 1)) = {π§ β π β£ (π¦ππ§) < (π₯ + 1)}) |
123 | 118, 122 | eqtr4d 2776 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π = (π¦(ballβπ)(π₯ + 1))) |
124 | | oveq2 7369 |
. . . . . . 7
β’ (π = (π₯ + 1) β (π¦(ballβπ)π) = (π¦(ballβπ)(π₯ + 1))) |
125 | 124 | rspceeqv 3599 |
. . . . . 6
β’ (((π₯ + 1) β β+
β§ π = (π¦(ballβπ)(π₯ + 1))) β βπ β β+ π = (π¦(ballβπ)π)) |
126 | 100, 123,
125 | syl2anc 585 |
. . . . 5
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β βπ β β+ π = (π¦(ballβπ)π)) |
127 | 126 | ralrimiva 3140 |
. . . 4
β’ (((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)) |
128 | | isbnd 36289 |
. . . 4
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
129 | 87, 127, 128 | sylanbrc 584 |
. . 3
β’ (((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β π β (Bndβπ)) |
130 | 129 | r19.29an 3152 |
. 2
β’ ((π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) β π β (Bndβπ)) |
131 | 86, 130 | impbii 208 |
1
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |