Step | Hyp | Ref
| Expression |
1 | | 4re 12245 |
. . . . 5
โข 4 โ
โ |
2 | 1 | a1i 11 |
. . . 4
โข (๐ โ 4 โ
โ) |
3 | | 2itscp.d |
. . . . . . . 8
โข ๐ท = (๐ โ ๐ด) |
4 | | 2itscp.x |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
5 | | 2itscp.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
6 | 4, 5 | resubcld 11591 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐ด) โ โ) |
7 | 3, 6 | eqeltrid 2838 |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
8 | 7 | resqcld 14039 |
. . . . . 6
โข (๐ โ (๐ทโ2) โ โ) |
9 | | 2itscp.c |
. . . . . . . 8
โข ๐ถ = ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) |
10 | | 2itscp.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
11 | 7, 10 | remulcld 11193 |
. . . . . . . . 9
โข (๐ โ (๐ท ยท ๐ต) โ โ) |
12 | | 2itscp.e |
. . . . . . . . . . 11
โข ๐ธ = (๐ต โ ๐) |
13 | | 2itscp.y |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
14 | 10, 13 | resubcld 11591 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โ ๐) โ โ) |
15 | 12, 14 | eqeltrid 2838 |
. . . . . . . . . 10
โข (๐ โ ๐ธ โ โ) |
16 | 15, 5 | remulcld 11193 |
. . . . . . . . 9
โข (๐ โ (๐ธ ยท ๐ด) โ โ) |
17 | 11, 16 | readdcld 11192 |
. . . . . . . 8
โข (๐ โ ((๐ท ยท ๐ต) + (๐ธ ยท ๐ด)) โ โ) |
18 | 9, 17 | eqeltrid 2838 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
19 | 18 | resqcld 14039 |
. . . . . 6
โข (๐ โ (๐ถโ2) โ โ) |
20 | 8, 19 | remulcld 11193 |
. . . . 5
โข (๐ โ ((๐ทโ2) ยท (๐ถโ2)) โ โ) |
21 | 15 | resqcld 14039 |
. . . . . . 7
โข (๐ โ (๐ธโ2) โ โ) |
22 | 21, 8 | readdcld 11192 |
. . . . . 6
โข (๐ โ ((๐ธโ2) + (๐ทโ2)) โ โ) |
23 | | 2itscp.r |
. . . . . . . . 9
โข (๐ โ ๐
โ โ) |
24 | 23 | resqcld 14039 |
. . . . . . . 8
โข (๐ โ (๐
โ2) โ โ) |
25 | 21, 24 | remulcld 11193 |
. . . . . . 7
โข (๐ โ ((๐ธโ2) ยท (๐
โ2)) โ โ) |
26 | 19, 25 | resubcld 11591 |
. . . . . 6
โข (๐ โ ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))) โ โ) |
27 | 22, 26 | remulcld 11193 |
. . . . 5
โข (๐ โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))) โ โ) |
28 | 20, 27 | resubcld 11591 |
. . . 4
โข (๐ โ (((๐ทโ2) ยท (๐ถโ2)) โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))) โ
โ) |
29 | | 4pos 12268 |
. . . . 5
โข 0 <
4 |
30 | 29 | a1i 11 |
. . . 4
โข (๐ โ 0 < 4) |
31 | 8, 24 | remulcld 11193 |
. . . . . . . . 9
โข (๐ โ ((๐ทโ2) ยท (๐
โ2)) โ โ) |
32 | 25, 31 | readdcld 11192 |
. . . . . . . 8
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ โ) |
33 | 32, 19 | resubcld 11591 |
. . . . . . 7
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2)) โ โ) |
34 | 12 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐ธ = (๐ต โ ๐)) |
35 | 10 | recnd 11191 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
36 | 13 | recnd 11191 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
37 | | itscnhlinecirc02plem1.n |
. . . . . . . . . 10
โข (๐ โ ๐ต โ ๐) |
38 | 35, 36, 37 | subne0d 11529 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐) โ 0) |
39 | 34, 38 | eqnetrd 3008 |
. . . . . . . 8
โข (๐ โ ๐ธ โ 0) |
40 | 15, 39 | sqgt0d 14162 |
. . . . . . 7
โข (๐ โ 0 < (๐ธโ2)) |
41 | | 2itscp.l |
. . . . . . . . 9
โข (๐ โ ((๐ดโ2) + (๐ตโ2)) < (๐
โ2)) |
42 | 37 | orcd 872 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐ โจ ๐ด โ ๐)) |
43 | | eqid 2733 |
. . . . . . . . 9
โข ((๐ธโ2) + (๐ทโ2)) = ((๐ธโ2) + (๐ทโ2)) |
44 | | eqid 2733 |
. . . . . . . . 9
โข (((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2))) โ (๐ถโ2)) = (((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2))) โ (๐ถโ2)) |
45 | 5, 10, 4, 13, 3, 12, 9, 23, 41, 42, 43, 44 | 2itscp 46957 |
. . . . . . . 8
โข (๐ โ 0 < (((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2))) โ (๐ถโ2))) |
46 | 21 | recnd 11191 |
. . . . . . . . . . 11
โข (๐ โ (๐ธโ2) โ โ) |
47 | 8 | recnd 11191 |
. . . . . . . . . . 11
โข (๐ โ (๐ทโ2) โ โ) |
48 | 24 | recnd 11191 |
. . . . . . . . . . 11
โข (๐ โ (๐
โ2) โ โ) |
49 | 46, 47, 48 | adddird 11188 |
. . . . . . . . . 10
โข (๐ โ (((๐ธโ2) + (๐ทโ2)) ยท (๐
โ2)) = (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) |
50 | 46, 47 | addcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((๐ธโ2) + (๐ทโ2)) โ โ) |
51 | 50, 48 | mulcomd 11184 |
. . . . . . . . . 10
โข (๐ โ (((๐ธโ2) + (๐ทโ2)) ยท (๐
โ2)) = ((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2)))) |
52 | 49, 51 | eqtr3d 2775 |
. . . . . . . . 9
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) = ((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2)))) |
53 | 52 | oveq1d 7376 |
. . . . . . . 8
โข (๐ โ ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2)) = (((๐
โ2) ยท ((๐ธโ2) + (๐ทโ2))) โ (๐ถโ2))) |
54 | 45, 53 | breqtrrd 5137 |
. . . . . . 7
โข (๐ โ 0 < ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2))) |
55 | 21, 33, 40, 54 | mulgt0d 11318 |
. . . . . 6
โข (๐ โ 0 < ((๐ธโ2) ยท ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2)))) |
56 | 47, 46, 48 | mul12d 11372 |
. . . . . . . . . 10
โข (๐ โ ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2))) = ((๐ธโ2) ยท ((๐ทโ2) ยท (๐
โ2)))) |
57 | 56 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) = (((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ธโ2) ยท ((๐ทโ2) ยท (๐
โ2))))) |
58 | 46, 48 | mulcld 11183 |
. . . . . . . . . 10
โข (๐ โ ((๐ธโ2) ยท (๐
โ2)) โ โ) |
59 | 47, 48 | mulcld 11183 |
. . . . . . . . . 10
โข (๐ โ ((๐ทโ2) ยท (๐
โ2)) โ โ) |
60 | 46, 58, 59 | adddid 11187 |
. . . . . . . . 9
โข (๐ โ ((๐ธโ2) ยท (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) = (((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ธโ2) ยท ((๐ทโ2) ยท (๐
โ2))))) |
61 | 57, 60 | eqtr4d 2776 |
. . . . . . . 8
โข (๐ โ (((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) = ((๐ธโ2) ยท (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))))) |
62 | 61 | oveq1d 7376 |
. . . . . . 7
โข (๐ โ ((((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2))) = (((๐ธโ2) ยท (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2)))) |
63 | 58, 59 | addcld 11182 |
. . . . . . . 8
โข (๐ โ (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ โ) |
64 | 19 | recnd 11191 |
. . . . . . . 8
โข (๐ โ (๐ถโ2) โ โ) |
65 | 46, 63, 64 | subdid 11619 |
. . . . . . 7
โข (๐ โ ((๐ธโ2) ยท ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2))) = (((๐ธโ2) ยท (((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2)))) |
66 | 62, 65 | eqtr4d 2776 |
. . . . . 6
โข (๐ โ ((((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2))) = ((๐ธโ2) ยท ((((๐ธโ2) ยท (๐
โ2)) + ((๐ทโ2) ยท (๐
โ2))) โ (๐ถโ2)))) |
67 | 55, 66 | breqtrrd 5137 |
. . . . 5
โข (๐ โ 0 < ((((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2)))) |
68 | 15 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐ธ โ โ) |
69 | 68 | sqcld 14058 |
. . . . . 6
โข (๐ โ (๐ธโ2) โ โ) |
70 | 7 | recnd 11191 |
. . . . . . 7
โข (๐ โ ๐ท โ โ) |
71 | 70 | sqcld 14058 |
. . . . . 6
โข (๐ โ (๐ทโ2) โ โ) |
72 | 25 | recnd 11191 |
. . . . . 6
โข (๐ โ ((๐ธโ2) ยท (๐
โ2)) โ โ) |
73 | | mulsubaddmulsub 11627 |
. . . . . 6
โข ((((๐ธโ2) โ โ โง
(๐ทโ2) โ โ)
โง ((๐ถโ2) โ
โ โง ((๐ธโ2)
ยท (๐
โ2)) โ
โ)) โ (((๐ทโ2) ยท (๐ถโ2)) โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))) = ((((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2)))) |
74 | 69, 71, 64, 72, 73 | syl22anc 838 |
. . . . 5
โข (๐ โ (((๐ทโ2) ยท (๐ถโ2)) โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))) = ((((๐ธโ2) ยท ((๐ธโ2) ยท (๐
โ2))) + ((๐ทโ2) ยท ((๐ธโ2) ยท (๐
โ2)))) โ ((๐ธโ2) ยท (๐ถโ2)))) |
75 | 67, 74 | breqtrrd 5137 |
. . . 4
โข (๐ โ 0 < (((๐ทโ2) ยท (๐ถโ2)) โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) |
76 | 2, 28, 30, 75 | mulgt0d 11318 |
. . 3
โข (๐ โ 0 < (4 ยท
(((๐ทโ2) ยท
(๐ถโ2)) โ
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
77 | | 4cn 12246 |
. . . . 5
โข 4 โ
โ |
78 | 77 | a1i 11 |
. . . 4
โข (๐ โ 4 โ
โ) |
79 | 18 | recnd 11191 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
80 | 79 | sqcld 14058 |
. . . . 5
โข (๐ โ (๐ถโ2) โ โ) |
81 | 71, 80 | mulcld 11183 |
. . . 4
โข (๐ โ ((๐ทโ2) ยท (๐ถโ2)) โ โ) |
82 | 69, 71 | addcld 11182 |
. . . . 5
โข (๐ โ ((๐ธโ2) + (๐ทโ2)) โ โ) |
83 | 23 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐
โ โ) |
84 | 83 | sqcld 14058 |
. . . . . . 7
โข (๐ โ (๐
โ2) โ โ) |
85 | 69, 84 | mulcld 11183 |
. . . . . 6
โข (๐ โ ((๐ธโ2) ยท (๐
โ2)) โ โ) |
86 | 80, 85 | subcld 11520 |
. . . . 5
โข (๐ โ ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))) โ โ) |
87 | 82, 86 | mulcld 11183 |
. . . 4
โข (๐ โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))) โ โ) |
88 | 78, 81, 87 | subdid 11619 |
. . 3
โข (๐ โ (4 ยท (((๐ทโ2) ยท (๐ถโ2)) โ (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) = ((4 ยท ((๐ทโ2) ยท (๐ถโ2))) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
89 | 76, 88 | breqtrd 5135 |
. 2
โข (๐ โ 0 < ((4 ยท
((๐ทโ2) ยท (๐ถโ2))) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
90 | | 2cnd 12239 |
. . . . . 6
โข (๐ โ 2 โ
โ) |
91 | 70, 79 | mulcld 11183 |
. . . . . 6
โข (๐ โ (๐ท ยท ๐ถ) โ โ) |
92 | 90, 91 | mulcld 11183 |
. . . . 5
โข (๐ โ (2 ยท (๐ท ยท ๐ถ)) โ โ) |
93 | | sqneg 14030 |
. . . . 5
โข ((2
ยท (๐ท ยท ๐ถ)) โ โ โ (-(2
ยท (๐ท ยท ๐ถ))โ2) = ((2 ยท (๐ท ยท ๐ถ))โ2)) |
94 | 92, 93 | syl 17 |
. . . 4
โข (๐ โ (-(2 ยท (๐ท ยท ๐ถ))โ2) = ((2 ยท (๐ท ยท ๐ถ))โ2)) |
95 | 90, 91 | sqmuld 14072 |
. . . 4
โข (๐ โ ((2 ยท (๐ท ยท ๐ถ))โ2) = ((2โ2) ยท ((๐ท ยท ๐ถ)โ2))) |
96 | | sq2 14110 |
. . . . . 6
โข
(2โ2) = 4 |
97 | 96 | a1i 11 |
. . . . 5
โข (๐ โ (2โ2) =
4) |
98 | 70, 79 | sqmuld 14072 |
. . . . 5
โข (๐ โ ((๐ท ยท ๐ถ)โ2) = ((๐ทโ2) ยท (๐ถโ2))) |
99 | 97, 98 | oveq12d 7379 |
. . . 4
โข (๐ โ ((2โ2) ยท
((๐ท ยท ๐ถ)โ2)) = (4 ยท ((๐ทโ2) ยท (๐ถโ2)))) |
100 | 94, 95, 99 | 3eqtrd 2777 |
. . 3
โข (๐ โ (-(2 ยท (๐ท ยท ๐ถ))โ2) = (4 ยท ((๐ทโ2) ยท (๐ถโ2)))) |
101 | 100 | oveq1d 7376 |
. 2
โข (๐ โ ((-(2 ยท (๐ท ยท ๐ถ))โ2) โ (4 ยท (((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2)))))) = ((4 ยท ((๐ทโ2) ยท (๐ถโ2))) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |
102 | 89, 101 | breqtrrd 5137 |
1
โข (๐ โ 0 < ((-(2 ยท
(๐ท ยท ๐ถ))โ2) โ (4 ยท
(((๐ธโ2) + (๐ทโ2)) ยท ((๐ถโ2) โ ((๐ธโ2) ยท (๐
โ2))))))) |