Step | Hyp | Ref
| Expression |
1 | | itscnhlc0yqe.q |
. . . . 5
โข ๐ = ((๐ดโ2) + (๐ตโ2)) |
2 | | eqid 2733 |
. . . . 5
โข -(2
ยท (๐ต ยท ๐ถ)) = -(2 ยท (๐ต ยท ๐ถ)) |
3 | | eqid 2733 |
. . . . 5
โข ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))) = ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))) |
4 | 1, 2, 3 | itsclc0yqe 46937 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โ ((((๐โ2) +
(๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0)) |
5 | 4 | 3adant1r 1178 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ)) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0)) |
6 | 5 | 3adant2r 1180 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0)) |
7 | | 3simpa 1149 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ โ โง ๐ต โ
โ)) |
8 | 7 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ (๐ด โ โ โง ๐ต โ โ)) |
9 | 1 | resum2sqcl 46882 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ โ
โ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ๐ โ โ) |
11 | 10 | 3ad2ant1 1134 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
12 | 11 | recnd 11191 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
13 | | simpr1 1195 |
. . . . . . . . . . 11
โข ((๐ด โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ด โ โ) |
14 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ด โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ด โ 0) |
15 | | simpr2 1196 |
. . . . . . . . . . 11
โข ((๐ด โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ต โ โ) |
16 | 1 | resum2sqgt0 46883 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โ 0 < ๐) |
17 | 13, 14, 15, 16 | syl21anc 837 |
. . . . . . . . . 10
โข ((๐ด โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ 0 < ๐) |
18 | 17 | ex 414 |
. . . . . . . . 9
โข (๐ด โ 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ 0 <
๐)) |
19 | | simpr2 1196 |
. . . . . . . . . . . 12
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ต โ โ) |
20 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ต โ 0) |
21 | | simpr1 1195 |
. . . . . . . . . . . 12
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ด โ โ) |
22 | | eqid 2733 |
. . . . . . . . . . . . 13
โข ((๐ตโ2) + (๐ดโ2)) = ((๐ตโ2) + (๐ดโ2)) |
23 | 22 | resum2sqgt0 46883 |
. . . . . . . . . . . 12
โข (((๐ต โ โ โง ๐ต โ 0) โง ๐ด โ โ) โ 0 < ((๐ตโ2) + (๐ดโ2))) |
24 | 19, 20, 21, 23 | syl21anc 837 |
. . . . . . . . . . 11
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ 0 < ((๐ตโ2) + (๐ดโ2))) |
25 | | simp1 1137 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
26 | 25 | recnd 11191 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
27 | 26 | sqcld 14058 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ดโ2) โ
โ) |
28 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
29 | 28 | recnd 11191 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
30 | 29 | sqcld 14058 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ตโ2) โ
โ) |
31 | 27, 30 | addcomd 11365 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ดโ2) + (๐ตโ2)) = ((๐ตโ2) + (๐ดโ2))) |
32 | 31 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ((๐ดโ2) + (๐ตโ2)) = ((๐ตโ2) + (๐ดโ2))) |
33 | 1, 32 | eqtrid 2785 |
. . . . . . . . . . 11
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ ๐ = ((๐ตโ2) + (๐ดโ2))) |
34 | 24, 33 | breqtrrd 5137 |
. . . . . . . . . 10
โข ((๐ต โ 0 โง (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) โ 0 < ๐) |
35 | 34 | ex 414 |
. . . . . . . . 9
โข (๐ต โ 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ 0 <
๐)) |
36 | 18, 35 | jaoi 856 |
. . . . . . . 8
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ 0 < ๐)) |
37 | 36 | impcom 409 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ 0 < ๐) |
38 | 37 | gt0ne0d 11727 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ๐ โ 0) |
39 | 38 | 3ad2ant1 1134 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ 0) |
40 | | 2cnd 12239 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ 2 โ
โ) |
41 | | recn 11149 |
. . . . . . . . . . 11
โข (๐ต โ โ โ ๐ต โ
โ) |
42 | 41 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
43 | 42 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ๐ต โ โ) |
44 | 43 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ต โ โ) |
45 | | recn 11149 |
. . . . . . . . . . 11
โข (๐ถ โ โ โ ๐ถ โ
โ) |
46 | 45 | 3ad2ant3 1136 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
47 | 46 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ๐ถ โ โ) |
48 | 47 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ถ โ โ) |
49 | 44, 48 | mulcld 11183 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ต ยท ๐ถ) โ โ) |
50 | 40, 49 | mulcld 11183 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (2 ยท (๐ต ยท ๐ถ)) โ โ) |
51 | 50 | negcld 11507 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ -(2 ยท (๐ต ยท ๐ถ)) โ โ) |
52 | 48 | sqcld 14058 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ถโ2) โ โ) |
53 | | recn 11149 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ
โ) |
54 | 53 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
55 | 54 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ๐ด โ โ) |
56 | 55 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ โ) |
57 | 56 | sqcld 14058 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ดโ2) โ โ) |
58 | | simpl 484 |
. . . . . . . . . 10
โข ((๐
โ โ+
โง 0 โค ๐ท) โ
๐
โ
โ+) |
59 | 58 | rpcnd 12967 |
. . . . . . . . 9
โข ((๐
โ โ+
โง 0 โค ๐ท) โ
๐
โ
โ) |
60 | 59 | 3ad2ant2 1135 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐
โ โ) |
61 | 60 | sqcld 14058 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐
โ2) โ โ) |
62 | 57, 61 | mulcld 11183 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ดโ2) ยท (๐
โ2)) โ โ) |
63 | 52, 62 | subcld 11520 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))) โ โ) |
64 | | recn 11149 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
65 | 64 | adantl 483 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
66 | 65 | 3ad2ant3 1136 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
67 | | eqidd 2734 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((-(2 ยท
(๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))) = ((-(2 ยท
(๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))))) |
68 | 12, 39, 51, 63, 66, 67 | quad 26213 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0 โ (๐ = ((--(2 ยท (๐ต ยท ๐ถ)) + (โโ((-(2 ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท (๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท ๐)) โจ ๐ = ((--(2 ยท (๐ต ยท ๐ถ)) โ (โโ((-(2 ยท
(๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐))))) |
69 | 53 | abscld 15330 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
70 | 69 | recnd 11191 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
71 | 70 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(absโ๐ด) โ
โ) |
72 | 71 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ (absโ๐ด) โ
โ) |
73 | 72 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (absโ๐ด) โ
โ) |
74 | | itsclc0yqsol.d |
. . . . . . . . . . . . . 14
โข ๐ท = (((๐
โ2) ยท ๐) โ (๐ถโ2)) |
75 | 58 | rpred 12965 |
. . . . . . . . . . . . . . . . . 18
โข ((๐
โ โ+
โง 0 โค ๐ท) โ
๐
โ
โ) |
76 | 75 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐
โ โ) |
77 | 76 | resqcld 14039 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐
โ2) โ โ) |
78 | 77, 11 | remulcld 11193 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐
โ2) ยท ๐) โ โ) |
79 | | simp1l3 1269 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ถ โ โ) |
80 | 79 | resqcld 14039 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ถโ2) โ โ) |
81 | 78, 80 | resubcld 11591 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (((๐
โ2) ยท ๐) โ (๐ถโ2)) โ โ) |
82 | 74, 81 | eqeltrid 2838 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ท โ โ) |
83 | 82 | recnd 11191 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ท โ โ) |
84 | 83 | sqrtcld 15331 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ
(โโ๐ท) โ
โ) |
85 | 40, 73, 84 | mulassd 11186 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((2 ยท
(absโ๐ด)) ยท
(โโ๐ท)) = (2
ยท ((absโ๐ด)
ยท (โโ๐ท)))) |
86 | 85 | oveq2d 7377 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((2 ยท (๐ต ยท ๐ถ)) + ((2 ยท (absโ๐ด)) ยท (โโ๐ท))) = ((2 ยท (๐ต ยท ๐ถ)) + (2 ยท ((absโ๐ด) ยท (โโ๐ท))))) |
87 | 50 | negnegd 11511 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ --(2 ยท
(๐ต ยท ๐ถ)) = (2 ยท (๐ต ยท ๐ถ))) |
88 | | simpl 484 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
89 | 88 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
90 | | simp2r 1201 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ 0 โค ๐ท) |
91 | 1, 2, 3, 74 | itsclc0yqsollem2 46939 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ โง 0 โค
๐ท) โ
(โโ((-(2 ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท (๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))))) = ((2 ยท
(absโ๐ด)) ยท
(โโ๐ท))) |
92 | 89, 76, 90, 91 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ
(โโ((-(2 ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท (๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))))) = ((2 ยท
(absโ๐ด)) ยท
(โโ๐ท))) |
93 | 87, 92 | oveq12d 7379 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (--(2 ยท
(๐ต ยท ๐ถ)) + (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) = ((2 ยท
(๐ต ยท ๐ถ)) + ((2 ยท
(absโ๐ด)) ยท
(โโ๐ท)))) |
94 | 73, 84 | mulcld 11183 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((absโ๐ด) ยท (โโ๐ท)) โ
โ) |
95 | 40, 49, 94 | adddid 11187 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (2 ยท ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท)))) = ((2 ยท (๐ต ยท ๐ถ)) + (2 ยท ((absโ๐ด) ยท (โโ๐ท))))) |
96 | 86, 93, 95 | 3eqtr4d 2783 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (--(2 ยท
(๐ต ยท ๐ถ)) + (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) = (2 ยท
((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))))) |
97 | 96 | oveq1d 7376 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((--(2 ยท
(๐ต ยท ๐ถ)) + (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐)) = ((2 ยท ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท)))) / (2 ยท ๐))) |
98 | 49, 94 | addcld 11182 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) โ โ) |
99 | | 2ne0 12265 |
. . . . . . . . 9
โข 2 โ
0 |
100 | 99 | a1i 11 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ 2 โ
0) |
101 | 98, 12, 40, 39, 100 | divcan5d 11965 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((2 ยท
((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท)))) / (2 ยท ๐)) = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐)) |
102 | 97, 101 | eqtrd 2773 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((--(2 ยท
(๐ต ยท ๐ถ)) + (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐)) = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐)) |
103 | 102 | eqeq2d 2744 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ = ((--(2 ยท (๐ต ยท ๐ถ)) + (โโ((-(2 ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท (๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท ๐)) โ ๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐))) |
104 | 85 | oveq2d 7377 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((2 ยท (๐ต ยท ๐ถ)) โ ((2 ยท (absโ๐ด)) ยท (โโ๐ท))) = ((2 ยท (๐ต ยท ๐ถ)) โ (2 ยท ((absโ๐ด) ยท (โโ๐ท))))) |
105 | 87, 92 | oveq12d 7379 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (--(2 ยท
(๐ต ยท ๐ถ)) โ (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) = ((2 ยท
(๐ต ยท ๐ถ)) โ ((2 ยท
(absโ๐ด)) ยท
(โโ๐ท)))) |
106 | 40, 49, 94 | subdid 11619 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (2 ยท ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท)))) = ((2 ยท (๐ต ยท ๐ถ)) โ (2 ยท ((absโ๐ด) ยท (โโ๐ท))))) |
107 | 104, 105,
106 | 3eqtr4d 2783 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (--(2 ยท
(๐ต ยท ๐ถ)) โ (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) = (2 ยท
((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))))) |
108 | 107 | oveq1d 7376 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((--(2 ยท
(๐ต ยท ๐ถ)) โ (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐)) = ((2 ยท ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท)))) / (2 ยท ๐))) |
109 | 49, 94 | subcld 11520 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) โ โ) |
110 | 109, 12, 40, 39, 100 | divcan5d 11965 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((2 ยท
((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท)))) / (2 ยท ๐)) = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) |
111 | 108, 110 | eqtrd 2773 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((--(2 ยท
(๐ต ยท ๐ถ)) โ (โโ((-(2
ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐)) = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) |
112 | 111 | eqeq2d 2744 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (๐ = ((--(2 ยท (๐ต ยท ๐ถ)) โ (โโ((-(2 ยท
(๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐)) โ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐))) |
113 | 103, 112 | orbi12d 918 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ = ((--(2 ยท (๐ต ยท ๐ถ)) + (โโ((-(2 ยท (๐ต ยท ๐ถ))โ2) โ (4 ยท (๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท ๐)) โจ ๐ = ((--(2 ยท (๐ต ยท ๐ถ)) โ (โโ((-(2 ยท
(๐ต ยท ๐ถ))โ2) โ (4 ยท
(๐ ยท ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2)))))))) / (2 ยท
๐))) โ (๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)))) |
114 | 68, 113 | bitrd 279 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0 โ (๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)))) |
115 | | absid 15190 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง 0 โค
๐ด) โ (absโ๐ด) = ๐ด) |
116 | 115 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ (0 โค
๐ด โ (absโ๐ด) = ๐ด)) |
117 | 116 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (0 โค
๐ด โ (absโ๐ด) = ๐ด)) |
118 | 117 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ (0 โค ๐ด โ (absโ๐ด) = ๐ด)) |
119 | 118 | 3ad2ant1 1134 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (0 โค ๐ด โ (absโ๐ด) = ๐ด)) |
120 | 119 | impcom 409 |
. . . . . . . . . 10
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (absโ๐ด) = ๐ด) |
121 | 120 | oveq1d 7376 |
. . . . . . . . 9
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((absโ๐ด) ยท (โโ๐ท)) = (๐ด ยท (โโ๐ท))) |
122 | 121 | oveq2d 7377 |
. . . . . . . 8
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท)))) |
123 | 122 | oveq1d 7376 |
. . . . . . 7
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)) |
124 | 123 | eqeq2d 2744 |
. . . . . 6
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))) |
125 | 121 | oveq2d 7377 |
. . . . . . . 8
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท)))) |
126 | 125 | oveq1d 7376 |
. . . . . . 7
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐) = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) |
127 | 126 | eqeq2d 2744 |
. . . . . 6
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐) โ ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐))) |
128 | 124, 127 | orbi12d 918 |
. . . . 5
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)))) |
129 | | pm1.4 868 |
. . . . 5
โข ((๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))) |
130 | 128, 129 | syl6bi 253 |
. . . 4
โข ((0 โค
๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |
131 | 49 | adantl 483 |
. . . . . . . . . 10
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (๐ต ยท ๐ถ) โ โ) |
132 | 94 | adantl 483 |
. . . . . . . . . 10
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((absโ๐ด) ยท (โโ๐ท)) โ
โ) |
133 | 131, 132 | subnegd 11527 |
. . . . . . . . 9
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) โ -((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท)))) |
134 | 73 | adantl 483 |
. . . . . . . . . . . 12
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (absโ๐ด) โ
โ) |
135 | 84 | adantl 483 |
. . . . . . . . . . . 12
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ
(โโ๐ท) โ
โ) |
136 | 134, 135 | mulneg1d 11616 |
. . . . . . . . . . 11
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (-(absโ๐ด) ยท (โโ๐ท)) = -((absโ๐ด) ยท (โโ๐ท))) |
137 | 89 | simp1d 1143 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ โ) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ๐ด โ โ) |
139 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โ โ ๐ด โ
โ) |
140 | | 0red 11166 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด โ โ โ 0 โ
โ) |
141 | 139, 140 | ltnled 11310 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ด โ โ โ (๐ด < 0 โ ยฌ 0 โค
๐ด)) |
142 | | ltle 11251 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โ โง 0 โ
โ) โ (๐ด < 0
โ ๐ด โค
0)) |
143 | 140, 142 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ด โ โ โ (๐ด < 0 โ ๐ด โค 0)) |
144 | 141, 143 | sylbird 260 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ โ (ยฌ 0
โค ๐ด โ ๐ด โค 0)) |
145 | 144 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (ยฌ 0
โค ๐ด โ ๐ด โค 0)) |
146 | 145 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ (ยฌ 0 โค ๐ด โ ๐ด โค 0)) |
147 | 146 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (ยฌ 0 โค ๐ด โ ๐ด โค 0)) |
148 | 147 | impcom 409 |
. . . . . . . . . . . . . . 15
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ๐ด โค 0) |
149 | 138, 148 | absnidd 15307 |
. . . . . . . . . . . . . 14
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (absโ๐ด) = -๐ด) |
150 | 149 | negeqd 11403 |
. . . . . . . . . . . . 13
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ -(absโ๐ด) = --๐ด) |
151 | 56 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ๐ด โ โ) |
152 | 151 | negnegd 11511 |
. . . . . . . . . . . . 13
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ --๐ด = ๐ด) |
153 | 150, 152 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ -(absโ๐ด) = ๐ด) |
154 | 153 | oveq1d 7376 |
. . . . . . . . . . 11
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (-(absโ๐ด) ยท (โโ๐ท)) = (๐ด ยท (โโ๐ท))) |
155 | 136, 154 | eqtr3d 2775 |
. . . . . . . . . 10
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ -((absโ๐ด) ยท (โโ๐ท)) = (๐ด ยท (โโ๐ท))) |
156 | 155 | oveq2d 7377 |
. . . . . . . . 9
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) โ -((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท)))) |
157 | 133, 156 | eqtr3d 2775 |
. . . . . . . 8
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท)))) |
158 | 157 | oveq1d 7376 |
. . . . . . 7
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) |
159 | 158 | eqeq2d 2744 |
. . . . . 6
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โ ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐))) |
160 | 131, 132 | negsubd 11526 |
. . . . . . . . 9
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) + -((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท)))) |
161 | 155 | oveq2d 7377 |
. . . . . . . . 9
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) + -((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท)))) |
162 | 160, 161 | eqtr3d 2775 |
. . . . . . . 8
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) = ((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท)))) |
163 | 162 | oveq1d 7376 |
. . . . . . 7
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐) = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)) |
164 | 163 | eqeq2d 2744 |
. . . . . 6
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ (๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐) โ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))) |
165 | 159, 164 | orbi12d 918 |
. . . . 5
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |
166 | 165 | biimpd 228 |
. . . 4
โข ((ยฌ 0
โค ๐ด โง (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ))) โ ((๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |
167 | 130, 166 | pm2.61ian 811 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ = (((๐ต ยท ๐ถ) + ((absโ๐ด) ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) โ ((absโ๐ด) ยท (โโ๐ท))) / ๐)) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |
168 | 114, 167 | sylbid 239 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ (((๐ ยท (๐โ2)) + ((-(2 ยท (๐ต ยท ๐ถ)) ยท ๐) + ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))))) = 0 โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |
169 | 6, 168 | syld 47 |
1
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ (๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐) โจ ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))) |