Step | Hyp | Ref
| Expression |
1 | | ipcn.w |
. . 3
β’ (π β π β βPreHil) |
2 | | ipcn.a |
. . 3
β’ (π β π΄ β π) |
3 | | ipcn.b |
. . 3
β’ (π β π΅ β π) |
4 | | ipcn.v |
. . . 4
β’ π = (Baseβπ) |
5 | | ipcn.h |
. . . 4
β’ , =
(Β·πβπ) |
6 | 4, 5 | cphipcl 24578 |
. . 3
β’ ((π β βPreHil β§
π΄ β π β§ π΅ β π) β (π΄ , π΅) β β) |
7 | 1, 2, 3, 6 | syl3anc 1372 |
. 2
β’ (π β (π΄ , π΅) β β) |
8 | | ipcn.x |
. . 3
β’ (π β π β π) |
9 | | ipcn.y |
. . 3
β’ (π β π β π) |
10 | 4, 5 | cphipcl 24578 |
. . 3
β’ ((π β βPreHil β§
π β π β§ π β π) β (π , π) β β) |
11 | 1, 8, 9, 10 | syl3anc 1372 |
. 2
β’ (π β (π , π) β β) |
12 | 4, 5 | cphipcl 24578 |
. . 3
β’ ((π β βPreHil β§
π΄ β π β§ π β π) β (π΄ , π) β β) |
13 | 1, 2, 9, 12 | syl3anc 1372 |
. 2
β’ (π β (π΄ , π) β β) |
14 | | ipcn.r |
. . 3
β’ (π β π
β
β+) |
15 | 14 | rpred 12965 |
. 2
β’ (π β π
β β) |
16 | 7, 13 | subcld 11520 |
. . . 4
β’ (π β ((π΄ , π΅) β (π΄ , π)) β β) |
17 | 16 | abscld 15330 |
. . 3
β’ (π β (absβ((π΄ , π΅) β (π΄ , π))) β β) |
18 | | cphnlm 24559 |
. . . . . . . . 9
β’ (π β βPreHil β
π β
NrmMod) |
19 | 1, 18 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmMod) |
20 | | nlmngp 24064 |
. . . . . . . 8
β’ (π β NrmMod β π β NrmGrp) |
21 | 19, 20 | syl 17 |
. . . . . . 7
β’ (π β π β NrmGrp) |
22 | | ipcn.n |
. . . . . . . 8
β’ π = (normβπ) |
23 | 4, 22 | nmcl 23995 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π) β (πβπ΄) β β) |
24 | 21, 2, 23 | syl2anc 585 |
. . . . . 6
β’ (π β (πβπ΄) β β) |
25 | 4, 22 | nmge0 23996 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΄ β π) β 0 β€ (πβπ΄)) |
26 | 21, 2, 25 | syl2anc 585 |
. . . . . 6
β’ (π β 0 β€ (πβπ΄)) |
27 | 24, 26 | ge0p1rpd 12995 |
. . . . 5
β’ (π β ((πβπ΄) + 1) β
β+) |
28 | 27 | rpred 12965 |
. . . 4
β’ (π β ((πβπ΄) + 1) β β) |
29 | | ngpms 23979 |
. . . . . 6
β’ (π β NrmGrp β π β MetSp) |
30 | 21, 29 | syl 17 |
. . . . 5
β’ (π β π β MetSp) |
31 | | ipcn.d |
. . . . . 6
β’ π· = (distβπ) |
32 | 4, 31 | mscl 23837 |
. . . . 5
β’ ((π β MetSp β§ π΅ β π β§ π β π) β (π΅π·π) β β) |
33 | 30, 3, 9, 32 | syl3anc 1372 |
. . . 4
β’ (π β (π΅π·π) β β) |
34 | 28, 33 | remulcld 11193 |
. . 3
β’ (π β (((πβπ΄) + 1) Β· (π΅π·π)) β β) |
35 | 15 | rehalfcld 12408 |
. . 3
β’ (π β (π
/ 2) β β) |
36 | 24, 33 | remulcld 11193 |
. . . 4
β’ (π β ((πβπ΄) Β· (π΅π·π)) β β) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(-gβπ) = (-gβπ) |
38 | 5, 4, 37 | cphsubdi 24596 |
. . . . . . 7
β’ ((π β βPreHil β§
(π΄ β π β§ π΅ β π β§ π β π)) β (π΄ , (π΅(-gβπ)π)) = ((π΄ , π΅) β (π΄ , π))) |
39 | 1, 2, 3, 9, 38 | syl13anc 1373 |
. . . . . 6
β’ (π β (π΄ , (π΅(-gβπ)π)) = ((π΄ , π΅) β (π΄ , π))) |
40 | 39 | fveq2d 6850 |
. . . . 5
β’ (π β (absβ(π΄ , (π΅(-gβπ)π))) = (absβ((π΄ , π΅) β (π΄ , π)))) |
41 | | ngpgrp 23978 |
. . . . . . . . 9
β’ (π β NrmGrp β π β Grp) |
42 | 21, 41 | syl 17 |
. . . . . . . 8
β’ (π β π β Grp) |
43 | 4, 37 | grpsubcl 18835 |
. . . . . . . 8
β’ ((π β Grp β§ π΅ β π β§ π β π) β (π΅(-gβπ)π) β π) |
44 | 42, 3, 9, 43 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΅(-gβπ)π) β π) |
45 | 4, 5, 22 | ipcau 24625 |
. . . . . . 7
β’ ((π β βPreHil β§
π΄ β π β§ (π΅(-gβπ)π) β π) β (absβ(π΄ , (π΅(-gβπ)π))) β€ ((πβπ΄) Β· (πβ(π΅(-gβπ)π)))) |
46 | 1, 2, 44, 45 | syl3anc 1372 |
. . . . . 6
β’ (π β (absβ(π΄ , (π΅(-gβπ)π))) β€ ((πβπ΄) Β· (πβ(π΅(-gβπ)π)))) |
47 | 22, 4, 37, 31 | ngpds 23983 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π΅ β π β§ π β π) β (π΅π·π) = (πβ(π΅(-gβπ)π))) |
48 | 21, 3, 9, 47 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΅π·π) = (πβ(π΅(-gβπ)π))) |
49 | 48 | oveq2d 7377 |
. . . . . 6
β’ (π β ((πβπ΄) Β· (π΅π·π)) = ((πβπ΄) Β· (πβ(π΅(-gβπ)π)))) |
50 | 46, 49 | breqtrrd 5137 |
. . . . 5
β’ (π β (absβ(π΄ , (π΅(-gβπ)π))) β€ ((πβπ΄) Β· (π΅π·π))) |
51 | 40, 50 | eqbrtrrd 5133 |
. . . 4
β’ (π β (absβ((π΄ , π΅) β (π΄ , π))) β€ ((πβπ΄) Β· (π΅π·π))) |
52 | | msxms 23830 |
. . . . . . 7
β’ (π β MetSp β π β
βMetSp) |
53 | 30, 52 | syl 17 |
. . . . . 6
β’ (π β π β βMetSp) |
54 | 4, 31 | xmsge0 23839 |
. . . . . 6
β’ ((π β βMetSp β§ π΅ β π β§ π β π) β 0 β€ (π΅π·π)) |
55 | 53, 3, 9, 54 | syl3anc 1372 |
. . . . 5
β’ (π β 0 β€ (π΅π·π)) |
56 | 24 | lep1d 12094 |
. . . . 5
β’ (π β (πβπ΄) β€ ((πβπ΄) + 1)) |
57 | 24, 28, 33, 55, 56 | lemul1ad 12102 |
. . . 4
β’ (π β ((πβπ΄) Β· (π΅π·π)) β€ (((πβπ΄) + 1) Β· (π΅π·π))) |
58 | 17, 36, 34, 51, 57 | letrd 11320 |
. . 3
β’ (π β (absβ((π΄ , π΅) β (π΄ , π))) β€ (((πβπ΄) + 1) Β· (π΅π·π))) |
59 | | ipcn.2 |
. . . . 5
β’ (π β (π΅π·π) < π) |
60 | | ipcn.t |
. . . . 5
β’ π = ((π
/ 2) / ((πβπ΄) + 1)) |
61 | 59, 60 | breqtrdi 5150 |
. . . 4
β’ (π β (π΅π·π) < ((π
/ 2) / ((πβπ΄) + 1))) |
62 | 33, 35, 27 | ltmuldiv2d 13013 |
. . . 4
β’ (π β ((((πβπ΄) + 1) Β· (π΅π·π)) < (π
/ 2) β (π΅π·π) < ((π
/ 2) / ((πβπ΄) + 1)))) |
63 | 61, 62 | mpbird 257 |
. . 3
β’ (π β (((πβπ΄) + 1) Β· (π΅π·π)) < (π
/ 2)) |
64 | 17, 34, 35, 58, 63 | lelttrd 11321 |
. 2
β’ (π β (absβ((π΄ , π΅) β (π΄ , π))) < (π
/ 2)) |
65 | 13, 11 | subcld 11520 |
. . . 4
β’ (π β ((π΄ , π) β (π , π)) β β) |
66 | 65 | abscld 15330 |
. . 3
β’ (π β (absβ((π΄ , π) β (π , π))) β β) |
67 | 4, 31 | mscl 23837 |
. . . . 5
β’ ((π β MetSp β§ π΄ β π β§ π β π) β (π΄π·π) β β) |
68 | 30, 2, 8, 67 | syl3anc 1372 |
. . . 4
β’ (π β (π΄π·π) β β) |
69 | 4, 22 | nmcl 23995 |
. . . . . 6
β’ ((π β NrmGrp β§ π΅ β π) β (πβπ΅) β β) |
70 | 21, 3, 69 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ΅) β β) |
71 | 14 | rphalfcld 12977 |
. . . . . . . 8
β’ (π β (π
/ 2) β
β+) |
72 | 71, 27 | rpdivcld 12982 |
. . . . . . 7
β’ (π β ((π
/ 2) / ((πβπ΄) + 1)) β
β+) |
73 | 60, 72 | eqeltrid 2838 |
. . . . . 6
β’ (π β π β
β+) |
74 | 73 | rpred 12965 |
. . . . 5
β’ (π β π β β) |
75 | 70, 74 | readdcld 11192 |
. . . 4
β’ (π β ((πβπ΅) + π) β β) |
76 | 68, 75 | remulcld 11193 |
. . 3
β’ (π β ((π΄π·π) Β· ((πβπ΅) + π)) β β) |
77 | 4, 22 | nmcl 23995 |
. . . . . 6
β’ ((π β NrmGrp β§ π β π) β (πβπ) β β) |
78 | 21, 9, 77 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ) β β) |
79 | 68, 78 | remulcld 11193 |
. . . 4
β’ (π β ((π΄π·π) Β· (πβπ)) β β) |
80 | 5, 4, 37 | cphsubdir 24595 |
. . . . . . 7
β’ ((π β βPreHil β§
(π΄ β π β§ π β π β§ π β π)) β ((π΄(-gβπ)π) , π) = ((π΄ , π) β (π , π))) |
81 | 1, 2, 8, 9, 80 | syl13anc 1373 |
. . . . . 6
β’ (π β ((π΄(-gβπ)π) , π) = ((π΄ , π) β (π , π))) |
82 | 81 | fveq2d 6850 |
. . . . 5
β’ (π β (absβ((π΄(-gβπ)π) , π)) = (absβ((π΄ , π) β (π , π)))) |
83 | 4, 37 | grpsubcl 18835 |
. . . . . . . 8
β’ ((π β Grp β§ π΄ β π β§ π β π) β (π΄(-gβπ)π) β π) |
84 | 42, 2, 8, 83 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄(-gβπ)π) β π) |
85 | 4, 5, 22 | ipcau 24625 |
. . . . . . 7
β’ ((π β βPreHil β§
(π΄(-gβπ)π) β π β§ π β π) β (absβ((π΄(-gβπ)π) , π)) β€ ((πβ(π΄(-gβπ)π)) Β· (πβπ))) |
86 | 1, 84, 9, 85 | syl3anc 1372 |
. . . . . 6
β’ (π β (absβ((π΄(-gβπ)π) , π)) β€ ((πβ(π΄(-gβπ)π)) Β· (πβπ))) |
87 | 22, 4, 37, 31 | ngpds 23983 |
. . . . . . . 8
β’ ((π β NrmGrp β§ π΄ β π β§ π β π) β (π΄π·π) = (πβ(π΄(-gβπ)π))) |
88 | 21, 2, 8, 87 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄π·π) = (πβ(π΄(-gβπ)π))) |
89 | 88 | oveq1d 7376 |
. . . . . 6
β’ (π β ((π΄π·π) Β· (πβπ)) = ((πβ(π΄(-gβπ)π)) Β· (πβπ))) |
90 | 86, 89 | breqtrrd 5137 |
. . . . 5
β’ (π β (absβ((π΄(-gβπ)π) , π)) β€ ((π΄π·π) Β· (πβπ))) |
91 | 82, 90 | eqbrtrrd 5133 |
. . . 4
β’ (π β (absβ((π΄ , π) β (π , π))) β€ ((π΄π·π) Β· (πβπ))) |
92 | 4, 31 | xmsge0 23839 |
. . . . . 6
β’ ((π β βMetSp β§ π΄ β π β§ π β π) β 0 β€ (π΄π·π)) |
93 | 53, 2, 8, 92 | syl3anc 1372 |
. . . . 5
β’ (π β 0 β€ (π΄π·π)) |
94 | 78, 70 | resubcld 11591 |
. . . . . . 7
β’ (π β ((πβπ) β (πβπ΅)) β β) |
95 | 4, 22, 37 | nm2dif 24004 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ π β π β§ π΅ β π) β ((πβπ) β (πβπ΅)) β€ (πβ(π(-gβπ)π΅))) |
96 | 21, 9, 3, 95 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((πβπ) β (πβπ΅)) β€ (πβ(π(-gβπ)π΅))) |
97 | 22, 4, 37, 31 | ngpdsr 23984 |
. . . . . . . . 9
β’ ((π β NrmGrp β§ π΅ β π β§ π β π) β (π΅π·π) = (πβ(π(-gβπ)π΅))) |
98 | 21, 3, 9, 97 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π΅π·π) = (πβ(π(-gβπ)π΅))) |
99 | 96, 98 | breqtrrd 5137 |
. . . . . . 7
β’ (π β ((πβπ) β (πβπ΅)) β€ (π΅π·π)) |
100 | 33, 74, 59 | ltled 11311 |
. . . . . . 7
β’ (π β (π΅π·π) β€ π) |
101 | 94, 33, 74, 99, 100 | letrd 11320 |
. . . . . 6
β’ (π β ((πβπ) β (πβπ΅)) β€ π) |
102 | 78, 70, 74 | lesubadd2d 11762 |
. . . . . 6
β’ (π β (((πβπ) β (πβπ΅)) β€ π β (πβπ) β€ ((πβπ΅) + π))) |
103 | 101, 102 | mpbid 231 |
. . . . 5
β’ (π β (πβπ) β€ ((πβπ΅) + π)) |
104 | 78, 75, 68, 93, 103 | lemul2ad 12103 |
. . . 4
β’ (π β ((π΄π·π) Β· (πβπ)) β€ ((π΄π·π) Β· ((πβπ΅) + π))) |
105 | 66, 79, 76, 91, 104 | letrd 11320 |
. . 3
β’ (π β (absβ((π΄ , π) β (π , π))) β€ ((π΄π·π) Β· ((πβπ΅) + π))) |
106 | | ipcn.1 |
. . . . 5
β’ (π β (π΄π·π) < π) |
107 | | ipcn.u |
. . . . 5
β’ π = ((π
/ 2) / ((πβπ΅) + π)) |
108 | 106, 107 | breqtrdi 5150 |
. . . 4
β’ (π β (π΄π·π) < ((π
/ 2) / ((πβπ΅) + π))) |
109 | | 0red 11166 |
. . . . . 6
β’ (π β 0 β
β) |
110 | 4, 22 | nmge0 23996 |
. . . . . . 7
β’ ((π β NrmGrp β§ π΅ β π) β 0 β€ (πβπ΅)) |
111 | 21, 3, 110 | syl2anc 585 |
. . . . . 6
β’ (π β 0 β€ (πβπ΅)) |
112 | 70, 73 | ltaddrpd 12998 |
. . . . . 6
β’ (π β (πβπ΅) < ((πβπ΅) + π)) |
113 | 109, 70, 75, 111, 112 | lelttrd 11321 |
. . . . 5
β’ (π β 0 < ((πβπ΅) + π)) |
114 | | ltmuldiv 12036 |
. . . . 5
β’ (((π΄π·π) β β β§ (π
/ 2) β β β§ (((πβπ΅) + π) β β β§ 0 < ((πβπ΅) + π))) β (((π΄π·π) Β· ((πβπ΅) + π)) < (π
/ 2) β (π΄π·π) < ((π
/ 2) / ((πβπ΅) + π)))) |
115 | 68, 35, 75, 113, 114 | syl112anc 1375 |
. . . 4
β’ (π β (((π΄π·π) Β· ((πβπ΅) + π)) < (π
/ 2) β (π΄π·π) < ((π
/ 2) / ((πβπ΅) + π)))) |
116 | 108, 115 | mpbird 257 |
. . 3
β’ (π β ((π΄π·π) Β· ((πβπ΅) + π)) < (π
/ 2)) |
117 | 66, 76, 35, 105, 116 | lelttrd 11321 |
. 2
β’ (π β (absβ((π΄ , π) β (π , π))) < (π
/ 2)) |
118 | 7, 11, 13, 15, 64, 117 | abs3lemd 15355 |
1
β’ (π β (absβ((π΄ , π΅) β (π , π))) < π
) |