Step | Hyp | Ref
| Expression |
1 | | 2cn 8989 |
. . . . . 6
โข 2 โ
โ |
2 | | simpll 527 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
3 | | simprl 529 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
4 | | remulcl 7938 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
5 | 2, 3, 4 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
6 | | mulge0 8575 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
7 | | resqrtcl 11037 |
. . . . . . . 8
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
8 | 5, 6, 7 | syl2anc 411 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
9 | 8 | recnd 7985 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โ โ) |
10 | | sqmul 10581 |
. . . . . 6
โข ((2
โ โ โง (โโ(๐ด ยท ๐ต)) โ โ) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = ((2โ2)
ยท ((โโ(๐ด
ยท ๐ต))โ2))) |
11 | 1, 9, 10 | sylancr 414 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = ((2โ2)
ยท ((โโ(๐ด
ยท ๐ต))โ2))) |
12 | | sq2 10615 |
. . . . . . 7
โข
(2โ2) = 4 |
13 | 12 | oveq1i 5884 |
. . . . . 6
โข
((2โ2) ยท ((โโ(๐ด ยท ๐ต))โ2)) = (4 ยท
((โโ(๐ด ยท
๐ต))โ2)) |
14 | | resqrtth 11039 |
. . . . . . . 8
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (๐ด ยท ๐ต)) |
15 | 5, 6, 14 | syl2anc 411 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ(๐ด ยท ๐ต))โ2) = (๐ด ยท ๐ต)) |
16 | 15 | oveq2d 5890 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท
((โโ(๐ด ยท
๐ต))โ2)) = (4 ยท
(๐ด ยท ๐ต))) |
17 | 13, 16 | eqtrid 2222 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2โ2) ยท
((โโ(๐ด ยท
๐ต))โ2)) = (4 ยท
(๐ด ยท ๐ต))) |
18 | 11, 17 | eqtrd 2210 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) = (4 ยท
(๐ด ยท ๐ต))) |
19 | 2, 3 | resubcld 8337 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โ ๐ต) โ โ) |
20 | 19 | sqge0d 10680 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค ((๐ด โ ๐ต)โ2)) |
21 | 2 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
22 | 3 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
23 | | binom2 10631 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
24 | 21, 22, 23 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
25 | | binom2sub 10633 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
26 | 21, 22, 25 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) = (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
27 | 24, 26 | oveq12d 5892 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)))) |
28 | 2 | resqcld 10679 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ดโ2) โ โ) |
29 | | 2re 8988 |
. . . . . . . . . . . 12
โข 2 โ
โ |
30 | | remulcl 7938 |
. . . . . . . . . . . 12
โข ((2
โ โ โง (๐ด
ยท ๐ต) โ โ)
โ (2 ยท (๐ด
ยท ๐ต)) โ
โ) |
31 | 29, 5, 30 | sylancr 414 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (๐ด ยท ๐ต)) โ โ) |
32 | 28, 31 | readdcld 7986 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
33 | 32 | recnd 7985 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
34 | 28, 31 | resubcld 8337 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) โ โ) |
35 | 34 | recnd 7985 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) โ โ) |
36 | 3 | resqcld 10679 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ตโ2) โ โ) |
37 | 36 | recnd 7985 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ตโ2) โ โ) |
38 | 33, 35, 37 | pnpcan2d 8305 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ (((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))) + (๐ตโ2))) = (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต))))) |
39 | 31 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (๐ด ยท ๐ต)) โ โ) |
40 | 39 | 2timesd 9160 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท (2
ยท (๐ด ยท ๐ต))) = ((2 ยท (๐ด ยท ๐ต)) + (2 ยท (๐ด ยท ๐ต)))) |
41 | | 2t2e4 9072 |
. . . . . . . . . . 11
โข (2
ยท 2) = 4 |
42 | 41 | oveq1i 5884 |
. . . . . . . . . 10
โข ((2
ยท 2) ยท (๐ด
ยท ๐ต)) = (4 ยท
(๐ด ยท ๐ต)) |
43 | | 2cnd 8991 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 2 โ
โ) |
44 | 5 | recnd 7985 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
45 | 43, 43, 44 | mulassd 7980 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท 2)
ยท (๐ด ยท ๐ต)) = (2 ยท (2 ยท
(๐ด ยท ๐ต)))) |
46 | 42, 45 | eqtr3id 2224 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) = (2 ยท (2 ยท (๐ด ยท ๐ต)))) |
47 | 28 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ดโ2) โ โ) |
48 | 47, 39, 39 | pnncand 8306 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต)))) = ((2 ยท (๐ด ยท ๐ต)) + (2 ยท (๐ด ยท ๐ต)))) |
49 | 40, 46, 48 | 3eqtr4rd 2221 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ดโ2) + (2 ยท (๐ด ยท ๐ต))) โ ((๐ดโ2) โ (2 ยท (๐ด ยท ๐ต)))) = (4 ยท (๐ด ยท ๐ต))) |
50 | 27, 38, 49 | 3eqtrd 2214 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต))) |
51 | 2, 3 | readdcld 7986 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด + ๐ต) โ โ) |
52 | 51 | resqcld 10679 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) โ โ) |
53 | 52 | recnd 7985 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด + ๐ต)โ2) โ โ) |
54 | 19 | resqcld 10679 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) โ โ) |
55 | 54 | recnd 7985 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด โ ๐ต)โ2) โ โ) |
56 | | 4re 8995 |
. . . . . . . . . 10
โข 4 โ
โ |
57 | | remulcl 7938 |
. . . . . . . . . 10
โข ((4
โ โ โง (๐ด
ยท ๐ต) โ โ)
โ (4 ยท (๐ด
ยท ๐ต)) โ
โ) |
58 | 56, 5, 57 | sylancr 414 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โ โ) |
59 | 58 | recnd 7985 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โ โ) |
60 | | subsub23 8161 |
. . . . . . . 8
โข ((((๐ด + ๐ต)โ2) โ โ โง ((๐ด โ ๐ต)โ2) โ โ โง (4 ยท
(๐ด ยท ๐ต)) โ โ) โ
((((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2))) |
61 | 53, 55, 59, 60 | syl3anc 1238 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((((๐ด + ๐ต)โ2) โ ((๐ด โ ๐ต)โ2)) = (4 ยท (๐ด ยท ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2))) |
62 | 50, 61 | mpbid 147 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) = ((๐ด โ ๐ต)โ2)) |
63 | 20, 62 | breqtrrd 4031 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต)))) |
64 | 52, 58 | subge0d 8491 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (0 โค (((๐ด + ๐ต)โ2) โ (4 ยท (๐ด ยท ๐ต))) โ (4 ยท (๐ด ยท ๐ต)) โค ((๐ด + ๐ต)โ2))) |
65 | 63, 64 | mpbid 147 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (4 ยท (๐ด ยท ๐ต)) โค ((๐ด + ๐ต)โ2)) |
66 | 18, 65 | eqbrtrd 4025 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต)))โ2) โค ((๐ด + ๐ต)โ2)) |
67 | | remulcl 7938 |
. . . . 5
โข ((2
โ โ โง (โโ(๐ด ยท ๐ต)) โ โ) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โ
โ) |
68 | 29, 8, 67 | sylancr 414 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โ
โ) |
69 | | sqrtge0 11041 |
. . . . . 6
โข (((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โ 0 โค (โโ(๐ด ยท ๐ต))) |
70 | 5, 6, 69 | syl2anc 411 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค
(โโ(๐ด ยท
๐ต))) |
71 | | 0le2 9008 |
. . . . . 6
โข 0 โค
2 |
72 | | mulge0 8575 |
. . . . . 6
โข (((2
โ โ โง 0 โค 2) โง ((โโ(๐ด ยท ๐ต)) โ โ โง 0 โค
(โโ(๐ด ยท
๐ต)))) โ 0 โค (2
ยท (โโ(๐ด
ยท ๐ต)))) |
73 | 29, 71, 72 | mpanl12 436 |
. . . . 5
โข
(((โโ(๐ด
ยท ๐ต)) โ โ
โง 0 โค (โโ(๐ด ยท ๐ต))) โ 0 โค (2 ยท
(โโ(๐ด ยท
๐ต)))) |
74 | 8, 70, 73 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (2 ยท
(โโ(๐ด ยท
๐ต)))) |
75 | | addge0 8407 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด + ๐ต)) |
76 | 75 | an4s 588 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด + ๐ต)) |
77 | 68, 51, 74, 76 | le2sqd 10685 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต) โ ((2 ยท (โโ(๐ด ยท ๐ต)))โ2) โค ((๐ด + ๐ต)โ2))) |
78 | 66, 77 | mpbird 167 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต)) |
79 | | 2pos 9009 |
. . . . 5
โข 0 <
2 |
80 | 29, 79 | pm3.2i 272 |
. . . 4
โข (2 โ
โ โง 0 < 2) |
81 | 80 | a1i 9 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (2 โ โ
โง 0 < 2)) |
82 | | lemuldiv2 8838 |
. . 3
โข
(((โโ(๐ด
ยท ๐ต)) โ โ
โง (๐ด + ๐ต) โ โ โง (2 โ
โ โง 0 < 2)) โ ((2 ยท (โโ(๐ด ยท ๐ต))) โค (๐ด + ๐ต) โ (โโ(๐ด ยท ๐ต)) โค ((๐ด + ๐ต) / 2))) |
83 | 8, 51, 81, 82 | syl3anc 1238 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((2 ยท
(โโ(๐ด ยท
๐ต))) โค (๐ด + ๐ต) โ (โโ(๐ด ยท ๐ต)) โค ((๐ด + ๐ต) / 2))) |
84 | 78, 83 | mpbid 147 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) โค ((๐ด + ๐ต) / 2)) |