Step | Hyp | Ref
| Expression |
1 | | simpl1l 1224 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐ด โ โ) |
2 | | simpl1r 1225 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐ต โ โ) |
3 | | simpl2l 1226 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐ โ โ) |
4 | | simpl2r 1227 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐ โ โ) |
5 | | itscnhlinecirc02plem2.d |
. . 3
โข ๐ท = (๐ โ ๐ด) |
6 | | itscnhlinecirc02plem2.e |
. . 3
โข ๐ธ = (๐ต โ ๐) |
7 | | eqid 2736 |
. . 3
โข ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) = ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) |
8 | | simprl 769 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐
โ โ) |
9 | | simprr 771 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ((๐ดโ2) + (๐ตโ2)) < (๐
โ2)) |
10 | | simpl3 1193 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ๐ต โ ๐) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | itscnhlinecirc02plem1 46186 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ 0 < ((-(2 ยท
(๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
12 | | simplr 767 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ต โ
โ) |
13 | 12 | recnd 11049 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ต โ
โ) |
14 | | simprl 769 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
15 | 14 | recnd 11049 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
16 | 13, 15 | mulcomd 11042 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ต ยท ๐) = (๐ ยท ๐ต)) |
17 | | simpll 765 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ
โ) |
18 | 17 | recnd 11049 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ
โ) |
19 | | simprr 771 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
20 | 19 | recnd 11049 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ
โ) |
21 | 18, 20 | mulcomd 11042 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ด ยท ๐) = (๐ ยท ๐ด)) |
22 | 16, 21 | oveq12d 7325 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต ยท ๐) โ (๐ด ยท ๐)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
23 | 15, 18, 13 | subdird 11478 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ โ ๐ด) ยท ๐ต) = ((๐ ยท ๐ต) โ (๐ด ยท ๐ต))) |
24 | 13, 20, 18 | subdird 11478 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต โ ๐) ยท ๐ด) = ((๐ต ยท ๐ด) โ (๐ ยท ๐ด))) |
25 | 23, 24 | oveq12d 7325 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ โ ๐ด) ยท ๐ต) + ((๐ต โ ๐) ยท ๐ด)) = (((๐ ยท ๐ต) โ (๐ด ยท ๐ต)) + ((๐ต ยท ๐ด) โ (๐ ยท ๐ด)))) |
26 | 13, 18 | mulcomd 11042 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ต ยท ๐ด) = (๐ด ยท ๐ต)) |
27 | 26 | oveq1d 7322 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) = ((๐ด ยท ๐ต) โ (๐ ยท ๐ด))) |
28 | 27 | oveq2d 7323 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ ยท ๐ต) โ (๐ด ยท ๐ต)) + ((๐ต ยท ๐ด) โ (๐ ยท ๐ด))) = (((๐ ยท ๐ต) โ (๐ด ยท ๐ต)) + ((๐ด ยท ๐ต) โ (๐ ยท ๐ด)))) |
29 | 15, 13 | mulcld 11041 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐ต) โ โ) |
30 | 18, 13 | mulcld 11041 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ด ยท ๐ต) โ โ) |
31 | 20, 18 | mulcld 11041 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ ยท ๐ด) โ โ) |
32 | 29, 30, 31 | npncand 11402 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ ยท ๐ต) โ (๐ด ยท ๐ต)) + ((๐ด ยท ๐ต) โ (๐ ยท ๐ด))) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
33 | 25, 28, 32 | 3eqtrd 2780 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ โ ๐ด) ยท ๐ต) + ((๐ต โ ๐) ยท ๐ด)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
34 | 22, 33 | eqtr4d 2779 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ต ยท ๐) โ (๐ด ยท ๐)) = (((๐ โ ๐ด) ยท ๐ต) + ((๐ต โ ๐) ยท ๐ด))) |
35 | | itscnhlinecirc02plem2.c |
. . . . . . . . . 10
โข ๐ถ = ((๐ต ยท ๐) โ (๐ด ยท ๐)) |
36 | 5 | oveq1i 7317 |
. . . . . . . . . . 11
โข (๐ท ยท ๐ต) = ((๐ โ ๐ด) ยท ๐ต) |
37 | 6 | oveq1i 7317 |
. . . . . . . . . . 11
โข (๐ธ ยท ๐ด) = ((๐ต โ ๐) ยท ๐ด) |
38 | 36, 37 | oveq12i 7319 |
. . . . . . . . . 10
โข ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) = (((๐ โ ๐ด) ยท ๐ต) + ((๐ต โ ๐) ยท ๐ด)) |
39 | 34, 35, 38 | 3eqtr4g 2801 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ๐ถ = ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))) |
40 | 39 | oveq2d 7323 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ท ยท ๐ถ) = (๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)))) |
41 | 40 | oveq2d 7323 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (2
ยท (๐ท ยท ๐ถ)) = (2 ยท (๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))) |
42 | 41 | negeqd 11261 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ -(2
ยท (๐ท ยท ๐ถ)) = -(2 ยท (๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))) |
43 | 42 | oveq1d 7322 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (-(2
ยท (๐ท ยท ๐ถ))โ2) = (-(2 ยท
(๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))โ2)) |
44 | 39 | oveq1d 7322 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (๐ถโ2) = (((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2)) |
45 | 44 | oveq1d 7322 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))) = ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2)))) |
46 | 45 | oveq2d 7323 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))) = (((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2))))) |
47 | 46 | oveq2d 7323 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ (4
ยท (((๐ธโ2) +
(๐ทโ2)) ยท
((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))) = (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2)))))) |
48 | 43, 47 | oveq12d 7325 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ)) โ ((-(2
ยท (๐ท ยท ๐ถ))โ2) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) = ((-(2 ยท
(๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
49 | 48 | 3adant3 1132 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โ ((-(2 ยท (๐ท ยท ๐ถ))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) = ((-(2 ยท (๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
50 | 49 | adantr 482 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ ((-(2 ยท (๐ท ยท ๐ถ))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) = ((-(2 ยท (๐ท ยท ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((((๐ท ยท ๐ต) + (๐ธ ยท ๐ด))โ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
51 | 11, 50 | breqtrrd 5109 |
1
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ โ โ โง ๐ โ โ) โง ๐ต โ ๐) โง (๐
โ โ โง ((๐ดโ2) + (๐ตโ2)) < (๐
โ2))) โ 0 < ((-(2 ยท
(๐ท ยท ๐ถ))โ2) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |