Step | Hyp | Ref
| Expression |
1 | | 2cn 12236 |
. . . . . 6
โข 2 โ
โ |
2 | | simpll 766 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
3 | | simprl 770 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
4 | | remulcl 11144 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
5 | 2, 3, 4 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
6 | | mulge0 11681 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
7 | | resqrtcl 15147 |
. . . . . . . 8
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
8 | 5, 6, 7 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
9 | 8 | recnd 11191 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
10 | | sqmul 14033 |
. . . . . 6
โข ((2
โ โ โง (โโ(๐ด ยท ๐ต)) โ โ) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = ((2โ2)
ยท ((โโ(๐ด
ยท ๐ต))โ2))) |
11 | 1, 9, 10 | sylancr 588 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = ((2โ2)
ยท ((โโ(๐ด
ยท ๐ต))โ2))) |
12 | | sq2 14110 |
. . . . . . 7
โข
(2โ2) = 4 |
13 | 12 | oveq1i 7371 |
. . . . . 6
โข
((2โ2) ยท ((โโ(๐ด ยท ๐ต))โ2)) = (4 ยท
((โโ(๐ด ยท
๐ต))โ2)) |
14 | 5 | recnd 11191 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
15 | | sqrtth 15258 |
. . . . . . . 8
โข ((๐ด ยท ๐ต) โ โ โ
((โโ(๐ด ยท
๐ต))โ2) = (๐ด ยท ๐ต)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (๐ด ยท ๐ต)) |
17 | 16 | oveq2d 7377 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท
((โโ(๐ด ยท
๐ต))โ2)) = (4 ยท
(๐ด ยท ๐ต))) |
18 | 13, 17 | eqtrid 2785 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2โ2) ยท
((โโ(๐ด ยท
๐ต))โ2)) = (4 ยท
(๐ด ยท ๐ต))) |
19 | 11, 18 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = (4 ยท
(๐ด ยท ๐ต))) |
20 | 2, 3 | resubcld 11591 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โ ๐ต) โ โ) |
21 | 20 | sqge0d 14051 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค ((๐ด โ ๐ต)โ2)) |
22 | 2 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
23 | 3 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
24 | | binom2 14130 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
26 | | binom2sub 14132 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
27 | 22, 23, 26 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
28 | 25, 27 | oveq12d 7379 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)))) |
29 | 2 | resqcld 14039 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ดโ2) โ โ) |
30 | | 2re 12235 |
. . . . . . . . . . . 12
โข 2 โ
โ |
31 | | remulcl 11144 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (๐ด
ยท ๐ต) โ โ)
โ (2 ยท (๐ด
ยท ๐ต)) โ
โ) |
32 | 30, 5, 31 | sylancr 588 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (๐ด ยท ๐ต)) โ โ) |
33 | 29, 32 | readdcld 11192 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
34 | 33 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
35 | 29, 32 | resubcld 11591 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) โ โ) |
36 | 35 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) โ โ) |
37 | 3 | resqcld 14039 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ตโ2) โ โ) |
38 | 37 | recnd 11191 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ตโ2) โ โ) |
39 | 34, 36, 38 | pnpcan2d 11558 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))))) |
40 | 32 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (๐ด ยท ๐ต)) โ โ) |
41 | 40 | 2timesd 12404 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (2
ยท (๐ด ยท ๐ต))) = ((2 ยท (๐ด ยท ๐ต)) + (2 ยท (๐ด ยท ๐ต)))) |
42 | | 2t2e4 12325 |
. . . . . . . . . . 11
โข (2
ยท 2) = 4 |
43 | 42 | oveq1i 7371 |
. . . . . . . . . 10
โข ((2
ยท 2) ยท (๐ด
ยท ๐ต)) = (4 ยท
(๐ด ยท ๐ต)) |
44 | | 2cnd 12239 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 2 โ
โ) |
45 | 44, 44, 14 | mulassd 11186 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท 2)
ยท (๐ด ยท ๐ต)) = (2 ยท (2 ยท
(๐ด ยท ๐ต)))) |
46 | 43, 45 | eqtr3id 2787 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) = (2 ยท (2 ยท (๐ด ยท ๐ต)))) |
47 | 29 | recnd 11191 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ดโ2) โ โ) |
48 | 47, 40, 40 | pnncand 11559 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต)))) = ((2 ยท (๐ด ยท ๐ต)) + (2 ยท (๐ด ยท ๐ต)))) |
49 | 41, 46, 48 | 3eqtr4rd 2784 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต)))) = (4 ยท (๐ด ยท ๐ต))) |
50 | 28, 39, 49 | 3eqtrd 2777 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต))) |
51 | 2, 3 | readdcld 11192 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด + ๐ต) โ โ) |
52 | 51 | resqcld 14039 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) โ โ) |
53 | 52 | recnd 11191 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) โ โ) |
54 | 20 | resqcld 14039 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) โ โ) |
55 | 54 | recnd 11191 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) โ โ) |
56 | | 4re 12245 |
. . . . . . . . . 10
โข 4 โ
โ |
57 | | remulcl 11144 |
. . . . . . . . . 10
โข ((4
โ โ โง (๐ด
ยท ๐ต) โ โ)
โ (4 ยท (๐ด
ยท ๐ต)) โ
โ) |
58 | 56, 5, 57 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โ โ) |
59 | 58 | recnd 11191 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โ โ) |
60 | | subsub23 11414 |
. . . . . . . 8
โข ((((๐ด + ๐ต)โ2) โ โ โง ((๐ด โ ๐ต)โ2) โ โ โง (4 ยท
(๐ด ยท ๐ต)) โ โ) โ
((((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2))) |
61 | 53, 55, 59, 60 | syl3anc 1372 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2))) |
62 | 50, 61 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2)) |
63 | 21, 62 | breqtrrd 5137 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต)))) |
64 | 52, 58 | subge0d 11753 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (0 โค (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) โ (4 ยท (๐ด ยท ๐ต)) โค ((๐ด + ๐ต)โ2))) |
65 | 63, 64 | mpbid 231 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โค ((๐ด + ๐ต)โ2)) |
66 | 19, 65 | eqbrtrd 5131 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) โค ((๐ด + ๐ต)โ2)) |
67 | | remulcl 11144 |
. . . . 5
โข ((2
โ โ โง (โโ(๐ด ยท ๐ต)) โ โ) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โ
โ) |
68 | 30, 8, 67 | sylancr 588 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โ
โ) |
69 | | sqrtge0 15151 |
. . . . . 6
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ 0 โค (โโ(๐ด ยท ๐ต))) |
70 | 5, 6, 69 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
(โโ(๐ด ยท
๐ต))) |
71 | | 0le2 12263 |
. . . . . 6
โข 0 โค
2 |
72 | | mulge0 11681 |
. . . . . 6
โข (((2
โ โ โง 0 โค 2) โง ((โโ(๐ด ยท ๐ต)) โ โ โง 0 โค
(โโ(๐ด ยท
๐ต)))) โ 0 โค (2
ยท (โโ(๐ด
ยท ๐ต)))) |
73 | 30, 71, 72 | mpanl12 701 |
. . . . 5
โข
(((โโ(๐ด
ยท ๐ต)) โ โ
โง 0 โค (โโ(๐ด ยท ๐ต))) โ 0 โค (2 ยท
(โโ(๐ด ยท
๐ต)))) |
74 | 8, 70, 73 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (2 ยท
(โโ(๐ด ยท
๐ต)))) |
75 | | addge0 11652 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด + ๐ต)) |
76 | 75 | an4s 659 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด + ๐ต)) |
77 | 68, 51, 74, 76 | le2sqd 14169 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต) โ ((2 ยท (โโ(๐ด ยท ๐ต)))โ2) โค ((๐ด + ๐ต)โ2))) |
78 | 66, 77 | mpbird 257 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต)) |
79 | | 2rp 12928 |
. . . 4
โข 2 โ
โ+ |
80 | 79 | a1i 11 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 2 โ
โ+) |
81 | 8, 51, 80 | lemuldiv2d 13015 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต) โ (โโ(๐ด ยท ๐ต)) โค ((๐ด + ๐ต) / 2))) |
82 | 78, 81 | mpbid 231 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โค ((๐ด + ๐ต) / 2)) |