Step | Hyp | Ref
| Expression |
1 | | csbrn.1 |
. . . . 5
โข (๐ โ ๐ด โ Fin) |
2 | | csbrn.2 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
3 | 2 | resqcld 14031 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ตโ2) โ โ) |
4 | | 2re 12228 |
. . . . . . 7
โข 2 โ
โ |
5 | | csbrn.3 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
6 | 2, 5 | remulcld 11186 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
7 | | remulcl 11137 |
. . . . . . 7
โข ((2
โ โ โง (๐ต
ยท ๐ถ) โ โ)
โ (2 ยท (๐ต
ยท ๐ถ)) โ
โ) |
8 | 4, 6, 7 | sylancr 588 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
9 | 3, 8 | readdcld 11185 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) โ โ) |
10 | 1, 9 | fsumrecl 15620 |
. . . 4
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) โ โ) |
11 | 1, 3 | fsumrecl 15620 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด (๐ตโ2) โ โ) |
12 | 5 | resqcld 14031 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ (๐ถโ2) โ โ) |
13 | 1, 12 | fsumrecl 15620 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ๐ด (๐ถโ2) โ โ) |
14 | 11, 13 | remulcld 11186 |
. . . . . . 7
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ โ) |
15 | 2 | sqge0d 14043 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ 0 โค (๐ตโ2)) |
16 | 1, 3, 15 | fsumge0 15681 |
. . . . . . . 8
โข (๐ โ 0 โค ฮฃ๐ โ ๐ด (๐ตโ2)) |
17 | 5 | sqge0d 14043 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ 0 โค (๐ถโ2)) |
18 | 1, 12, 17 | fsumge0 15681 |
. . . . . . . 8
โข (๐ โ 0 โค ฮฃ๐ โ ๐ด (๐ถโ2)) |
19 | 11, 13, 16, 18 | mulge0d 11733 |
. . . . . . 7
โข (๐ โ 0 โค (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) |
20 | 14, 19 | resqrtcld 15303 |
. . . . . 6
โข (๐ โ
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ โ) |
21 | | remulcl 11137 |
. . . . . 6
โข ((2
โ โ โง (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ โ) โ (2
ยท (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) โ โ) |
22 | 4, 20, 21 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) โ โ) |
23 | 11, 22 | readdcld 11185 |
. . . 4
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) โ
โ) |
24 | 3 | recnd 11184 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ตโ2) โ โ) |
25 | 8 | recnd 11184 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
26 | 1, 24, 25 | fsumadd 15626 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) = (ฮฃ๐ โ ๐ด (๐ตโ2) + ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ)))) |
27 | 1, 8 | fsumrecl 15620 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ)) โ โ) |
28 | | 2cnd 12232 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
29 | 6 | recnd 11184 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ (๐ต ยท ๐ถ) โ โ) |
30 | 1, 28, 29 | fsummulc2 15670 |
. . . . . . 7
โข (๐ โ (2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) = ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ))) |
31 | 1, 6 | fsumrecl 15620 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) |
32 | 31 | recnd 11184 |
. . . . . . . . . 10
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โ โ) |
33 | 32 | abscld 15322 |
. . . . . . . . 9
โข (๐ โ (absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โ โ) |
34 | 31 | leabsd 15300 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โค (absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))) |
35 | 1, 2, 5 | csbren 24766 |
. . . . . . . . . . 11
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2) โค (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) |
36 | | absresq 15188 |
. . . . . . . . . . . 12
โข
(ฮฃ๐ โ
๐ด (๐ต ยท ๐ถ) โ โ โ
((absโฮฃ๐ โ
๐ด (๐ต ยท ๐ถ))โ2) = (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) |
37 | 31, 36 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) = (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)โ2)) |
38 | | resqrtth 15141 |
. . . . . . . . . . . 12
โข
(((ฮฃ๐ โ
๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)) โ โ โง 0 โค
(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ
((โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))โ2) = (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) |
39 | 14, 19, 38 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ
((โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))โ2) = (ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) |
40 | 35, 37, 39 | 3brtr4d 5138 |
. . . . . . . . . 10
โข (๐ โ ((absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โค
((โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))โ2)) |
41 | 32 | absge0d 15330 |
. . . . . . . . . . 11
โข (๐ โ 0 โค
(absโฮฃ๐ โ
๐ด (๐ต ยท ๐ถ))) |
42 | 14, 19 | sqrtge0d 15306 |
. . . . . . . . . . 11
โข (๐ โ 0 โค
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
43 | 33, 20, 41, 42 | le2sqd 14161 |
. . . . . . . . . 10
โข (๐ โ ((absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โค (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ ((absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ))โ2) โค
((โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))โ2))) |
44 | 40, 43 | mpbird 257 |
. . . . . . . . 9
โข (๐ โ (absโฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โค (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
45 | 31, 33, 20, 34, 44 | letrd 11313 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โค (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
46 | 4 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
47 | | 2pos 12257 |
. . . . . . . . . 10
โข 0 <
2 |
48 | 47 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 < 2) |
49 | | lemul2 12009 |
. . . . . . . . 9
โข
((ฮฃ๐ โ
๐ด (๐ต ยท ๐ถ) โ โ โง
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ โ โง (2 โ
โ โง 0 < 2)) โ (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โค (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ (2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โค (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))))) |
50 | 31, 20, 46, 48, 49 | syl112anc 1375 |
. . . . . . . 8
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ) โค (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) โ (2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โค (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))))) |
51 | 45, 50 | mpbid 231 |
. . . . . . 7
โข (๐ โ (2 ยท ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) โค (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
52 | 30, 51 | eqbrtrrd 5130 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ)) โค (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
53 | 27, 22, 11, 52 | leadd2dd 11771 |
. . . . 5
โข (๐ โ (ฮฃ๐ โ ๐ด (๐ตโ2) + ฮฃ๐ โ ๐ด (2 ยท (๐ต ยท ๐ถ))) โค (ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))))) |
54 | 26, 53 | eqbrtrd 5128 |
. . . 4
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) โค (ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))))) |
55 | 10, 23, 13, 54 | leadd1dd 11770 |
. . 3
โข (๐ โ (ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + ฮฃ๐ โ ๐ด (๐ถโ2)) โค ((ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
56 | 2, 5 | readdcld 11185 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ (๐ต + ๐ถ) โ โ) |
57 | 56 | resqcld 14031 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ((๐ต + ๐ถ)โ2) โ โ) |
58 | 1, 57 | fsumrecl 15620 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2) โ โ) |
59 | 56 | sqge0d 14043 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ 0 โค ((๐ต + ๐ถ)โ2)) |
60 | 1, 57, 59 | fsumge0 15681 |
. . . . 5
โข (๐ โ 0 โค ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2)) |
61 | | resqrtth 15141 |
. . . . 5
โข
((ฮฃ๐ โ
๐ด ((๐ต + ๐ถ)โ2) โ โ โง 0 โค
ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2)) โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))โ2) = ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2)) |
62 | 58, 60, 61 | syl2anc 585 |
. . . 4
โข (๐ โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))โ2) = ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2)) |
63 | 2 | recnd 11184 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
64 | 5 | recnd 11184 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
65 | | binom2 14122 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ต + ๐ถ)โ2) = (((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + (๐ถโ2))) |
66 | 63, 64, 65 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ((๐ต + ๐ถ)โ2) = (((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + (๐ถโ2))) |
67 | 66 | sumeq2dv 15589 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2) = ฮฃ๐ โ ๐ด (((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + (๐ถโ2))) |
68 | 9 | recnd 11184 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) โ โ) |
69 | 12 | recnd 11184 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ถโ2) โ โ) |
70 | 1, 68, 69 | fsumadd 15626 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ๐ด (((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + (๐ถโ2)) = (ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
71 | 67, 70 | eqtrd 2777 |
. . . 4
โข (๐ โ ฮฃ๐ โ ๐ด ((๐ต + ๐ถ)โ2) = (ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
72 | 62, 71 | eqtrd 2777 |
. . 3
โข (๐ โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))โ2) = (ฮฃ๐ โ ๐ด ((๐ตโ2) + (2 ยท (๐ต ยท ๐ถ))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
73 | 11, 16 | resqrtcld 15303 |
. . . . . 6
โข (๐ โ
(โโฮฃ๐
โ ๐ด (๐ตโ2)) โ โ) |
74 | 73 | recnd 11184 |
. . . . 5
โข (๐ โ
(โโฮฃ๐
โ ๐ด (๐ตโ2)) โ โ) |
75 | 13, 18 | resqrtcld 15303 |
. . . . . 6
โข (๐ โ
(โโฮฃ๐
โ ๐ด (๐ถโ2)) โ โ) |
76 | 75 | recnd 11184 |
. . . . 5
โข (๐ โ
(โโฮฃ๐
โ ๐ด (๐ถโ2)) โ โ) |
77 | | binom2 14122 |
. . . . 5
โข
(((โโฮฃ๐ โ ๐ด (๐ตโ2)) โ โ โง
(โโฮฃ๐
โ ๐ด (๐ถโ2)) โ โ) โ
(((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))โ2) =
((((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) + (2 ยท
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2))))) + ((โโฮฃ๐ โ ๐ด (๐ถโ2))โ2))) |
78 | 74, 76, 77 | syl2anc 585 |
. . . 4
โข (๐ โ
(((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))โ2) =
((((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) + (2 ยท
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2))))) + ((โโฮฃ๐ โ ๐ด (๐ถโ2))โ2))) |
79 | | resqrtth 15141 |
. . . . . . 7
โข
((ฮฃ๐ โ
๐ด (๐ตโ2) โ โ โง 0 โค
ฮฃ๐ โ ๐ด (๐ตโ2)) โ
((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) = ฮฃ๐ โ ๐ด (๐ตโ2)) |
80 | 11, 16, 79 | syl2anc 585 |
. . . . . 6
โข (๐ โ
((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) = ฮฃ๐ โ ๐ด (๐ตโ2)) |
81 | 11, 16, 13, 18 | sqrtmuld 15310 |
. . . . . . . 8
โข (๐ โ
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))) = ((โโฮฃ๐ โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2)))) |
82 | 81 | eqcomd 2743 |
. . . . . . 7
โข (๐ โ
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2))) = (โโ(ฮฃ๐ โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))) |
83 | 82 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (2 ยท
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2)))) = (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) |
84 | 80, 83 | oveq12d 7376 |
. . . . 5
โข (๐ โ
(((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) + (2 ยท
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2))))) = (ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2)))))) |
85 | | resqrtth 15141 |
. . . . . 6
โข
((ฮฃ๐ โ
๐ด (๐ถโ2) โ โ โง 0 โค
ฮฃ๐ โ ๐ด (๐ถโ2)) โ
((โโฮฃ๐
โ ๐ด (๐ถโ2))โ2) = ฮฃ๐ โ ๐ด (๐ถโ2)) |
86 | 13, 18, 85 | syl2anc 585 |
. . . . 5
โข (๐ โ
((โโฮฃ๐
โ ๐ด (๐ถโ2))โ2) = ฮฃ๐ โ ๐ด (๐ถโ2)) |
87 | 84, 86 | oveq12d 7376 |
. . . 4
โข (๐ โ
((((โโฮฃ๐
โ ๐ด (๐ตโ2))โ2) + (2 ยท
((โโฮฃ๐
โ ๐ด (๐ตโ2)) ยท
(โโฮฃ๐
โ ๐ด (๐ถโ2))))) + ((โโฮฃ๐ โ ๐ด (๐ถโ2))โ2)) = ((ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
88 | 78, 87 | eqtrd 2777 |
. . 3
โข (๐ โ
(((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))โ2) = ((ฮฃ๐ โ ๐ด (๐ตโ2) + (2 ยท
(โโ(ฮฃ๐
โ ๐ด (๐ตโ2) ยท ฮฃ๐ โ ๐ด (๐ถโ2))))) + ฮฃ๐ โ ๐ด (๐ถโ2))) |
89 | 55, 72, 88 | 3brtr4d 5138 |
. 2
โข (๐ โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))โ2) โค
(((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))โ2)) |
90 | 58, 60 | resqrtcld 15303 |
. . 3
โข (๐ โ
(โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2)) โ โ) |
91 | 73, 75 | readdcld 11185 |
. . 3
โข (๐ โ
((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2))) โ โ) |
92 | 58, 60 | sqrtge0d 15306 |
. . 3
โข (๐ โ 0 โค
(โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))) |
93 | 11, 16 | sqrtge0d 15306 |
. . . 4
โข (๐ โ 0 โค
(โโฮฃ๐
โ ๐ด (๐ตโ2))) |
94 | 13, 18 | sqrtge0d 15306 |
. . . 4
โข (๐ โ 0 โค
(โโฮฃ๐
โ ๐ด (๐ถโ2))) |
95 | 73, 75, 93, 94 | addge0d 11732 |
. . 3
โข (๐ โ 0 โค
((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))) |
96 | 90, 91, 92, 95 | le2sqd 14161 |
. 2
โข (๐ โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2)) โค ((โโฮฃ๐ โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2))) โ
((โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2))โ2) โค
(((โโฮฃ๐
โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))โ2))) |
97 | 89, 96 | mpbird 257 |
1
โข (๐ โ
(โโฮฃ๐
โ ๐ด ((๐ต + ๐ถ)โ2)) โค ((โโฮฃ๐ โ ๐ด (๐ตโ2)) + (โโฮฃ๐ โ ๐ด (๐ถโ2)))) |