Step | Hyp | Ref
| Expression |
1 | | bndmet 36697 |
. . 3
β’ (π β (Bndβπ) β π β (Metβπ)) |
2 | | 0re 11216 |
. . . . . 6
β’ 0 β
β |
3 | 2 | ne0ii 4338 |
. . . . 5
β’ β
β β
|
4 | | metf 23836 |
. . . . . . . . . 10
β’ (π β (Metβπ) β π:(π Γ π)βΆβ) |
5 | 4 | ffnd 6719 |
. . . . . . . . 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 6729 |
. . . . . . . . . . 11
β’ (π β (Bndβπ) β dom π = (π Γ π)) |
10 | | xpeq2 5698 |
. . . . . . . . . . . 12
β’ (π = β
β (π Γ π) = (π Γ β
)) |
11 | | xp0 6158 |
. . . . . . . . . . . 12
β’ (π Γ β
) =
β
|
12 | 10, 11 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π = β
β (π Γ π) = β
) |
13 | 9, 12 | sylan9eq 2793 |
. . . . . . . . . 10
β’ ((π β (Bndβπ) β§ π = β
) β dom π = β
) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β dom π = β
) |
15 | | dm0rn0 5925 |
. . . . . . . . 9
β’ (dom
π = β
β ran
π =
β
) |
16 | 14, 15 | sylib 217 |
. . . . . . . 8
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β ran π = β
) |
17 | | 0ss 4397 |
. . . . . . . 8
β’ β
β (0[,]π₯) |
18 | 16, 17 | eqsstrdi 4037 |
. . . . . . 7
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β ran π β (0[,]π₯)) |
19 | | df-f 6548 |
. . . . . . 7
β’ (π:(π Γ π)βΆ(0[,]π₯) β (π Fn (π Γ π) β§ ran π β (0[,]π₯))) |
20 | 7, 18, 19 | sylanbrc 584 |
. . . . . 6
β’ (((π β (Bndβπ) β§ π = β
) β§ π₯ β β) β π:(π Γ π)βΆ(0[,]π₯)) |
21 | 20 | ralrimiva 3147 |
. . . . 5
β’ ((π β (Bndβπ) β§ π = β
) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
22 | | r19.2z 4495 |
. . . . 5
β’ ((β
β β
β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
23 | 3, 21, 22 | sylancr 588 |
. . . 4
β’ ((π β (Bndβπ) β§ π = β
) β βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) |
24 | | isbnd2 36699 |
. . . . . 6
β’ ((π β (Bndβπ) β§ π β β
) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
25 | 24 | simprbi 498 |
. . . . 5
β’ ((π β (Bndβπ) β§ π β β
) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)) |
26 | | 2re 12286 |
. . . . . . . . . . 11
β’ 2 β
β |
27 | | simprlr 779 |
. . . . . . . . . . . 12
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π β β+) |
28 | 27 | rpred 13016 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π β β) |
29 | | remulcl 11195 |
. . . . . . . . . . 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 23838 |
. . . . . . . . . . . . . 14
β’ ((π β (Metβπ) β§ π₯ β π β§ π§ β π) β (π₯ππ§) β β) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β β) |
37 | | metge0 23851 |
. . . . . . . . . . . . . 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 23838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (Metβπ) β§ π¦ β π β§ π₯ β π) β (π¦ππ₯) β β) |
43 | 32, 41, 33, 42 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ₯) β β) |
44 | | metcl 23838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (Metβπ) β§ π¦ β π β§ π§ β π) β (π¦ππ§) β β) |
45 | 32, 41, 34, 44 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π¦ππ§) β β) |
46 | 43, 45 | readdcld 11243 |
. . . . . . . . . . . . . . 15
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) β β) |
47 | | mettri2 23847 |
. . . . . . . . . . . . . . . 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 23840 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Metβπ) β π β (βMetβπ)) |
53 | 32, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β (βMetβπ)) |
54 | | rpxr 12983 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β π β
β*) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π)) β π β β*) |
56 | 55 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β β*) |
57 | | elbl2 23896 |
. . . . . . . . . . . . . . . . . . 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 23896 |
. . . . . . . . . . . . . . . . . . 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 11837 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) < (π + π)) |
65 | 49 | recnd 11242 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β π β β) |
66 | 65 | 2timesd 12455 |
. . . . . . . . . . . . . . . 16
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (2 Β· π) = (π + π)) |
67 | 64, 66 | breqtrrd 5177 |
. . . . . . . . . . . . . . 15
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β ((π¦ππ₯) + (π¦ππ§)) < (2 Β· π)) |
68 | 36, 46, 39, 48, 67 | lelttrd 11372 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) < (2 Β· π)) |
69 | 36, 39, 68 | ltled 11362 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β§ (π₯ β π β§ π§ β π)) β (π₯ππ§) β€ (2 Β· π)) |
70 | | elicc2 13389 |
. . . . . . . . . . . . . 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 3201 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β βπ₯ β π βπ§ β π (π₯ππ§) β (0[,](2 Β· π))) |
74 | | ffnov 7535 |
. . . . . . . . . . 11
β’ (π:(π Γ π)βΆ(0[,](2 Β· π)) β (π Fn (π Γ π) β§ βπ₯ β π βπ§ β π (π₯ππ§) β (0[,](2 Β· π)))) |
75 | 31, 73, 74 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β (Metβπ) β§ ((π¦ β π β§ π β β+) β§ π = (π¦(ballβπ)π))) β π:(π Γ π)βΆ(0[,](2 Β· π))) |
76 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π₯ = (2 Β· π) β (0[,]π₯) = (0[,](2 Β· π))) |
77 | 76 | feq3d 6705 |
. . . . . . . . . . 11
β’ (π₯ = (2 Β· π) β (π:(π Γ π)βΆ(0[,]π₯) β π:(π Γ π)βΆ(0[,](2 Β· π)))) |
78 | 77 | rspcev 3613 |
. . . . . . . . . 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 3212 |
. . . . . . 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 3030 |
. . 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 23849 |
. . . . . . . . 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 7579 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π¦ππ¦) β (0[,]π₯)) |
95 | | elicc2 13389 |
. . . . . . . . . . 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 5173 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β 0 β€ π₯) |
100 | 88, 99 | ge0p1rpd 13046 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π₯ + 1) β
β+) |
101 | | fovcdm 7577 |
. . . . . . . . . . . . . 14
β’ ((π:(π Γ π)βΆ(0[,]π₯) β§ π¦ β π β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
102 | 101 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π:(π Γ π)βΆ(0[,]π₯) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
103 | 102 | adantlll 717 |
. . . . . . . . . . . 12
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) β (0[,]π₯)) |
104 | | elicc2 13389 |
. . . . . . . . . . . . . 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 11387 |
. . . . . . . . . . . 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 12144 |
. . . . . . . . . 10
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β π₯ < (π₯ + 1)) |
115 | 108, 109,
112, 113, 114 | lelttrd 11372 |
. . . . . . . . 9
β’
(((((π β
(Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β§ π§ β π) β (π¦ππ§) < (π₯ + 1)) |
116 | 115 | ralrimiva 3147 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β βπ§ β π (π¦ππ§) < (π₯ + 1)) |
117 | | rabid2 3465 |
. . . . . . . 8
β’ (π = {π§ β π β£ (π¦ππ§) < (π₯ + 1)} β βπ§ β π (π¦ππ§) < (π₯ + 1)) |
118 | 116, 117 | sylibr 233 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π = {π§ β π β£ (π¦ππ§) < (π₯ + 1)}) |
119 | 89, 52 | syl 17 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β π β (βMetβπ)) |
120 | 111 | rexrd 11264 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β (π₯ + 1) β
β*) |
121 | | blval 23892 |
. . . . . . . 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 7417 |
. . . . . . 7
β’ (π = (π₯ + 1) β (π¦(ballβπ)π) = (π¦(ballβπ)(π₯ + 1))) |
125 | 124 | rspceeqv 3634 |
. . . . . 6
β’ (((π₯ + 1) β β+
β§ π = (π¦(ballβπ)(π₯ + 1))) β βπ β β+ π = (π¦(ballβπ)π)) |
126 | 100, 123,
125 | syl2anc 585 |
. . . . 5
β’ ((((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β§ π¦ β π) β βπ β β+ π = (π¦(ballβπ)π)) |
127 | 126 | ralrimiva 3147 |
. . . 4
β’ (((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)) |
128 | | isbnd 36696 |
. . . 4
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
129 | 87, 127, 128 | sylanbrc 584 |
. . 3
β’ (((π β (Metβπ) β§ π₯ β β) β§ π:(π Γ π)βΆ(0[,]π₯)) β π β (Bndβπ)) |
130 | 129 | r19.29an 3159 |
. 2
β’ ((π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯)) β π β (Bndβπ)) |
131 | 86, 130 | impbii 208 |
1
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β β π:(π Γ π)βΆ(0[,]π₯))) |