Step | Hyp | Ref
| Expression |
1 | | 4re 12242 |
. . . . . 6
β’ 4 β
β |
2 | | minvec.x |
. . . . . . . 8
β’ π = (Baseβπ) |
3 | | minvec.m |
. . . . . . . 8
β’ β =
(-gβπ) |
4 | | minvec.n |
. . . . . . . 8
β’ π = (normβπ) |
5 | | minvec.u |
. . . . . . . 8
β’ (π β π β βPreHil) |
6 | | minvec.y |
. . . . . . . 8
β’ (π β π β (LSubSpβπ)) |
7 | | minvec.w |
. . . . . . . 8
β’ (π β (π βΎs π) β CMetSp) |
8 | | minvec.a |
. . . . . . . 8
β’ (π β π΄ β π) |
9 | | minvec.j |
. . . . . . . 8
β’ π½ = (TopOpenβπ) |
10 | | minvec.r |
. . . . . . . 8
β’ π
= ran (π¦ β π β¦ (πβ(π΄ β π¦))) |
11 | | minvec.s |
. . . . . . . 8
β’ π = inf(π
, β, < ) |
12 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | minveclem4c 24805 |
. . . . . . 7
β’ (π β π β β) |
13 | 12 | resqcld 14036 |
. . . . . 6
β’ (π β (πβ2) β β) |
14 | | remulcl 11141 |
. . . . . 6
β’ ((4
β β β§ (πβ2) β β) β (4 Β·
(πβ2)) β
β) |
15 | 1, 13, 14 | sylancr 588 |
. . . . 5
β’ (π β (4 Β· (πβ2)) β
β) |
16 | | cphngp 24553 |
. . . . . . . . . 10
β’ (π β βPreHil β
π β
NrmGrp) |
17 | 5, 16 | syl 17 |
. . . . . . . . 9
β’ (π β π β NrmGrp) |
18 | | ngpms 23972 |
. . . . . . . . 9
β’ (π β NrmGrp β π β MetSp) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
β’ (π β π β MetSp) |
20 | | minvec.d |
. . . . . . . . 9
β’ π· = ((distβπ) βΎ (π Γ π)) |
21 | 2, 20 | msmet 23826 |
. . . . . . . 8
β’ (π β MetSp β π· β (Metβπ)) |
22 | 19, 21 | syl 17 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
23 | | eqid 2733 |
. . . . . . . . . 10
β’
(LSubSpβπ) =
(LSubSpβπ) |
24 | 2, 23 | lssss 20412 |
. . . . . . . . 9
β’ (π β (LSubSpβπ) β π β π) |
25 | 6, 24 | syl 17 |
. . . . . . . 8
β’ (π β π β π) |
26 | | minveclem2.3 |
. . . . . . . 8
β’ (π β πΎ β π) |
27 | 25, 26 | sseldd 3946 |
. . . . . . 7
β’ (π β πΎ β π) |
28 | | minveclem2.4 |
. . . . . . . 8
β’ (π β πΏ β π) |
29 | 25, 28 | sseldd 3946 |
. . . . . . 7
β’ (π β πΏ β π) |
30 | | metcl 23701 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ πΎ β π β§ πΏ β π) β (πΎπ·πΏ) β β) |
31 | 22, 27, 29, 30 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΎπ·πΏ) β β) |
32 | 31 | resqcld 14036 |
. . . . 5
β’ (π β ((πΎπ·πΏ)β2) β β) |
33 | 15, 32 | readdcld 11189 |
. . . 4
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β β) |
34 | | cphlmod 24554 |
. . . . . . . . . 10
β’ (π β βPreHil β
π β
LMod) |
35 | 5, 34 | syl 17 |
. . . . . . . . 9
β’ (π β π β LMod) |
36 | | cphclm 24569 |
. . . . . . . . . . . . . . 15
β’ (π β βPreHil β
π β
βMod) |
37 | 5, 36 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β βMod) |
38 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Scalarβπ) =
(Scalarβπ) |
39 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
40 | 38, 39 | clmzss 24457 |
. . . . . . . . . . . . . 14
β’ (π β βMod β
β€ β (Baseβ(Scalarβπ))) |
41 | 37, 40 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β€ β
(Baseβ(Scalarβπ))) |
42 | | 2z 12540 |
. . . . . . . . . . . . . 14
β’ 2 β
β€ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 2 β
β€) |
44 | 41, 43 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (π β 2 β
(Baseβ(Scalarβπ))) |
45 | | 2ne0 12262 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
46 | 45 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β 0) |
47 | 38, 39 | cphreccl 24561 |
. . . . . . . . . . . 12
β’ ((π β βPreHil β§ 2
β (Baseβ(Scalarβπ)) β§ 2 β 0) β (1 / 2) β
(Baseβ(Scalarβπ))) |
48 | 5, 44, 46, 47 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (1 / 2) β
(Baseβ(Scalarβπ))) |
49 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(+gβπ) = (+gβπ) |
50 | 49, 23 | lssvacl 20430 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β (LSubSpβπ)) β§ (πΎ β π β§ πΏ β π)) β (πΎ(+gβπ)πΏ) β π) |
51 | 35, 6, 26, 28, 50 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β (πΎ(+gβπ)πΏ) β π) |
52 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (
Β·π βπ) = ( Β·π
βπ) |
53 | 38, 52, 39, 23 | lssvscl 20431 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β (LSubSpβπ)) β§ ((1 / 2) β
(Baseβ(Scalarβπ)) β§ (πΎ(+gβπ)πΏ) β π)) β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β π) |
54 | 35, 6, 48, 51, 53 | syl22anc 838 |
. . . . . . . . . 10
β’ (π β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β π) |
55 | 25, 54 | sseldd 3946 |
. . . . . . . . 9
β’ (π β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β π) |
56 | 2, 3 | lmodvsubcl 20382 |
. . . . . . . . 9
β’ ((π β LMod β§ π΄ β π β§ ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β π) β (π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))) β π) |
57 | 35, 8, 55, 56 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))) β π) |
58 | 2, 4 | nmcl 23988 |
. . . . . . . 8
β’ ((π β NrmGrp β§ (π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))) β π) β (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β β) |
59 | 17, 57, 58 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β β) |
60 | 59 | resqcld 14036 |
. . . . . 6
β’ (π β ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β
β) |
61 | | remulcl 11141 |
. . . . . 6
β’ ((4
β β β§ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β β) β (4
Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) β
β) |
62 | 1, 60, 61 | sylancr 588 |
. . . . 5
β’ (π β (4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) β
β) |
63 | 62, 32 | readdcld 11189 |
. . . 4
β’ (π β ((4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) β β) |
64 | | minveclem2.1 |
. . . . . 6
β’ (π β π΅ β β) |
65 | 13, 64 | readdcld 11189 |
. . . . 5
β’ (π β ((πβ2) + π΅) β β) |
66 | | remulcl 11141 |
. . . . 5
β’ ((4
β β β§ ((πβ2) + π΅) β β) β (4 Β· ((πβ2) + π΅)) β β) |
67 | 1, 65, 66 | sylancr 588 |
. . . 4
β’ (π β (4 Β· ((πβ2) + π΅)) β β) |
68 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | minveclem1 24804 |
. . . . . . . . . 10
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
69 | 68 | simp3d 1145 |
. . . . . . . . 9
β’ (π β βπ€ β π
0 β€ π€) |
70 | 68 | simp1d 1143 |
. . . . . . . . . 10
β’ (π β π
β β) |
71 | 68 | simp2d 1144 |
. . . . . . . . . 10
β’ (π β π
β β
) |
72 | | 0re 11162 |
. . . . . . . . . . 11
β’ 0 β
β |
73 | | breq1 5109 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
74 | 73 | ralbidv 3171 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
75 | 74 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
76 | 72, 69, 75 | sylancr 588 |
. . . . . . . . . 10
β’ (π β βπ₯ β β βπ€ β π
π₯ β€ π€) |
77 | 72 | a1i 11 |
. . . . . . . . . 10
β’ (π β 0 β
β) |
78 | | infregelb 12144 |
. . . . . . . . . 10
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
79 | 70, 71, 76, 77, 78 | syl31anc 1374 |
. . . . . . . . 9
β’ (π β (0 β€ inf(π
, β, < ) β
βπ€ β π
0 β€ π€)) |
80 | 69, 79 | mpbird 257 |
. . . . . . . 8
β’ (π β 0 β€ inf(π
, β, <
)) |
81 | 80, 11 | breqtrrdi 5148 |
. . . . . . 7
β’ (π β 0 β€ π) |
82 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
83 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β (π΄ β π¦) = (π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
84 | 83 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π¦ = ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)) β (πβ(π΄ β π¦)) = (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
85 | 84 | rspceeqv 3596 |
. . . . . . . . . . . 12
β’ ((((1 /
2)( Β·π βπ)(πΎ(+gβπ)πΏ)) β π β§ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) β βπ¦ β π (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = (πβ(π΄ β π¦))) |
86 | 54, 82, 85 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β βπ¦ β π (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = (πβ(π΄ β π¦))) |
87 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β π β¦ (πβ(π΄ β π¦))) = (π¦ β π β¦ (πβ(π΄ β π¦))) |
88 | | fvex 6856 |
. . . . . . . . . . . 12
β’ (πβ(π΄ β π¦)) β V |
89 | 87, 88 | elrnmpti 5916 |
. . . . . . . . . . 11
β’ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β ran (π¦ β π β¦ (πβ(π΄ β π¦))) β βπ¦ β π (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = (πβ(π΄ β π¦))) |
90 | 86, 89 | sylibr 233 |
. . . . . . . . . 10
β’ (π β (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β ran (π¦ β π β¦ (πβ(π΄ β π¦)))) |
91 | 90, 10 | eleqtrrdi 2845 |
. . . . . . . . 9
β’ (π β (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β π
) |
92 | | infrelb 12145 |
. . . . . . . . 9
β’ ((π
β β β§
βπ₯ β β
βπ€ β π
π₯ β€ π€ β§ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β π
) β inf(π
, β, < ) β€ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
93 | 70, 76, 91, 92 | syl3anc 1372 |
. . . . . . . 8
β’ (π β inf(π
, β, < ) β€ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
94 | 11, 93 | eqbrtrid 5141 |
. . . . . . 7
β’ (π β π β€ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
95 | | le2sq2 14046 |
. . . . . . 7
β’ (((π β β β§ 0 β€
π) β§ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β β β§ π β€ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))) β (πβ2) β€ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) |
96 | 12, 81, 59, 94, 95 | syl22anc 838 |
. . . . . 6
β’ (π β (πβ2) β€ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) |
97 | | 4pos 12265 |
. . . . . . . . 9
β’ 0 <
4 |
98 | 1, 97 | pm3.2i 472 |
. . . . . . . 8
β’ (4 β
β β§ 0 < 4) |
99 | | lemul2 12013 |
. . . . . . . 8
β’ (((πβ2) β β β§
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β β β§ (4 β
β β§ 0 < 4)) β ((πβ2) β€ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)))) |
100 | 98, 99 | mp3an3 1451 |
. . . . . . 7
β’ (((πβ2) β β β§
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β β) β ((πβ2) β€ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)))) |
101 | 13, 60, 100 | syl2anc 585 |
. . . . . 6
β’ (π β ((πβ2) β€ ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)))) |
102 | 96, 101 | mpbid 231 |
. . . . 5
β’ (π β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2))) |
103 | 15, 62, 32, 102 | leadd1dd 11774 |
. . . 4
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) + ((πΎπ·πΏ)β2))) |
104 | | metcl 23701 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π΄ β π β§ πΎ β π) β (π΄π·πΎ) β β) |
105 | 22, 8, 27, 104 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΎ) β β) |
106 | 105 | resqcld 14036 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) β β) |
107 | | metcl 23701 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π΄ β π β§ πΏ β π) β (π΄π·πΏ) β β) |
108 | 22, 8, 29, 107 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΏ) β β) |
109 | 108 | resqcld 14036 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) β β) |
110 | | minveclem2.5 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) β€ ((πβ2) + π΅)) |
111 | | minveclem2.6 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) β€ ((πβ2) + π΅)) |
112 | 106, 109,
65, 65, 110, 111 | le2addd 11779 |
. . . . . . 7
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (((πβ2) + π΅) + ((πβ2) + π΅))) |
113 | 65 | recnd 11188 |
. . . . . . . 8
β’ (π β ((πβ2) + π΅) β β) |
114 | 113 | 2timesd 12401 |
. . . . . . 7
β’ (π β (2 Β· ((πβ2) + π΅)) = (((πβ2) + π΅) + ((πβ2) + π΅))) |
115 | 112, 114 | breqtrrd 5134 |
. . . . . 6
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (2 Β· ((πβ2) + π΅))) |
116 | 106, 109 | readdcld 11189 |
. . . . . . 7
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β β) |
117 | | 2re 12232 |
. . . . . . . 8
β’ 2 β
β |
118 | | remulcl 11141 |
. . . . . . . 8
β’ ((2
β β β§ ((πβ2) + π΅) β β) β (2 Β· ((πβ2) + π΅)) β β) |
119 | 117, 65, 118 | sylancr 588 |
. . . . . . 7
β’ (π β (2 Β· ((πβ2) + π΅)) β β) |
120 | | 2pos 12261 |
. . . . . . . . 9
β’ 0 <
2 |
121 | 117, 120 | pm3.2i 472 |
. . . . . . . 8
β’ (2 β
β β§ 0 < 2) |
122 | | lemul2 12013 |
. . . . . . . 8
β’
(((((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β β β§ (2 Β·
((πβ2) + π΅)) β β β§ (2
β β β§ 0 < 2)) β ((((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (2 Β· ((πβ2) + π΅)) β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) β€ (2 Β· (2 Β·
((πβ2) + π΅))))) |
123 | 121, 122 | mp3an3 1451 |
. . . . . . 7
β’
(((((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β β β§ (2 Β·
((πβ2) + π΅)) β β) β
((((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (2 Β· ((πβ2) + π΅)) β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) β€ (2 Β· (2 Β·
((πβ2) + π΅))))) |
124 | 116, 119,
123 | syl2anc 585 |
. . . . . 6
β’ (π β ((((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (2 Β· ((πβ2) + π΅)) β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) β€ (2 Β· (2 Β·
((πβ2) + π΅))))) |
125 | 115, 124 | mpbid 231 |
. . . . 5
β’ (π β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) β€ (2 Β· (2 Β·
((πβ2) + π΅)))) |
126 | 2, 3 | lmodvsubcl 20382 |
. . . . . . . 8
β’ ((π β LMod β§ π΄ β π β§ πΎ β π) β (π΄ β πΎ) β π) |
127 | 35, 8, 27, 126 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄ β πΎ) β π) |
128 | 2, 3 | lmodvsubcl 20382 |
. . . . . . . 8
β’ ((π β LMod β§ π΄ β π β§ πΏ β π) β (π΄ β πΏ) β π) |
129 | 35, 8, 29, 128 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄ β πΏ) β π) |
130 | 2, 49, 3, 4 | nmpar 24620 |
. . . . . . 7
β’ ((π β βPreHil β§
(π΄ β πΎ) β π β§ (π΄ β πΏ) β π) β (((πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))β2) + ((πβ((π΄ β πΎ) β (π΄ β πΏ)))β2)) = (2 Β· (((πβ(π΄ β πΎ))β2) + ((πβ(π΄ β πΏ))β2)))) |
131 | 5, 127, 129, 130 | syl3anc 1372 |
. . . . . 6
β’ (π β (((πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))β2) + ((πβ((π΄ β πΎ) β (π΄ β πΏ)))β2)) = (2 Β· (((πβ(π΄ β πΎ))β2) + ((πβ(π΄ β πΏ))β2)))) |
132 | | 2cn 12233 |
. . . . . . . . . 10
β’ 2 β
β |
133 | 59 | recnd 11188 |
. . . . . . . . . 10
β’ (π β (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β β) |
134 | | sqmul 14030 |
. . . . . . . . . 10
β’ ((2
β β β§ (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) β β) β ((2 Β·
(πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))β2) = ((2β2) Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2))) |
135 | 132, 133,
134 | sylancr 588 |
. . . . . . . . 9
β’ (π β ((2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))β2) = ((2β2) Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2))) |
136 | | sq2 14107 |
. . . . . . . . . 10
β’
(2β2) = 4 |
137 | 136 | oveq1i 7368 |
. . . . . . . . 9
β’
((2β2) Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) = (4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) |
138 | 135, 137 | eqtrdi 2789 |
. . . . . . . 8
β’ (π β ((2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))β2) = (4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2))) |
139 | 2, 4, 52, 38, 39 | cphnmvs 24570 |
. . . . . . . . . . . 12
β’ ((π β βPreHil β§ 2
β (Baseβ(Scalarβπ)) β§ (π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))) β π) β (πβ(2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = ((absβ2) Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))) |
140 | 5, 44, 57, 139 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (πβ(2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = ((absβ2) Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))) |
141 | | 0le2 12260 |
. . . . . . . . . . . . 13
β’ 0 β€
2 |
142 | | absid 15187 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ 0 β€ 2) β (absβ2) = 2) |
143 | 117, 141,
142 | mp2an 691 |
. . . . . . . . . . . 12
β’
(absβ2) = 2 |
144 | 143 | oveq1i 7368 |
. . . . . . . . . . 11
β’
((absβ2) Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = (2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
145 | 140, 144 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β (πβ(2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = (2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))) |
146 | 2, 52, 38, 39, 3, 35, 44, 8, 55 | lmodsubdi 20394 |
. . . . . . . . . . . 12
β’ (π β (2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = ((2(
Β·π βπ)π΄) β (2(
Β·π βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
147 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(.gβπ) = (.gβπ) |
148 | 2, 147, 49 | mulg2 18890 |
. . . . . . . . . . . . . . 15
β’ (π΄ β π β (2(.gβπ)π΄) = (π΄(+gβπ)π΄)) |
149 | 8, 148 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β
(2(.gβπ)π΄) = (π΄(+gβπ)π΄)) |
150 | 2, 147, 52 | clmmulg 24480 |
. . . . . . . . . . . . . . 15
β’ ((π β βMod β§ 2
β β€ β§ π΄
β π) β
(2(.gβπ)π΄) = (2( Β·π
βπ)π΄)) |
151 | 37, 43, 8, 150 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β
(2(.gβπ)π΄) = (2( Β·π
βπ)π΄)) |
152 | 149, 151 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ (π β (π΄(+gβπ)π΄) = (2( Β·π
βπ)π΄)) |
153 | 2, 49 | lmodvacl 20351 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ πΎ β π β§ πΏ β π) β (πΎ(+gβπ)πΏ) β π) |
154 | 35, 27, 29, 153 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (πΎ(+gβπ)πΏ) β π) |
155 | 2, 52 | clmvs1 24472 |
. . . . . . . . . . . . . . 15
β’ ((π β βMod β§ (πΎ(+gβπ)πΏ) β π) β (1(
Β·π βπ)(πΎ(+gβπ)πΏ)) = (πΎ(+gβπ)πΏ)) |
156 | 37, 154, 155 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (1(
Β·π βπ)(πΎ(+gβπ)πΏ)) = (πΎ(+gβπ)πΏ)) |
157 | 132, 45 | recidi 11891 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· (1 / 2)) = 1 |
158 | 157 | oveq1i 7368 |
. . . . . . . . . . . . . . 15
β’ ((2
Β· (1 / 2))( Β·π βπ)(πΎ(+gβπ)πΏ)) = (1( Β·π
βπ)(πΎ(+gβπ)πΏ)) |
159 | 2, 38, 52, 39 | clmvsass 24468 |
. . . . . . . . . . . . . . . 16
β’ ((π β βMod β§ (2
β (Baseβ(Scalarβπ)) β§ (1 / 2) β
(Baseβ(Scalarβπ)) β§ (πΎ(+gβπ)πΏ) β π)) β ((2 Β· (1 / 2))(
Β·π βπ)(πΎ(+gβπ)πΏ)) = (2( Β·π
βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
160 | 37, 44, 48, 154, 159 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (π β ((2 Β· (1 / 2))(
Β·π βπ)(πΎ(+gβπ)πΏ)) = (2( Β·π
βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
161 | 158, 160 | eqtr3id 2787 |
. . . . . . . . . . . . . 14
β’ (π β (1(
Β·π βπ)(πΎ(+gβπ)πΏ)) = (2( Β·π
βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
162 | 156, 161 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ (π β (πΎ(+gβπ)πΏ) = (2( Β·π
βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) |
163 | 152, 162 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π β ((π΄(+gβπ)π΄) β (πΎ(+gβπ)πΏ)) = ((2(
Β·π βπ)π΄) β (2(
Β·π βπ)((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) |
164 | | lmodabl 20384 |
. . . . . . . . . . . . . 14
β’ (π β LMod β π β Abel) |
165 | 35, 164 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β Abel) |
166 | 2, 49, 3 | ablsub4 19596 |
. . . . . . . . . . . . 13
β’ ((π β Abel β§ (π΄ β π β§ π΄ β π) β§ (πΎ β π β§ πΏ β π)) β ((π΄(+gβπ)π΄) β (πΎ(+gβπ)πΏ)) = ((π΄ β πΎ)(+gβπ)(π΄ β πΏ))) |
167 | 165, 8, 8, 27, 29, 166 | syl122anc 1380 |
. . . . . . . . . . . 12
β’ (π β ((π΄(+gβπ)π΄) β (πΎ(+gβπ)πΏ)) = ((π΄ β πΎ)(+gβπ)(π΄ β πΏ))) |
168 | 146, 163,
167 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (π β (2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))) = ((π΄ β πΎ)(+gβπ)(π΄ β πΏ))) |
169 | 168 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π β (πβ(2(
Β·π βπ)(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = (πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))) |
170 | 145, 169 | eqtr3d 2775 |
. . . . . . . . 9
β’ (π β (2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))) = (πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))) |
171 | 170 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((2 Β· (πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ)))))β2) = ((πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))β2)) |
172 | 138, 171 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) = ((πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))β2)) |
173 | | eqid 2733 |
. . . . . . . . . . 11
β’
(distβπ) =
(distβπ) |
174 | 4, 2, 3, 173 | ngpdsr 23977 |
. . . . . . . . . 10
β’ ((π β NrmGrp β§ πΎ β π β§ πΏ β π) β (πΎ(distβπ)πΏ) = (πβ(πΏ β πΎ))) |
175 | 17, 27, 29, 174 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΎ(distβπ)πΏ) = (πβ(πΏ β πΎ))) |
176 | 20 | oveqi 7371 |
. . . . . . . . . 10
β’ (πΎπ·πΏ) = (πΎ((distβπ) βΎ (π Γ π))πΏ) |
177 | 27, 29 | ovresd 7522 |
. . . . . . . . . 10
β’ (π β (πΎ((distβπ) βΎ (π Γ π))πΏ) = (πΎ(distβπ)πΏ)) |
178 | 176, 177 | eqtrid 2785 |
. . . . . . . . 9
β’ (π β (πΎπ·πΏ) = (πΎ(distβπ)πΏ)) |
179 | 2, 3, 165, 8, 27, 29 | ablnnncan1 19607 |
. . . . . . . . . 10
β’ (π β ((π΄ β πΎ) β (π΄ β πΏ)) = (πΏ β πΎ)) |
180 | 179 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β (πβ((π΄ β πΎ) β (π΄ β πΏ))) = (πβ(πΏ β πΎ))) |
181 | 175, 178,
180 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (π β (πΎπ·πΏ) = (πβ((π΄ β πΎ) β (π΄ β πΏ)))) |
182 | 181 | oveq1d 7373 |
. . . . . . 7
β’ (π β ((πΎπ·πΏ)β2) = ((πβ((π΄ β πΎ) β (π΄ β πΏ)))β2)) |
183 | 172, 182 | oveq12d 7376 |
. . . . . 6
β’ (π β ((4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) = (((πβ((π΄ β πΎ)(+gβπ)(π΄ β πΏ)))β2) + ((πβ((π΄ β πΎ) β (π΄ β πΏ)))β2))) |
184 | 20 | oveqi 7371 |
. . . . . . . . . . 11
β’ (π΄π·πΎ) = (π΄((distβπ) βΎ (π Γ π))πΎ) |
185 | 8, 27 | ovresd 7522 |
. . . . . . . . . . 11
β’ (π β (π΄((distβπ) βΎ (π Γ π))πΎ) = (π΄(distβπ)πΎ)) |
186 | 184, 185 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β (π΄π·πΎ) = (π΄(distβπ)πΎ)) |
187 | 4, 2, 3, 173 | ngpds 23976 |
. . . . . . . . . . 11
β’ ((π β NrmGrp β§ π΄ β π β§ πΎ β π) β (π΄(distβπ)πΎ) = (πβ(π΄ β πΎ))) |
188 | 17, 8, 27, 187 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π΄(distβπ)πΎ) = (πβ(π΄ β πΎ))) |
189 | 186, 188 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (π΄π·πΎ) = (πβ(π΄ β πΎ))) |
190 | 189 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) = ((πβ(π΄ β πΎ))β2)) |
191 | 20 | oveqi 7371 |
. . . . . . . . . . 11
β’ (π΄π·πΏ) = (π΄((distβπ) βΎ (π Γ π))πΏ) |
192 | 8, 29 | ovresd 7522 |
. . . . . . . . . . 11
β’ (π β (π΄((distβπ) βΎ (π Γ π))πΏ) = (π΄(distβπ)πΏ)) |
193 | 191, 192 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β (π΄π·πΏ) = (π΄(distβπ)πΏ)) |
194 | 4, 2, 3, 173 | ngpds 23976 |
. . . . . . . . . . 11
β’ ((π β NrmGrp β§ π΄ β π β§ πΏ β π) β (π΄(distβπ)πΏ) = (πβ(π΄ β πΏ))) |
195 | 17, 8, 29, 194 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π΄(distβπ)πΏ) = (πβ(π΄ β πΏ))) |
196 | 193, 195 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (π΄π·πΏ) = (πβ(π΄ β πΏ))) |
197 | 196 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) = ((πβ(π΄ β πΏ))β2)) |
198 | 190, 197 | oveq12d 7376 |
. . . . . . 7
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) = (((πβ(π΄ β πΎ))β2) + ((πβ(π΄ β πΏ))β2))) |
199 | 198 | oveq2d 7374 |
. . . . . 6
β’ (π β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) = (2 Β· (((πβ(π΄ β πΎ))β2) + ((πβ(π΄ β πΏ))β2)))) |
200 | 131, 183,
199 | 3eqtr4d 2783 |
. . . . 5
β’ (π β ((4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) = (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)))) |
201 | | 2t2e4 12322 |
. . . . . . 7
β’ (2
Β· 2) = 4 |
202 | 201 | oveq1i 7368 |
. . . . . 6
β’ ((2
Β· 2) Β· ((πβ2) + π΅)) = (4 Β· ((πβ2) + π΅)) |
203 | | 2cnd 12236 |
. . . . . . 7
β’ (π β 2 β
β) |
204 | 203, 203,
113 | mulassd 11183 |
. . . . . 6
β’ (π β ((2 Β· 2) Β·
((πβ2) + π΅)) = (2 Β· (2 Β·
((πβ2) + π΅)))) |
205 | 202, 204 | eqtr3id 2787 |
. . . . 5
β’ (π β (4 Β· ((πβ2) + π΅)) = (2 Β· (2 Β· ((πβ2) + π΅)))) |
206 | 125, 200,
205 | 3brtr4d 5138 |
. . . 4
β’ (π β ((4 Β· ((πβ(π΄ β ((1 / 2)(
Β·π βπ)(πΎ(+gβπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) β€ (4 Β· ((πβ2) + π΅))) |
207 | 33, 63, 67, 103, 206 | letrd 11317 |
. . 3
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ (4 Β· ((πβ2) + π΅))) |
208 | | 4cn 12243 |
. . . . 5
β’ 4 β
β |
209 | 208 | a1i 11 |
. . . 4
β’ (π β 4 β
β) |
210 | 13 | recnd 11188 |
. . . 4
β’ (π β (πβ2) β β) |
211 | 64 | recnd 11188 |
. . . 4
β’ (π β π΅ β β) |
212 | 209, 210,
211 | adddid 11184 |
. . 3
β’ (π β (4 Β· ((πβ2) + π΅)) = ((4 Β· (πβ2)) + (4 Β· π΅))) |
213 | 207, 212 | breqtrd 5132 |
. 2
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· (πβ2)) + (4 Β· π΅))) |
214 | | remulcl 11141 |
. . . 4
β’ ((4
β β β§ π΅
β β) β (4 Β· π΅) β β) |
215 | 1, 64, 214 | sylancr 588 |
. . 3
β’ (π β (4 Β· π΅) β
β) |
216 | 32, 215, 15 | leadd2d 11755 |
. 2
β’ (π β (((πΎπ·πΏ)β2) β€ (4 Β· π΅) β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· (πβ2)) + (4 Β· π΅)))) |
217 | 213, 216 | mpbird 257 |
1
β’ (π β ((πΎπ·πΏ)β2) β€ (4 Β· π΅)) |