Step | Hyp | Ref
| Expression |
1 | | tcphcph.1 |
. . . . . . 7
β’ (π β π β PreHil) |
2 | | phllmod 21057 |
. . . . . . 7
β’ (π β PreHil β π β LMod) |
3 | | lmodgrp 20372 |
. . . . . . 7
β’ (π β LMod β π β Grp) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . 6
β’ (π β π β Grp) |
5 | | tcphcphlem1.3 |
. . . . . 6
β’ (π β π β π) |
6 | | tcphcphlem1.4 |
. . . . . 6
β’ (π β π β π) |
7 | | tcphcph.v |
. . . . . . 7
β’ π = (Baseβπ) |
8 | | tcphcph.m |
. . . . . . 7
β’ β =
(-gβπ) |
9 | 7, 8 | grpsubcl 18835 |
. . . . . 6
β’ ((π β Grp β§ π β π β§ π β π) β (π β π) β π) |
10 | 4, 5, 6, 9 | syl3anc 1372 |
. . . . 5
β’ (π β (π β π) β π) |
11 | | tcphval.n |
. . . . . 6
β’ πΊ = (toβPreHilβπ) |
12 | | tcphcph.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
13 | | tcphcph.2 |
. . . . . 6
β’ (π β πΉ = (βfld
βΎs πΎ)) |
14 | | tcphcph.h |
. . . . . 6
β’ , =
(Β·πβπ) |
15 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24620 |
. . . . 5
β’ ((π β§ (π β π) β π) β ((π β π) , (π β π)) β β) |
16 | 10, 15 | mpdan 686 |
. . . 4
β’ (π β ((π β π) , (π β π)) β β) |
17 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24620 |
. . . . . . 7
β’ ((π β§ π β π) β (π , π) β β) |
18 | 5, 17 | mpdan 686 |
. . . . . 6
β’ (π β (π , π) β β) |
19 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24620 |
. . . . . . 7
β’ ((π β§ π β π) β (π , π) β β) |
20 | 6, 19 | mpdan 686 |
. . . . . 6
β’ (π β (π , π) β β) |
21 | 18, 20 | readdcld 11192 |
. . . . 5
β’ (π β ((π , π) + (π , π)) β β) |
22 | 11, 7, 12, 1, 13 | phclm 24619 |
. . . . . . . . 9
β’ (π β π β βMod) |
23 | | tcphcph.k |
. . . . . . . . . 10
β’ πΎ = (BaseβπΉ) |
24 | 12, 23 | clmsscn 24465 |
. . . . . . . . 9
β’ (π β βMod β πΎ β
β) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
β’ (π β πΎ β β) |
26 | 12, 14, 7, 23 | ipcl 21060 |
. . . . . . . . 9
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
27 | 1, 5, 6, 26 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π , π) β πΎ) |
28 | 25, 27 | sseldd 3949 |
. . . . . . 7
β’ (π β (π , π) β β) |
29 | 12, 14, 7, 23 | ipcl 21060 |
. . . . . . . . 9
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
30 | 1, 6, 5, 29 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π , π) β πΎ) |
31 | 25, 30 | sseldd 3949 |
. . . . . . 7
β’ (π β (π , π) β β) |
32 | 28, 31 | addcld 11182 |
. . . . . 6
β’ (π β ((π , π) + (π , π)) β β) |
33 | 32 | abscld 15330 |
. . . . 5
β’ (π β (absβ((π , π) + (π , π))) β β) |
34 | 21, 33 | readdcld 11192 |
. . . 4
β’ (π β (((π , π) + (π , π)) + (absβ((π , π) + (π , π)))) β β) |
35 | 18 | recnd 11191 |
. . . . . 6
β’ (π β (π , π) β β) |
36 | | 2re 12235 |
. . . . . . . 8
β’ 2 β
β |
37 | | oveq12 7370 |
. . . . . . . . . . . . 13
β’ ((π₯ = π β§ π₯ = π) β (π₯ , π₯) = (π , π)) |
38 | 37 | anidms 568 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ , π₯) = (π , π)) |
39 | 38 | breq2d 5121 |
. . . . . . . . . . 11
β’ (π₯ = π β (0 β€ (π₯ , π₯) β 0 β€ (π , π))) |
40 | | tcphcph.4 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) |
41 | 40 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ₯ β π 0 β€ (π₯ , π₯)) |
42 | 39, 41, 5 | rspcdva 3584 |
. . . . . . . . . 10
β’ (π β 0 β€ (π , π)) |
43 | 18, 42 | resqrtcld 15311 |
. . . . . . . . 9
β’ (π β (ββ(π , π)) β β) |
44 | | oveq12 7370 |
. . . . . . . . . . . . 13
β’ ((π₯ = π β§ π₯ = π) β (π₯ , π₯) = (π , π)) |
45 | 44 | anidms 568 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ , π₯) = (π , π)) |
46 | 45 | breq2d 5121 |
. . . . . . . . . . 11
β’ (π₯ = π β (0 β€ (π₯ , π₯) β 0 β€ (π , π))) |
47 | 46, 41, 6 | rspcdva 3584 |
. . . . . . . . . 10
β’ (π β 0 β€ (π , π)) |
48 | 20, 47 | resqrtcld 15311 |
. . . . . . . . 9
β’ (π β (ββ(π , π)) β β) |
49 | 43, 48 | remulcld 11193 |
. . . . . . . 8
β’ (π β ((ββ(π , π)) Β· (ββ(π , π))) β β) |
50 | | remulcl 11144 |
. . . . . . . 8
β’ ((2
β β β§ ((ββ(π , π)) Β· (ββ(π , π))) β β) β (2 Β·
((ββ(π , π)) Β·
(ββ(π , π)))) β
β) |
51 | 36, 49, 50 | sylancr 588 |
. . . . . . 7
β’ (π β (2 Β·
((ββ(π , π)) Β·
(ββ(π , π)))) β
β) |
52 | 51 | recnd 11191 |
. . . . . 6
β’ (π β (2 Β·
((ββ(π , π)) Β·
(ββ(π , π)))) β
β) |
53 | 20 | recnd 11191 |
. . . . . 6
β’ (π β (π , π) β β) |
54 | 35, 52, 53 | add32d 11390 |
. . . . 5
β’ (π β (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π)) = (((π , π) + (π , π)) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π)))))) |
55 | 21, 51 | readdcld 11192 |
. . . . 5
β’ (π β (((π , π) + (π , π)) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) β β) |
56 | 54, 55 | eqeltrd 2834 |
. . . 4
β’ (π β (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π)) β β) |
57 | | oveq12 7370 |
. . . . . . . . . . 11
β’ ((π₯ = (π β π) β§ π₯ = (π β π)) β (π₯ , π₯) = ((π β π) , (π β π))) |
58 | 57 | anidms 568 |
. . . . . . . . . 10
β’ (π₯ = (π β π) β (π₯ , π₯) = ((π β π) , (π β π))) |
59 | 58 | breq2d 5121 |
. . . . . . . . 9
β’ (π₯ = (π β π) β (0 β€ (π₯ , π₯) β 0 β€ ((π β π) , (π β π)))) |
60 | 59, 41, 10 | rspcdva 3584 |
. . . . . . . 8
β’ (π β 0 β€ ((π β π) , (π β π))) |
61 | 16, 60 | absidd 15316 |
. . . . . . 7
β’ (π β (absβ((π β π) , (π β π))) = ((π β π) , (π β π))) |
62 | 12 | clmadd 24460 |
. . . . . . . . . . . 12
β’ (π β βMod β + =
(+gβπΉ)) |
63 | 22, 62 | syl 17 |
. . . . . . . . . . 11
β’ (π β + =
(+gβπΉ)) |
64 | 63 | oveqd 7378 |
. . . . . . . . . 10
β’ (π β ((π , π) + (π , π)) = ((π , π)(+gβπΉ)(π , π))) |
65 | 63 | oveqd 7378 |
. . . . . . . . . 10
β’ (π β ((π , π) + (π , π)) = ((π , π)(+gβπΉ)(π , π))) |
66 | 64, 65 | oveq12d 7379 |
. . . . . . . . 9
β’ (π β (((π , π) + (π , π))(-gβπΉ)((π , π) + (π , π))) = (((π , π)(+gβπΉ)(π , π))(-gβπΉ)((π , π)(+gβπΉ)(π , π)))) |
67 | 12, 14, 7, 23 | ipcl 21060 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
68 | 1, 5, 5, 67 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π , π) β πΎ) |
69 | 12, 14, 7, 23 | ipcl 21060 |
. . . . . . . . . . . 12
β’ ((π β PreHil β§ π β π β§ π β π) β (π , π) β πΎ) |
70 | 1, 6, 6, 69 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π , π) β πΎ) |
71 | 12, 23 | clmacl 24470 |
. . . . . . . . . . 11
β’ ((π β βMod β§ (π , π) β πΎ β§ (π , π) β πΎ) β ((π , π) + (π , π)) β πΎ) |
72 | 22, 68, 70, 71 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((π , π) + (π , π)) β πΎ) |
73 | 12, 23 | clmacl 24470 |
. . . . . . . . . . 11
β’ ((π β βMod β§ (π , π) β πΎ β§ (π , π) β πΎ) β ((π , π) + (π , π)) β πΎ) |
74 | 22, 27, 30, 73 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((π , π) + (π , π)) β πΎ) |
75 | 12, 23 | clmsub 24466 |
. . . . . . . . . 10
β’ ((π β βMod β§ ((π , π) + (π , π)) β πΎ β§ ((π , π) + (π , π)) β πΎ) β (((π , π) + (π , π)) β ((π , π) + (π , π))) = (((π , π) + (π , π))(-gβπΉ)((π , π) + (π , π)))) |
76 | 22, 72, 74, 75 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (((π , π) + (π , π)) β ((π , π) + (π , π))) = (((π , π) + (π , π))(-gβπΉ)((π , π) + (π , π)))) |
77 | | eqid 2733 |
. . . . . . . . . 10
β’
(-gβπΉ) = (-gβπΉ) |
78 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπΉ) = (+gβπΉ) |
79 | 12, 14, 7, 8, 77, 78, 1, 5, 6,
5, 6 | ip2subdi 21071 |
. . . . . . . . 9
β’ (π β ((π β π) , (π β π)) = (((π , π)(+gβπΉ)(π , π))(-gβπΉ)((π , π)(+gβπΉ)(π , π)))) |
80 | 66, 76, 79 | 3eqtr4rd 2784 |
. . . . . . . 8
β’ (π β ((π β π) , (π β π)) = (((π , π) + (π , π)) β ((π , π) + (π , π)))) |
81 | 80 | fveq2d 6850 |
. . . . . . 7
β’ (π β (absβ((π β π) , (π β π))) = (absβ(((π , π) + (π , π)) β ((π , π) + (π , π))))) |
82 | 61, 81 | eqtr3d 2775 |
. . . . . 6
β’ (π β ((π β π) , (π β π)) = (absβ(((π , π) + (π , π)) β ((π , π) + (π , π))))) |
83 | 25, 72 | sseldd 3949 |
. . . . . . 7
β’ (π β ((π , π) + (π , π)) β β) |
84 | 83, 32 | abs2dif2d 15352 |
. . . . . 6
β’ (π β (absβ(((π , π) + (π , π)) β ((π , π) + (π , π)))) β€ ((absβ((π , π) + (π , π))) + (absβ((π , π) + (π , π))))) |
85 | 82, 84 | eqbrtrd 5131 |
. . . . 5
β’ (π β ((π β π) , (π β π)) β€ ((absβ((π , π) + (π , π))) + (absβ((π , π) + (π , π))))) |
86 | 18, 20, 42, 47 | addge0d 11739 |
. . . . . . 7
β’ (π β 0 β€ ((π , π) + (π , π))) |
87 | 21, 86 | absidd 15316 |
. . . . . 6
β’ (π β (absβ((π , π) + (π , π))) = ((π , π) + (π , π))) |
88 | 87 | oveq1d 7376 |
. . . . 5
β’ (π β ((absβ((π , π) + (π , π))) + (absβ((π , π) + (π , π)))) = (((π , π) + (π , π)) + (absβ((π , π) + (π , π))))) |
89 | 85, 88 | breqtrd 5135 |
. . . 4
β’ (π β ((π β π) , (π β π)) β€ (((π , π) + (π , π)) + (absβ((π , π) + (π , π))))) |
90 | 28 | abscld 15330 |
. . . . . . . 8
β’ (π β (absβ(π , π)) β β) |
91 | | remulcl 11144 |
. . . . . . . 8
β’ ((2
β β β§ (absβ(π , π)) β β) β (2 Β·
(absβ(π , π))) β
β) |
92 | 36, 90, 91 | sylancr 588 |
. . . . . . 7
β’ (π β (2 Β·
(absβ(π , π))) β
β) |
93 | 28, 31 | abstrid 15350 |
. . . . . . . 8
β’ (π β (absβ((π , π) + (π , π))) β€ ((absβ(π , π)) + (absβ(π , π)))) |
94 | 90 | recnd 11191 |
. . . . . . . . . 10
β’ (π β (absβ(π , π)) β β) |
95 | 94 | 2timesd 12404 |
. . . . . . . . 9
β’ (π β (2 Β·
(absβ(π , π))) = ((absβ(π , π)) + (absβ(π , π)))) |
96 | 28 | abscjd 15344 |
. . . . . . . . . . 11
β’ (π β
(absβ(ββ(π , π))) = (absβ(π , π))) |
97 | 12 | clmcj 24462 |
. . . . . . . . . . . . . . 15
β’ (π β βMod β
β = (*πβπΉ)) |
98 | 22, 97 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β β =
(*πβπΉ)) |
99 | 98 | fveq1d 6848 |
. . . . . . . . . . . . 13
β’ (π β (ββ(π , π)) = ((*πβπΉ)β(π , π))) |
100 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(*πβπΉ) = (*πβπΉ) |
101 | 12, 14, 7, 100 | ipcj 21061 |
. . . . . . . . . . . . . 14
β’ ((π β PreHil β§ π β π β§ π β π) β ((*πβπΉ)β(π , π)) = (π , π)) |
102 | 1, 5, 6, 101 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β
((*πβπΉ)β(π , π)) = (π , π)) |
103 | 99, 102 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (ββ(π , π)) = (π , π)) |
104 | 103 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π β
(absβ(ββ(π , π))) = (absβ(π , π))) |
105 | 96, 104 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (π β (absβ(π , π)) = (absβ(π , π))) |
106 | 105 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β ((absβ(π , π)) + (absβ(π , π))) = ((absβ(π , π)) + (absβ(π , π)))) |
107 | 95, 106 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (2 Β·
(absβ(π , π))) = ((absβ(π , π)) + (absβ(π , π)))) |
108 | 93, 107 | breqtrrd 5137 |
. . . . . . 7
β’ (π β (absβ((π , π) + (π , π))) β€ (2 Β· (absβ(π , π)))) |
109 | | tcphcph.3 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) |
110 | | eqid 2733 |
. . . . . . . . . 10
β’
(normβπΊ) =
(normβπΊ) |
111 | | eqid 2733 |
. . . . . . . . . 10
β’ ((π , π) / (π , π)) = ((π , π) / (π , π)) |
112 | 11, 7, 12, 1, 13, 14, 109, 40, 23, 110, 111, 5, 6 | ipcau2 24621 |
. . . . . . . . 9
β’ (π β (absβ(π , π)) β€ (((normβπΊ)βπ) Β· ((normβπΊ)βπ))) |
113 | 11, 110, 7, 14 | tcphnmval 24616 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π β π) β ((normβπΊ)βπ) = (ββ(π , π))) |
114 | 4, 5, 113 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((normβπΊ)βπ) = (ββ(π , π))) |
115 | 11, 110, 7, 14 | tcphnmval 24616 |
. . . . . . . . . . 11
β’ ((π β Grp β§ π β π) β ((normβπΊ)βπ) = (ββ(π , π))) |
116 | 4, 6, 115 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((normβπΊ)βπ) = (ββ(π , π))) |
117 | 114, 116 | oveq12d 7379 |
. . . . . . . . 9
β’ (π β (((normβπΊ)βπ) Β· ((normβπΊ)βπ)) = ((ββ(π , π)) Β· (ββ(π , π)))) |
118 | 112, 117 | breqtrd 5135 |
. . . . . . . 8
β’ (π β (absβ(π , π)) β€ ((ββ(π , π)) Β· (ββ(π , π)))) |
119 | 36 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β
β) |
120 | | 2pos 12264 |
. . . . . . . . . 10
β’ 0 <
2 |
121 | 120 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 < 2) |
122 | | lemul2 12016 |
. . . . . . . . 9
β’
(((absβ(π
, π)) β β β§
((ββ(π , π)) Β·
(ββ(π , π))) β β β§ (2
β β β§ 0 < 2)) β ((absβ(π , π)) β€ ((ββ(π , π)) Β· (ββ(π , π))) β (2 Β· (absβ(π , π))) β€ (2 Β· ((ββ(π , π)) Β· (ββ(π , π)))))) |
123 | 90, 49, 119, 121, 122 | syl112anc 1375 |
. . . . . . . 8
β’ (π β ((absβ(π , π)) β€ ((ββ(π , π)) Β· (ββ(π , π))) β (2 Β· (absβ(π , π))) β€ (2 Β· ((ββ(π , π)) Β· (ββ(π , π)))))) |
124 | 118, 123 | mpbid 231 |
. . . . . . 7
β’ (π β (2 Β·
(absβ(π , π))) β€ (2 Β·
((ββ(π , π)) Β·
(ββ(π , π))))) |
125 | 33, 92, 51, 108, 124 | letrd 11320 |
. . . . . 6
β’ (π β (absβ((π , π) + (π , π))) β€ (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) |
126 | 33, 51, 21, 125 | leadd2dd 11778 |
. . . . 5
β’ (π β (((π , π) + (π , π)) + (absβ((π , π) + (π , π)))) β€ (((π , π) + (π , π)) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π)))))) |
127 | 126, 54 | breqtrrd 5137 |
. . . 4
β’ (π β (((π , π) + (π , π)) + (absβ((π , π) + (π , π)))) β€ (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π))) |
128 | 16, 34, 56, 89, 127 | letrd 11320 |
. . 3
β’ (π β ((π β π) , (π β π)) β€ (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π))) |
129 | 16 | recnd 11191 |
. . . 4
β’ (π β ((π β π) , (π β π)) β β) |
130 | 129 | sqsqrtd 15333 |
. . 3
β’ (π β ((ββ((π β π) , (π β π)))β2) = ((π β π) , (π β π))) |
131 | 35 | sqrtcld 15331 |
. . . . 5
β’ (π β (ββ(π , π)) β β) |
132 | 48 | recnd 11191 |
. . . . 5
β’ (π β (ββ(π , π)) β β) |
133 | | binom2 14130 |
. . . . 5
β’
(((ββ(π
, π)) β β β§
(ββ(π , π)) β β) β
(((ββ(π , π)) + (ββ(π , π)))β2) = ((((ββ(π , π))β2) + (2 Β·
((ββ(π , π)) Β·
(ββ(π , π))))) + ((ββ(π , π))β2))) |
134 | 131, 132,
133 | syl2anc 585 |
. . . 4
β’ (π β (((ββ(π , π)) + (ββ(π , π)))β2) = ((((ββ(π , π))β2) + (2 Β·
((ββ(π , π)) Β·
(ββ(π , π))))) + ((ββ(π , π))β2))) |
135 | 35 | sqsqrtd 15333 |
. . . . . 6
β’ (π β ((ββ(π , π))β2) = (π , π)) |
136 | 135 | oveq1d 7376 |
. . . . 5
β’ (π β (((ββ(π , π))β2) + (2 Β·
((ββ(π , π)) Β·
(ββ(π , π))))) = ((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π)))))) |
137 | 53 | sqsqrtd 15333 |
. . . . 5
β’ (π β ((ββ(π , π))β2) = (π , π)) |
138 | 136, 137 | oveq12d 7379 |
. . . 4
β’ (π β ((((ββ(π , π))β2) + (2 Β·
((ββ(π , π)) Β·
(ββ(π , π))))) + ((ββ(π , π))β2)) = (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π))) |
139 | 134, 138 | eqtrd 2773 |
. . 3
β’ (π β (((ββ(π , π)) + (ββ(π , π)))β2) = (((π , π) + (2 Β· ((ββ(π , π)) Β· (ββ(π , π))))) + (π , π))) |
140 | 128, 130,
139 | 3brtr4d 5141 |
. 2
β’ (π β ((ββ((π β π) , (π β π)))β2) β€ (((ββ(π , π)) + (ββ(π , π)))β2)) |
141 | 16, 60 | resqrtcld 15311 |
. . 3
β’ (π β (ββ((π β π) , (π β π))) β β) |
142 | 43, 48 | readdcld 11192 |
. . 3
β’ (π β ((ββ(π , π)) + (ββ(π , π))) β β) |
143 | 16, 60 | sqrtge0d 15314 |
. . 3
β’ (π β 0 β€
(ββ((π β π) , (π β π)))) |
144 | 18, 42 | sqrtge0d 15314 |
. . . 4
β’ (π β 0 β€
(ββ(π , π))) |
145 | 20, 47 | sqrtge0d 15314 |
. . . 4
β’ (π β 0 β€
(ββ(π , π))) |
146 | 43, 48, 144, 145 | addge0d 11739 |
. . 3
β’ (π β 0 β€
((ββ(π , π)) + (ββ(π , π)))) |
147 | 141, 142,
143, 146 | le2sqd 14169 |
. 2
β’ (π β ((ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π))) β ((ββ((π β π) , (π β π)))β2) β€ (((ββ(π , π)) + (ββ(π , π)))β2))) |
148 | 140, 147 | mpbird 257 |
1
β’ (π β (ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π)))) |