Step | Hyp | Ref
| Expression |
1 | | ipcn.t |
. . . 4
β’ π = ((π
/ 2) / ((πβπ΄) + 1)) |
2 | | ipcn.r |
. . . . . 6
β’ (π β π
β
β+) |
3 | 2 | rphalfcld 13028 |
. . . . 5
β’ (π β (π
/ 2) β
β+) |
4 | | ipcn.w |
. . . . . . . . 9
β’ (π β π β βPreHil) |
5 | | cphnlm 24689 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
NrmMod) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmMod) |
7 | | nlmngp 24194 |
. . . . . . . 8
β’ (π β NrmMod β π β NrmGrp) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ (π β π β NrmGrp) |
9 | | ipcn.a |
. . . . . . 7
β’ (π β π΄ β π) |
10 | | ipcn.v |
. . . . . . . 8
β’ π = (Baseβπ) |
11 | | ipcn.n |
. . . . . . . 8
β’ π = (normβπ) |
12 | 10, 11 | nmcl 24125 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π) β (πβπ΄) β β) |
13 | 8, 9, 12 | syl2anc 585 |
. . . . . 6
β’ (π β (πβπ΄) β β) |
14 | 10, 11 | nmge0 24126 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π) β 0 β€ (πβπ΄)) |
15 | 8, 9, 14 | syl2anc 585 |
. . . . . 6
β’ (π β 0 β€ (πβπ΄)) |
16 | 13, 15 | ge0p1rpd 13046 |
. . . . 5
β’ (π β ((πβπ΄) + 1) β
β+) |
17 | 3, 16 | rpdivcld 13033 |
. . . 4
β’ (π β ((π
/ 2) / ((πβπ΄) + 1)) β
β+) |
18 | 1, 17 | eqeltrid 2838 |
. . 3
β’ (π β π β
β+) |
19 | | ipcn.u |
. . . 4
β’ π = ((π
/ 2) / ((πβπ΅) + π)) |
20 | | ipcn.b |
. . . . . . . 8
β’ (π β π΅ β π) |
21 | 10, 11 | nmcl 24125 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π΅ β π) β (πβπ΅) β β) |
22 | 8, 20, 21 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβπ΅) β β) |
23 | 18 | rpred 13016 |
. . . . . . 7
β’ (π β π β β) |
24 | 22, 23 | readdcld 11243 |
. . . . . 6
β’ (π β ((πβπ΅) + π) β β) |
25 | | 0red 11217 |
. . . . . . 7
β’ (π β 0 β
β) |
26 | 10, 11 | nmge0 24126 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π΅ β π) β 0 β€ (πβπ΅)) |
27 | 8, 20, 26 | syl2anc 585 |
. . . . . . 7
β’ (π β 0 β€ (πβπ΅)) |
28 | 22, 18 | ltaddrpd 13049 |
. . . . . . 7
β’ (π β (πβπ΅) < ((πβπ΅) + π)) |
29 | 25, 22, 24, 27, 28 | lelttrd 11372 |
. . . . . 6
β’ (π β 0 < ((πβπ΅) + π)) |
30 | 24, 29 | elrpd 13013 |
. . . . 5
β’ (π β ((πβπ΅) + π) β
β+) |
31 | 3, 30 | rpdivcld 13033 |
. . . 4
β’ (π β ((π
/ 2) / ((πβπ΅) + π)) β
β+) |
32 | 19, 31 | eqeltrid 2838 |
. . 3
β’ (π β π β
β+) |
33 | 18, 32 | ifcld 4575 |
. 2
β’ (π β if(π β€ π, π, π) β
β+) |
34 | | ipcn.h |
. . . . 5
β’ , =
(Β·πβπ) |
35 | | ipcn.d |
. . . . 5
β’ π· = (distβπ) |
36 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β βPreHil) |
37 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π΄ β π) |
38 | 20 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π΅ β π) |
39 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π
β
β+) |
40 | | simprll 778 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π₯ β π) |
41 | | simprlr 779 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π¦ β π) |
42 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β NrmGrp) |
43 | | ngpms 24109 |
. . . . . . . 8
β’ (π β NrmGrp β π β MetSp) |
44 | 42, 43 | syl 17 |
. . . . . . 7
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β MetSp) |
45 | 10, 35 | mscl 23967 |
. . . . . . 7
β’ ((π β MetSp β§ π΄ β π β§ π₯ β π) β (π΄π·π₯) β β) |
46 | 44, 37, 40, 45 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΄π·π₯) β β) |
47 | 33 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β if(π β€ π, π, π) β
β+) |
48 | 47 | rpred 13016 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β if(π β€ π, π, π) β β) |
49 | 32 | rpred 13016 |
. . . . . . 7
β’ (π β π β β) |
50 | 49 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β β) |
51 | | simprrl 780 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΄π·π₯) < if(π β€ π, π, π)) |
52 | 23 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β β) |
53 | | min2 13169 |
. . . . . . 7
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
54 | 52, 50, 53 | syl2anc 585 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β if(π β€ π, π, π) β€ π) |
55 | 46, 48, 50, 51, 54 | ltletrd 11374 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΄π·π₯) < π) |
56 | 8, 43 | syl 17 |
. . . . . . . 8
β’ (π β π β MetSp) |
57 | 56 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β π β MetSp) |
58 | 10, 35 | mscl 23967 |
. . . . . . 7
β’ ((π β MetSp β§ π΅ β π β§ π¦ β π) β (π΅π·π¦) β β) |
59 | 57, 38, 41, 58 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΅π·π¦) β β) |
60 | | simprrr 781 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΅π·π¦) < if(π β€ π, π, π)) |
61 | | min1 13168 |
. . . . . . 7
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
62 | 52, 50, 61 | syl2anc 585 |
. . . . . 6
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β if(π β€ π, π, π) β€ π) |
63 | 59, 48, 52, 60, 62 | ltletrd 11374 |
. . . . 5
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (π΅π·π¦) < π) |
64 | 10, 34, 35, 11, 1, 19, 36, 37, 38, 39, 40, 41, 55, 63 | ipcnlem2 24761 |
. . . 4
β’ ((π β§ ((π₯ β π β§ π¦ β π) β§ ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
) |
65 | 64 | expr 458 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
)) |
66 | 65 | ralrimivva 3201 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
)) |
67 | | breq2 5153 |
. . . . . 6
β’ (π = if(π β€ π, π, π) β ((π΄π·π₯) < π β (π΄π·π₯) < if(π β€ π, π, π))) |
68 | | breq2 5153 |
. . . . . 6
β’ (π = if(π β€ π, π, π) β ((π΅π·π¦) < π β (π΅π·π¦) < if(π β€ π, π, π))) |
69 | 67, 68 | anbi12d 632 |
. . . . 5
β’ (π = if(π β€ π, π, π) β (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β ((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)))) |
70 | 69 | imbi1d 342 |
. . . 4
β’ (π = if(π β€ π, π, π) β ((((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
) β (((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
))) |
71 | 70 | 2ralbidv 3219 |
. . 3
β’ (π = if(π β€ π, π, π) β (βπ₯ β π βπ¦ β π (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
) β βπ₯ β π βπ¦ β π (((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
))) |
72 | 71 | rspcev 3613 |
. 2
β’
((if(π β€ π, π, π) β β+ β§
βπ₯ β π βπ¦ β π (((π΄π·π₯) < if(π β€ π, π, π) β§ (π΅π·π¦) < if(π β€ π, π, π)) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
)) β βπ β β+ βπ₯ β π βπ¦ β π (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
)) |
73 | 33, 66, 72 | syl2anc 585 |
1
β’ (π β βπ β β+ βπ₯ β π βπ¦ β π (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π
)) |