Step | Hyp | Ref
| Expression |
1 | | 4re 12242 |
. . . . . 6
β’ 4 β
β |
2 | | minveco.s |
. . . . . . . 8
β’ π = inf(π
, β, < ) |
3 | | minveco.x |
. . . . . . . . . . 11
β’ π = (BaseSetβπ) |
4 | | minveco.m |
. . . . . . . . . . 11
β’ π = ( βπ£
βπ) |
5 | | minveco.n |
. . . . . . . . . . 11
β’ π =
(normCVβπ) |
6 | | minveco.y |
. . . . . . . . . . 11
β’ π = (BaseSetβπ) |
7 | | minveco.u |
. . . . . . . . . . 11
β’ (π β π β
CPreHilOLD) |
8 | | minveco.w |
. . . . . . . . . . 11
β’ (π β π β ((SubSpβπ) β© CBan)) |
9 | | minveco.a |
. . . . . . . . . . 11
β’ (π β π΄ β π) |
10 | | minveco.d |
. . . . . . . . . . 11
β’ π· = (IndMetβπ) |
11 | | minveco.j |
. . . . . . . . . . 11
β’ π½ = (MetOpenβπ·) |
12 | | minveco.r |
. . . . . . . . . . 11
β’ π
= ran (π¦ β π β¦ (πβ(π΄ππ¦))) |
13 | 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | minvecolem1 29858 |
. . . . . . . . . 10
β’ (π β (π
β β β§ π
β β
β§ βπ€ β π
0 β€ π€)) |
14 | 13 | simp1d 1143 |
. . . . . . . . 9
β’ (π β π
β β) |
15 | 13 | simp2d 1144 |
. . . . . . . . 9
β’ (π β π
β β
) |
16 | | 0re 11162 |
. . . . . . . . . 10
β’ 0 β
β |
17 | 13 | simp3d 1145 |
. . . . . . . . . 10
β’ (π β βπ€ β π
0 β€ π€) |
18 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (π₯ β€ π€ β 0 β€ π€)) |
19 | 18 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (βπ€ β π
π₯ β€ π€ β βπ€ β π
0 β€ π€)) |
20 | 19 | rspcev 3580 |
. . . . . . . . . 10
β’ ((0
β β β§ βπ€ β π
0 β€ π€) β βπ₯ β β βπ€ β π
π₯ β€ π€) |
21 | 16, 17, 20 | sylancr 588 |
. . . . . . . . 9
β’ (π β βπ₯ β β βπ€ β π
π₯ β€ π€) |
22 | | infrecl 12142 |
. . . . . . . . 9
β’ ((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β inf(π
, β, < ) β
β) |
23 | 14, 15, 21, 22 | syl3anc 1372 |
. . . . . . . 8
β’ (π β inf(π
, β, < ) β
β) |
24 | 2, 23 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π β β) |
25 | 24 | resqcld 14036 |
. . . . . 6
β’ (π β (πβ2) β β) |
26 | | remulcl 11141 |
. . . . . 6
β’ ((4
β β β§ (πβ2) β β) β (4 Β·
(πβ2)) β
β) |
27 | 1, 25, 26 | sylancr 588 |
. . . . 5
β’ (π β (4 Β· (πβ2)) β
β) |
28 | | phnv 29798 |
. . . . . . . . 9
β’ (π β CPreHilOLD
β π β
NrmCVec) |
29 | 7, 28 | syl 17 |
. . . . . . . 8
β’ (π β π β NrmCVec) |
30 | 3, 10 | imsmet 29675 |
. . . . . . . 8
β’ (π β NrmCVec β π· β (Metβπ)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
32 | | inss1 4189 |
. . . . . . . . . 10
β’
((SubSpβπ)
β© CBan) β (SubSpβπ) |
33 | 32, 8 | sselid 3943 |
. . . . . . . . 9
β’ (π β π β (SubSpβπ)) |
34 | | eqid 2733 |
. . . . . . . . . 10
β’
(SubSpβπ) =
(SubSpβπ) |
35 | 3, 6, 34 | sspba 29711 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β π) |
36 | 29, 33, 35 | syl2anc 585 |
. . . . . . . 8
β’ (π β π β π) |
37 | | minvecolem2.3 |
. . . . . . . 8
β’ (π β πΎ β π) |
38 | 36, 37 | sseldd 3946 |
. . . . . . 7
β’ (π β πΎ β π) |
39 | | minvecolem2.4 |
. . . . . . . 8
β’ (π β πΏ β π) |
40 | 36, 39 | sseldd 3946 |
. . . . . . 7
β’ (π β πΏ β π) |
41 | | metcl 23701 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ πΎ β π β§ πΏ β π) β (πΎπ·πΏ) β β) |
42 | 31, 38, 40, 41 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΎπ·πΏ) β β) |
43 | 42 | resqcld 14036 |
. . . . 5
β’ (π β ((πΎπ·πΏ)β2) β β) |
44 | 27, 43 | readdcld 11189 |
. . . 4
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β β) |
45 | | ax-1cn 11114 |
. . . . . . . . . . . . 13
β’ 1 β
β |
46 | | halfcl 12383 |
. . . . . . . . . . . . 13
β’ (1 β
β β (1 / 2) β β) |
47 | 45, 46 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β (1 / 2) β
β) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (
+π£ βπ) = ( +π£ βπ) |
49 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (
+π£ βπ) = ( +π£ βπ) |
50 | 6, 48, 49, 34 | sspgval 29713 |
. . . . . . . . . . . . . 14
β’ (((π β NrmCVec β§ π β (SubSpβπ)) β§ (πΎ β π β§ πΏ β π)) β (πΎ( +π£ βπ)πΏ) = (πΎ( +π£ βπ)πΏ)) |
51 | 29, 33, 37, 39, 50 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ (π β (πΎ( +π£ βπ)πΏ) = (πΎ( +π£ βπ)πΏ)) |
52 | 34 | sspnv 29710 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ π β (SubSpβπ)) β π β NrmCVec) |
53 | 29, 33, 52 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π β NrmCVec) |
54 | 6, 49 | nvgcl 29604 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ πΎ β π β§ πΏ β π) β (πΎ( +π£ βπ)πΏ) β π) |
55 | 53, 37, 39, 54 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (πΎ( +π£ βπ)πΏ) β π) |
56 | 51, 55 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’ (π β (πΎ( +π£ βπ)πΏ) β π) |
57 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
58 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
59 | 6, 57, 58, 34 | sspsval 29715 |
. . . . . . . . . . . 12
β’ (((π β NrmCVec β§ π β (SubSpβπ)) β§ ((1 / 2) β β
β§ (πΎ(
+π£ βπ)πΏ) β π)) β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) |
60 | 29, 33, 47, 56, 59 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) |
61 | 6, 58 | nvscl 29610 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ (1 / 2)
β β β§ (πΎ(
+π£ βπ)πΏ) β π) β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π) |
62 | 53, 47, 56, 61 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π) |
63 | 60, 62 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (π β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π) |
64 | 36, 63 | sseldd 3946 |
. . . . . . . . 9
β’ (π β ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π) |
65 | 3, 4 | nvmcl 29630 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π΄ β π β§ ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π) β (π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) β π) |
66 | 29, 9, 64, 65 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) β π) |
67 | 3, 5 | nvcl 29645 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) β π) β (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β β) |
68 | 29, 66, 67 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β β) |
69 | 68 | resqcld 14036 |
. . . . . 6
β’ (π β ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β
β) |
70 | | remulcl 11141 |
. . . . . 6
β’ ((4
β β β§ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β β) β (4
Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) β
β) |
71 | 1, 69, 70 | sylancr 588 |
. . . . 5
β’ (π β (4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) β
β) |
72 | 71, 43 | readdcld 11189 |
. . . 4
β’ (π β ((4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) β β) |
73 | | minvecolem2.1 |
. . . . . 6
β’ (π β π΅ β β) |
74 | 25, 73 | readdcld 11189 |
. . . . 5
β’ (π β ((πβ2) + π΅) β β) |
75 | | remulcl 11141 |
. . . . 5
β’ ((4
β β β§ ((πβ2) + π΅) β β) β (4 Β· ((πβ2) + π΅)) β β) |
76 | 1, 74, 75 | sylancr 588 |
. . . 4
β’ (π β (4 Β· ((πβ2) + π΅)) β β) |
77 | 16 | a1i 11 |
. . . . . . . . . 10
β’ (π β 0 β
β) |
78 | | infregelb 12144 |
. . . . . . . . . 10
β’ (((π
β β β§ π
β β
β§ βπ₯ β β βπ€ β π
π₯ β€ π€) β§ 0 β β) β (0 β€
inf(π
, β, < )
β βπ€ β
π
0 β€ π€)) |
79 | 14, 15, 21, 77, 78 | syl31anc 1374 |
. . . . . . . . 9
β’ (π β (0 β€ inf(π
, β, < ) β
βπ€ β π
0 β€ π€)) |
80 | 17, 79 | mpbird 257 |
. . . . . . . 8
β’ (π β 0 β€ inf(π
, β, <
)) |
81 | 80, 2 | breqtrrdi 5148 |
. . . . . . 7
β’ (π β 0 β€ π) |
82 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) |
83 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β (π΄ππ¦) = (π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) |
84 | 83 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π¦ = ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β (πβ(π΄ππ¦)) = (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
85 | 84 | rspceeqv 3596 |
. . . . . . . . . . . 12
β’ ((((1 /
2)( Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π β§ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) β βπ¦ β π (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = (πβ(π΄ππ¦))) |
86 | 63, 82, 85 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β βπ¦ β π (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = (πβ(π΄ππ¦))) |
87 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π¦ β π β¦ (πβ(π΄ππ¦))) = (π¦ β π β¦ (πβ(π΄ππ¦))) |
88 | | fvex 6856 |
. . . . . . . . . . . 12
β’ (πβ(π΄ππ¦)) β V |
89 | 87, 88 | elrnmpti 5916 |
. . . . . . . . . . 11
β’ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β ran (π¦ β π β¦ (πβ(π΄ππ¦))) β βπ¦ β π (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = (πβ(π΄ππ¦))) |
90 | 86, 89 | sylibr 233 |
. . . . . . . . . 10
β’ (π β (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β ran (π¦ β π β¦ (πβ(π΄ππ¦)))) |
91 | 90, 12 | eleqtrrdi 2845 |
. . . . . . . . 9
β’ (π β (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β π
) |
92 | | infrelb 12145 |
. . . . . . . . 9
β’ ((π
β β β§
βπ₯ β β
βπ€ β π
π₯ β€ π€ β§ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β π
) β inf(π
, β, < ) β€ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
93 | 14, 21, 91, 92 | syl3anc 1372 |
. . . . . . . 8
β’ (π β inf(π
, β, < ) β€ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
94 | 2, 93 | eqbrtrid 5141 |
. . . . . . 7
β’ (π β π β€ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
95 | | le2sq2 14046 |
. . . . . . 7
β’ (((π β β β§ 0 β€
π) β§ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β β β§ π β€ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))) β (πβ2) β€ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) |
96 | 24, 81, 68, 94, 95 | syl22anc 838 |
. . . . . 6
β’ (π β (πβ2) β€ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) |
97 | | 4pos 12265 |
. . . . . . . . 9
β’ 0 <
4 |
98 | 1, 97 | pm3.2i 472 |
. . . . . . . 8
β’ (4 β
β β§ 0 < 4) |
99 | | lemul2 12013 |
. . . . . . . 8
β’ (((πβ2) β β β§
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β β β§ (4 β
β β§ 0 < 4)) β ((πβ2) β€ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)))) |
100 | 98, 99 | mp3an3 1451 |
. . . . . . 7
β’ (((πβ2) β β β§
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β β) β ((πβ2) β€ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)))) |
101 | 25, 69, 100 | syl2anc 585 |
. . . . . 6
β’ (π β ((πβ2) β€ ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2) β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)))) |
102 | 96, 101 | mpbid 231 |
. . . . 5
β’ (π β (4 Β· (πβ2)) β€ (4 Β·
((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2))) |
103 | 27, 71, 43, 102 | leadd1dd 11774 |
. . . 4
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) + ((πΎπ·πΏ)β2))) |
104 | | metcl 23701 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π΄ β π β§ πΎ β π) β (π΄π·πΎ) β β) |
105 | 31, 9, 38, 104 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΎ) β β) |
106 | 105 | resqcld 14036 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) β β) |
107 | | metcl 23701 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π΄ β π β§ πΏ β π) β (π΄π·πΏ) β β) |
108 | 31, 9, 40, 107 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΏ) β β) |
109 | 108 | resqcld 14036 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) β β) |
110 | | minvecolem2.5 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) β€ ((πβ2) + π΅)) |
111 | | minvecolem2.6 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) β€ ((πβ2) + π΅)) |
112 | 106, 109,
74, 74, 110, 111 | le2addd 11779 |
. . . . . . 7
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) β€ (((πβ2) + π΅) + ((πβ2) + π΅))) |
113 | 74 | 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, 74, 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 | 3, 4 | nvmcl 29630 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ πΎ β π) β (π΄ππΎ) β π) |
127 | 29, 9, 38, 126 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄ππΎ) β π) |
128 | 3, 4 | nvmcl 29630 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ πΏ β π) β (π΄ππΏ) β π) |
129 | 29, 9, 40, 128 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π΄ππΏ) β π) |
130 | 3, 48, 4, 5 | phpar2 29807 |
. . . . . . 7
β’ ((π β CPreHilOLD
β§ (π΄ππΎ) β π β§ (π΄ππΏ) β π) β (((πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))β2) + ((πβ((π΄ππΎ)π(π΄ππΏ)))β2)) = (2 Β· (((πβ(π΄ππΎ))β2) + ((πβ(π΄ππΏ))β2)))) |
131 | 7, 127, 129, 130 | syl3anc 1372 |
. . . . . 6
β’ (π β (((πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))β2) + ((πβ((π΄ππΎ)π(π΄ππΏ)))β2)) = (2 Β· (((πβ(π΄ππΎ))β2) + ((πβ(π΄ππΏ))β2)))) |
132 | | 2cn 12233 |
. . . . . . . . . 10
β’ 2 β
β |
133 | 68 | recnd 11188 |
. . . . . . . . . 10
β’ (π β (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β β) |
134 | | sqmul 14030 |
. . . . . . . . . 10
β’ ((2
β β β§ (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) β β) β ((2 Β·
(πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))β2) = ((2β2) Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2))) |
135 | 132, 133,
134 | sylancr 588 |
. . . . . . . . 9
β’ (π β ((2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))β2) = ((2β2) Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2))) |
136 | | sq2 14107 |
. . . . . . . . . 10
β’
(2β2) = 4 |
137 | 136 | oveq1i 7368 |
. . . . . . . . 9
β’
((2β2) Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) = (4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) |
138 | 135, 137 | eqtrdi 2789 |
. . . . . . . 8
β’ (π β ((2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))β2) = (4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2))) |
139 | 132 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β
β) |
140 | 3, 57, 5 | nvs 29647 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ 2 β
β β§ (π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))) β π) β (πβ(2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = ((absβ2) Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))) |
141 | 29, 139, 66, 140 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (πβ(2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = ((absβ2) Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))) |
142 | | 0le2 12260 |
. . . . . . . . . . . . 13
β’ 0 β€
2 |
143 | | absid 15187 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ 0 β€ 2) β (absβ2) = 2) |
144 | 117, 142,
143 | mp2an 691 |
. . . . . . . . . . . 12
β’
(absβ2) = 2 |
145 | 144 | oveq1i 7368 |
. . . . . . . . . . 11
β’
((absβ2) Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = (2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
146 | 141, 145 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β (πβ(2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = (2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))) |
147 | 3, 4, 57 | nvmdi 29632 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (2 β
β β§ π΄ β
π β§ ((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) β π)) β (2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = ((2(
Β·π OLD βπ)π΄)π(2( Β·π OLD
βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
148 | 29, 139, 9, 64, 147 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (π β (2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = ((2(
Β·π OLD βπ)π΄)π(2( Β·π OLD
βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
149 | 3, 48, 57 | nv2 29616 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π΄ β π) β (π΄( +π£ βπ)π΄) = (2(
Β·π OLD βπ)π΄)) |
150 | 29, 9, 149 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (π΄( +π£ βπ)π΄) = (2(
Β·π OLD βπ)π΄)) |
151 | | 2ne0 12262 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
0 |
152 | 132, 151 | recidi 11891 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· (1 / 2)) = 1 |
153 | 152 | oveq1i 7368 |
. . . . . . . . . . . . . . 15
β’ ((2
Β· (1 / 2))( Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (1(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) |
154 | 3, 48 | nvgcl 29604 |
. . . . . . . . . . . . . . . . 17
β’ ((π β NrmCVec β§ πΎ β π β§ πΏ β π) β (πΎ( +π£ βπ)πΏ) β π) |
155 | 29, 38, 40, 154 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΎ( +π£ βπ)πΏ) β π) |
156 | 3, 57 | nvsid 29611 |
. . . . . . . . . . . . . . . 16
β’ ((π β NrmCVec β§ (πΎ( +π£
βπ)πΏ) β π) β (1(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (πΎ( +π£ βπ)πΏ)) |
157 | 29, 155, 156 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (1(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (πΎ( +π£ βπ)πΏ)) |
158 | 153, 157 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π β ((2 Β· (1 / 2))(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (πΎ( +π£ βπ)πΏ)) |
159 | 3, 57 | nvsass 29612 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ (2 β
β β§ (1 / 2) β β β§ (πΎ( +π£ βπ)πΏ) β π)) β ((2 Β· (1 / 2))(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (2(
Β·π OLD βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) |
160 | 29, 139, 47, 155, 159 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (π β ((2 Β· (1 / 2))(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)) = (2(
Β·π OLD βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) |
161 | 158, 160 | eqtr3d 2775 |
. . . . . . . . . . . . 13
β’ (π β (πΎ( +π£ βπ)πΏ) = (2(
Β·π OLD βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) |
162 | 150, 161 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π β ((π΄( +π£ βπ)π΄)π(πΎ( +π£ βπ)πΏ)) = ((2(
Β·π OLD βπ)π΄)π(2( Β·π OLD
βπ)((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) |
163 | 3, 48, 4 | nvaddsub4 29641 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π΄ β π β§ π΄ β π) β§ (πΎ β π β§ πΏ β π)) β ((π΄( +π£ βπ)π΄)π(πΎ( +π£ βπ)πΏ)) = ((π΄ππΎ)( +π£ βπ)(π΄ππΏ))) |
164 | 29, 9, 9, 38, 40, 163 | syl122anc 1380 |
. . . . . . . . . . . 12
β’ (π β ((π΄( +π£ βπ)π΄)π(πΎ( +π£ βπ)πΏ)) = ((π΄ππΎ)( +π£ βπ)(π΄ππΏ))) |
165 | 148, 162,
164 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (π β (2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))) = ((π΄ππΎ)( +π£ βπ)(π΄ππΏ))) |
166 | 165 | fveq2d 6847 |
. . . . . . . . . 10
β’ (π β (πβ(2(
Β·π OLD βπ)(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = (πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))) |
167 | 146, 166 | eqtr3d 2775 |
. . . . . . . . 9
β’ (π β (2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))) = (πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))) |
168 | 167 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((2 Β· (πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ)))))β2) = ((πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))β2)) |
169 | 138, 168 | eqtr3d 2775 |
. . . . . . 7
β’ (π β (4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) = ((πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))β2)) |
170 | 3, 4, 5, 10 | imsdval 29670 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ πΏ β π β§ πΎ β π) β (πΏπ·πΎ) = (πβ(πΏππΎ))) |
171 | 29, 40, 38, 170 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΏπ·πΎ) = (πβ(πΏππΎ))) |
172 | | metsym 23719 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ πΎ β π β§ πΏ β π) β (πΎπ·πΏ) = (πΏπ·πΎ)) |
173 | 31, 38, 40, 172 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (πΎπ·πΏ) = (πΏπ·πΎ)) |
174 | 3, 4 | nvnnncan1 29631 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ (π΄ β π β§ πΎ β π β§ πΏ β π)) β ((π΄ππΎ)π(π΄ππΏ)) = (πΏππΎ)) |
175 | 29, 9, 38, 40, 174 | syl13anc 1373 |
. . . . . . . . . 10
β’ (π β ((π΄ππΎ)π(π΄ππΏ)) = (πΏππΎ)) |
176 | 175 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β (πβ((π΄ππΎ)π(π΄ππΏ))) = (πβ(πΏππΎ))) |
177 | 171, 173,
176 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (π β (πΎπ·πΏ) = (πβ((π΄ππΎ)π(π΄ππΏ)))) |
178 | 177 | oveq1d 7373 |
. . . . . . 7
β’ (π β ((πΎπ·πΏ)β2) = ((πβ((π΄ππΎ)π(π΄ππΏ)))β2)) |
179 | 169, 178 | oveq12d 7376 |
. . . . . 6
β’ (π β ((4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) = (((πβ((π΄ππΎ)( +π£ βπ)(π΄ππΏ)))β2) + ((πβ((π΄ππΎ)π(π΄ππΏ)))β2))) |
180 | 3, 4, 5, 10 | imsdval 29670 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ πΎ β π) β (π΄π·πΎ) = (πβ(π΄ππΎ))) |
181 | 29, 9, 38, 180 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΎ) = (πβ(π΄ππΎ))) |
182 | 181 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π΄π·πΎ)β2) = ((πβ(π΄ππΎ))β2)) |
183 | 3, 4, 5, 10 | imsdval 29670 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ πΏ β π) β (π΄π·πΏ) = (πβ(π΄ππΏ))) |
184 | 29, 9, 40, 183 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π΄π·πΏ) = (πβ(π΄ππΏ))) |
185 | 184 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π΄π·πΏ)β2) = ((πβ(π΄ππΏ))β2)) |
186 | 182, 185 | oveq12d 7376 |
. . . . . . 7
β’ (π β (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)) = (((πβ(π΄ππΎ))β2) + ((πβ(π΄ππΏ))β2))) |
187 | 186 | oveq2d 7374 |
. . . . . 6
β’ (π β (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2))) = (2 Β· (((πβ(π΄ππΎ))β2) + ((πβ(π΄ππΏ))β2)))) |
188 | 131, 179,
187 | 3eqtr4d 2783 |
. . . . 5
β’ (π β ((4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) = (2 Β· (((π΄π·πΎ)β2) + ((π΄π·πΏ)β2)))) |
189 | | 2t2e4 12322 |
. . . . . . 7
β’ (2
Β· 2) = 4 |
190 | 189 | oveq1i 7368 |
. . . . . 6
β’ ((2
Β· 2) Β· ((πβ2) + π΅)) = (4 Β· ((πβ2) + π΅)) |
191 | 139, 139,
113 | mulassd 11183 |
. . . . . 6
β’ (π β ((2 Β· 2) Β·
((πβ2) + π΅)) = (2 Β· (2 Β·
((πβ2) + π΅)))) |
192 | 190, 191 | eqtr3id 2787 |
. . . . 5
β’ (π β (4 Β· ((πβ2) + π΅)) = (2 Β· (2 Β· ((πβ2) + π΅)))) |
193 | 125, 188,
192 | 3brtr4d 5138 |
. . . 4
β’ (π β ((4 Β· ((πβ(π΄π((1 / 2)(
Β·π OLD βπ)(πΎ( +π£ βπ)πΏ))))β2)) + ((πΎπ·πΏ)β2)) β€ (4 Β· ((πβ2) + π΅))) |
194 | 44, 72, 76, 103, 193 | letrd 11317 |
. . 3
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ (4 Β· ((πβ2) + π΅))) |
195 | | 4cn 12243 |
. . . . 5
β’ 4 β
β |
196 | 195 | a1i 11 |
. . . 4
β’ (π β 4 β
β) |
197 | 25 | recnd 11188 |
. . . 4
β’ (π β (πβ2) β β) |
198 | 73 | recnd 11188 |
. . . 4
β’ (π β π΅ β β) |
199 | 196, 197,
198 | adddid 11184 |
. . 3
β’ (π β (4 Β· ((πβ2) + π΅)) = ((4 Β· (πβ2)) + (4 Β· π΅))) |
200 | 194, 199 | breqtrd 5132 |
. 2
β’ (π β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· (πβ2)) + (4 Β· π΅))) |
201 | | remulcl 11141 |
. . . 4
β’ ((4
β β β§ π΅
β β) β (4 Β· π΅) β β) |
202 | 1, 73, 201 | sylancr 588 |
. . 3
β’ (π β (4 Β· π΅) β
β) |
203 | 43, 202, 27 | leadd2d 11755 |
. 2
β’ (π β (((πΎπ·πΏ)β2) β€ (4 Β· π΅) β ((4 Β· (πβ2)) + ((πΎπ·πΏ)β2)) β€ ((4 Β· (πβ2)) + (4 Β· π΅)))) |
204 | 200, 203 | mpbird 257 |
1
β’ (π β ((πΎπ·πΏ)β2) β€ (4 Β· π΅)) |