Step | Hyp | Ref
| Expression |
1 | | 2re 12228 |
. . . . . 6
โข 2 โ
โ |
2 | 1 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
3 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
4 | | simpr 486 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
5 | 4 | cjcld 15082 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
6 | 3, 5 | mulcld 11176 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท (โโ๐ต)) โ
โ) |
7 | 6 | recld 15080 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) โ
โ) |
8 | 2, 7 | remulcld 11186 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (โโ(๐ด
ยท (โโ๐ต)))) โ โ) |
9 | | abscl 15164 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
10 | 3, 9 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ด) โ
โ) |
11 | | abscl 15164 |
. . . . . . 7
โข (๐ต โ โ โ
(absโ๐ต) โ
โ) |
12 | 4, 11 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ต) โ
โ) |
13 | 10, 12 | remulcld 11186 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) ยท
(absโ๐ต)) โ
โ) |
14 | 2, 13 | remulcld 11186 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ((absโ๐ด)
ยท (absโ๐ต)))
โ โ) |
15 | 10 | resqcld 14031 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด)โ2)
โ โ) |
16 | 12 | resqcld 14031 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ต)โ2)
โ โ) |
17 | 15, 16 | readdcld 11185 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((absโ๐ด)โ2) +
((absโ๐ต)โ2))
โ โ) |
18 | | releabs 15207 |
. . . . . . 7
โข ((๐ด ยท (โโ๐ต)) โ โ โ
(โโ(๐ด ยท
(โโ๐ต))) โค
(absโ(๐ด ยท
(โโ๐ต)))) |
19 | 6, 18 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) โค
(absโ(๐ด ยท
(โโ๐ต)))) |
20 | | absmul 15180 |
. . . . . . . 8
โข ((๐ด โ โ โง
(โโ๐ต) โ
โ) โ (absโ(๐ด ยท (โโ๐ต))) = ((absโ๐ด) ยท (absโ(โโ๐ต)))) |
21 | 3, 5, 20 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด ยท
(โโ๐ต))) =
((absโ๐ด) ยท
(absโ(โโ๐ต)))) |
22 | | abscj 15165 |
. . . . . . . . 9
โข (๐ต โ โ โ
(absโ(โโ๐ต)) = (absโ๐ต)) |
23 | 4, 22 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(โโ๐ต)) = (absโ๐ต)) |
24 | 23 | oveq2d 7374 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) ยท
(absโ(โโ๐ต))) = ((absโ๐ด) ยท (absโ๐ต))) |
25 | 21, 24 | eqtrd 2777 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด ยท
(โโ๐ต))) =
((absโ๐ด) ยท
(absโ๐ต))) |
26 | 19, 25 | breqtrd 5132 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด ยท
(โโ๐ต))) โค
((absโ๐ด) ยท
(absโ๐ต))) |
27 | | 2rp 12921 |
. . . . . . 7
โข 2 โ
โ+ |
28 | 27 | a1i 11 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ+) |
29 | 7, 13, 28 | lemul2d 13002 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ(๐ด ยท
(โโ๐ต))) โค
((absโ๐ด) ยท
(absโ๐ต)) โ (2
ยท (โโ(๐ด
ยท (โโ๐ต)))) โค (2 ยท ((absโ๐ด) ยท (absโ๐ต))))) |
30 | 26, 29 | mpbid 231 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (โโ(๐ด
ยท (โโ๐ต)))) โค (2 ยท ((absโ๐ด) ยท (absโ๐ต)))) |
31 | 8, 14, 17, 30 | leadd2dd 11771 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((absโ๐ด)โ2) +
((absโ๐ต)โ2)) +
(2 ยท (โโ(๐ด ยท (โโ๐ต))))) โค ((((absโ๐ด)โ2) + ((absโ๐ต)โ2)) + (2 ยท ((absโ๐ด) ยท (absโ๐ต))))) |
32 | | sqabsadd 15168 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ(๐ด + ๐ต))โ2) = ((((absโ๐ด)โ2) + ((absโ๐ต)โ2)) + (2 ยท
(โโ(๐ด ยท
(โโ๐ต)))))) |
33 | 10 | recnd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ด) โ
โ) |
34 | 12 | recnd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ต) โ
โ) |
35 | | binom2 14122 |
. . . . 5
โข
(((absโ๐ด)
โ โ โง (absโ๐ต) โ โ) โ (((absโ๐ด) + (absโ๐ต))โ2) = ((((absโ๐ด)โ2) + (2 ยท ((absโ๐ด) ยท (absโ๐ต)))) + ((absโ๐ต)โ2))) |
36 | 33, 34, 35 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((absโ๐ด) +
(absโ๐ต))โ2) =
((((absโ๐ด)โ2) +
(2 ยท ((absโ๐ด)
ยท (absโ๐ต)))) +
((absโ๐ต)โ2))) |
37 | 15 | recnd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด)โ2)
โ โ) |
38 | 14 | recnd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ((absโ๐ด)
ยท (absโ๐ต)))
โ โ) |
39 | 16 | recnd 11184 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ต)โ2)
โ โ) |
40 | 37, 38, 39 | add32d 11383 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((absโ๐ด)โ2) +
(2 ยท ((absโ๐ด)
ยท (absโ๐ต)))) +
((absโ๐ต)โ2)) =
((((absโ๐ด)โ2) +
((absโ๐ต)โ2)) +
(2 ยท ((absโ๐ด)
ยท (absโ๐ต))))) |
41 | 36, 40 | eqtrd 2777 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((absโ๐ด) +
(absโ๐ต))โ2) =
((((absโ๐ด)โ2) +
((absโ๐ต)โ2)) +
(2 ยท ((absโ๐ด)
ยท (absโ๐ต))))) |
42 | 31, 32, 41 | 3brtr4d 5138 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ(๐ด + ๐ต))โ2) โค
(((absโ๐ด) +
(absโ๐ต))โ2)) |
43 | | addcl 11134 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
44 | | abscl 15164 |
. . . 4
โข ((๐ด + ๐ต) โ โ โ (absโ(๐ด + ๐ต)) โ โ) |
45 | 43, 44 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด + ๐ต)) โ
โ) |
46 | 10, 12 | readdcld 11185 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) +
(absโ๐ต)) โ
โ) |
47 | | absge0 15173 |
. . . 4
โข ((๐ด + ๐ต) โ โ โ 0 โค
(absโ(๐ด + ๐ต))) |
48 | 43, 47 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(absโ(๐ด + ๐ต))) |
49 | | absge0 15173 |
. . . . 5
โข (๐ด โ โ โ 0 โค
(absโ๐ด)) |
50 | 3, 49 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(absโ๐ด)) |
51 | | absge0 15173 |
. . . . 5
โข (๐ต โ โ โ 0 โค
(absโ๐ต)) |
52 | 4, 51 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(absโ๐ต)) |
53 | 10, 12, 50, 52 | addge0d 11732 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((absโ๐ด) +
(absโ๐ต))) |
54 | 45, 46, 48, 53 | le2sqd 14161 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ(๐ด + ๐ต)) โค ((absโ๐ด) + (absโ๐ต)) โ ((absโ(๐ด + ๐ต))โ2) โค (((absโ๐ด) + (absโ๐ต))โ2))) |
55 | 42, 54 | mpbird 257 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ(๐ด + ๐ต)) โค ((absโ๐ด) + (absโ๐ต))) |