Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
2 | | unitssre 13423 |
. . . . . . . . 9
โข (0[,]1)
โ โ |
3 | | chordthmlem4.X |
. . . . . . . . 9
โข (๐ โ ๐ โ (0[,]1)) |
4 | 2, 3 | sselid 3947 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
5 | 1, 4 | resubcld 11590 |
. . . . . . 7
โข (๐ โ (1 โ ๐) โ
โ) |
6 | 5 | recnd 11190 |
. . . . . 6
โข (๐ โ (1 โ ๐) โ
โ) |
7 | 6 | abscld 15328 |
. . . . 5
โข (๐ โ (absโ(1 โ
๐)) โ
โ) |
8 | 7 | recnd 11190 |
. . . 4
โข (๐ โ (absโ(1 โ
๐)) โ
โ) |
9 | | chordthmlem4.B |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
10 | | chordthmlem4.A |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
11 | 9, 10 | subcld 11519 |
. . . . . 6
โข (๐ โ (๐ต โ ๐ด) โ โ) |
12 | 11 | abscld 15328 |
. . . . 5
โข (๐ โ (absโ(๐ต โ ๐ด)) โ โ) |
13 | 12 | recnd 11190 |
. . . 4
โข (๐ โ (absโ(๐ต โ ๐ด)) โ โ) |
14 | 4 | recnd 11190 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
15 | 14 | abscld 15328 |
. . . . 5
โข (๐ โ (absโ๐) โ
โ) |
16 | 15 | recnd 11190 |
. . . 4
โข (๐ โ (absโ๐) โ
โ) |
17 | 8, 13, 16, 13 | mul4d 11374 |
. . 3
โข (๐ โ (((absโ(1 โ
๐)) ยท
(absโ(๐ต โ ๐ด))) ยท ((absโ๐) ยท (absโ(๐ต โ ๐ด)))) = (((absโ(1 โ ๐)) ยท (absโ๐)) ยท ((absโ(๐ต โ ๐ด)) ยท (absโ(๐ต โ ๐ด))))) |
18 | | chordthmlem4.P |
. . . . . . 7
โข (๐ โ ๐ = ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต))) |
19 | 14, 10 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท ๐ด) โ โ) |
20 | 6, 9 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((1 โ ๐) ยท ๐ต) โ โ) |
21 | 19, 20 | addcld 11181 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต)) โ โ) |
22 | 18, 21 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
23 | 10, 22, 9, 14 | affineequiv2 26190 |
. . . . . . 7
โข (๐ โ (๐ = ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต)) โ (๐ โ ๐ด) = ((1 โ ๐) ยท (๐ต โ ๐ด)))) |
24 | 18, 23 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ โ ๐ด) = ((1 โ ๐) ยท (๐ต โ ๐ด))) |
25 | 24 | fveq2d 6851 |
. . . . 5
โข (๐ โ (absโ(๐ โ ๐ด)) = (absโ((1 โ ๐) ยท (๐ต โ ๐ด)))) |
26 | 6, 11 | absmuld 15346 |
. . . . 5
โข (๐ โ (absโ((1 โ
๐) ยท (๐ต โ ๐ด))) = ((absโ(1 โ ๐)) ยท (absโ(๐ต โ ๐ด)))) |
27 | 25, 26 | eqtrd 2777 |
. . . 4
โข (๐ โ (absโ(๐ โ ๐ด)) = ((absโ(1 โ ๐)) ยท (absโ(๐ต โ ๐ด)))) |
28 | 22, 9 | abssubd 15345 |
. . . . 5
โข (๐ โ (absโ(๐ โ ๐ต)) = (absโ(๐ต โ ๐))) |
29 | 10, 22, 9, 14 | affineequiv 26189 |
. . . . . . 7
โข (๐ โ (๐ = ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต)) โ (๐ต โ ๐) = (๐ ยท (๐ต โ ๐ด)))) |
30 | 18, 29 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ต โ ๐) = (๐ ยท (๐ต โ ๐ด))) |
31 | 30 | fveq2d 6851 |
. . . . 5
โข (๐ โ (absโ(๐ต โ ๐)) = (absโ(๐ ยท (๐ต โ ๐ด)))) |
32 | 14, 11 | absmuld 15346 |
. . . . 5
โข (๐ โ (absโ(๐ ยท (๐ต โ ๐ด))) = ((absโ๐) ยท (absโ(๐ต โ ๐ด)))) |
33 | 28, 31, 32 | 3eqtrd 2781 |
. . . 4
โข (๐ โ (absโ(๐ โ ๐ต)) = ((absโ๐) ยท (absโ(๐ต โ ๐ด)))) |
34 | 27, 33 | oveq12d 7380 |
. . 3
โข (๐ โ ((absโ(๐ โ ๐ด)) ยท (absโ(๐ โ ๐ต))) = (((absโ(1 โ ๐)) ยท (absโ(๐ต โ ๐ด))) ยท ((absโ๐) ยท (absโ(๐ต โ ๐ด))))) |
35 | 13 | sqvald 14055 |
. . . 4
โข (๐ โ ((absโ(๐ต โ ๐ด))โ2) = ((absโ(๐ต โ ๐ด)) ยท (absโ(๐ต โ ๐ด)))) |
36 | 35 | oveq2d 7378 |
. . 3
โข (๐ โ (((absโ(1 โ
๐)) ยท
(absโ๐)) ยท
((absโ(๐ต โ
๐ด))โ2)) =
(((absโ(1 โ ๐))
ยท (absโ๐))
ยท ((absโ(๐ต
โ ๐ด)) ยท
(absโ(๐ต โ ๐ด))))) |
37 | 17, 34, 36 | 3eqtr4d 2787 |
. 2
โข (๐ โ ((absโ(๐ โ ๐ด)) ยท (absโ(๐ โ ๐ต))) = (((absโ(1 โ ๐)) ยท (absโ๐)) ยท ((absโ(๐ต โ ๐ด))โ2))) |
38 | 1 | recnd 11190 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
39 | 38 | halfcld 12405 |
. . . . 5
โข (๐ โ (1 / 2) โ
โ) |
40 | 39 | sqcld 14056 |
. . . 4
โข (๐ โ ((1 / 2)โ2) โ
โ) |
41 | 1 | rehalfcld 12407 |
. . . . . . . . 9
โข (๐ โ (1 / 2) โ
โ) |
42 | 41, 4 | resubcld 11590 |
. . . . . . . 8
โข (๐ โ ((1 / 2) โ ๐) โ
โ) |
43 | 42 | recnd 11190 |
. . . . . . 7
โข (๐ โ ((1 / 2) โ ๐) โ
โ) |
44 | 43 | abscld 15328 |
. . . . . 6
โข (๐ โ (absโ((1 / 2)
โ ๐)) โ
โ) |
45 | 44 | recnd 11190 |
. . . . 5
โข (๐ โ (absโ((1 / 2)
โ ๐)) โ
โ) |
46 | 45 | sqcld 14056 |
. . . 4
โข (๐ โ ((absโ((1 / 2)
โ ๐))โ2) โ
โ) |
47 | 13 | sqcld 14056 |
. . . 4
โข (๐ โ ((absโ(๐ต โ ๐ด))โ2) โ โ) |
48 | 40, 46, 47 | subdird 11619 |
. . 3
โข (๐ โ ((((1 / 2)โ2) โ
((absโ((1 / 2) โ ๐))โ2)) ยท ((absโ(๐ต โ ๐ด))โ2)) = ((((1 / 2)โ2) ยท
((absโ(๐ต โ
๐ด))โ2)) โ
(((absโ((1 / 2) โ ๐))โ2) ยท ((absโ(๐ต โ ๐ด))โ2)))) |
49 | | subsq 14121 |
. . . . . . 7
โข (((1 / 2)
โ โ โง ((1 / 2) โ ๐) โ โ) โ (((1 / 2)โ2)
โ (((1 / 2) โ ๐)โ2)) = (((1 / 2) + ((1 / 2) โ
๐)) ยท ((1 / 2)
โ ((1 / 2) โ ๐)))) |
50 | 39, 43, 49 | syl2anc 585 |
. . . . . 6
โข (๐ โ (((1 / 2)โ2) โ
(((1 / 2) โ ๐)โ2)) = (((1 / 2) + ((1 / 2) โ
๐)) ยท ((1 / 2)
โ ((1 / 2) โ ๐)))) |
51 | 39, 39, 14 | addsubassd 11539 |
. . . . . . . 8
โข (๐ โ (((1 / 2) + (1 / 2))
โ ๐) = ((1 / 2) + ((1
/ 2) โ ๐))) |
52 | 38 | 2halvesd 12406 |
. . . . . . . . 9
โข (๐ โ ((1 / 2) + (1 / 2)) =
1) |
53 | 52 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ (((1 / 2) + (1 / 2))
โ ๐) = (1 โ
๐)) |
54 | 51, 53 | eqtr3d 2779 |
. . . . . . 7
โข (๐ โ ((1 / 2) + ((1 / 2)
โ ๐)) = (1 โ
๐)) |
55 | 39, 14 | nncand 11524 |
. . . . . . 7
โข (๐ โ ((1 / 2) โ ((1 / 2)
โ ๐)) = ๐) |
56 | 54, 55 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (((1 / 2) + ((1 / 2)
โ ๐)) ยท ((1 /
2) โ ((1 / 2) โ ๐))) = ((1 โ ๐) ยท ๐)) |
57 | 50, 56 | eqtr2d 2778 |
. . . . 5
โข (๐ โ ((1 โ ๐) ยท ๐) = (((1 / 2)โ2) โ (((1 / 2)
โ ๐)โ2))) |
58 | | elicc01 13390 |
. . . . . . . . 9
โข (๐ โ (0[,]1) โ (๐ โ โ โง 0 โค
๐ โง ๐ โค 1)) |
59 | 3, 58 | sylib 217 |
. . . . . . . 8
โข (๐ โ (๐ โ โ โง 0 โค ๐ โง ๐ โค 1)) |
60 | 59 | simp3d 1145 |
. . . . . . 7
โข (๐ โ ๐ โค 1) |
61 | 4, 1, 60 | abssubge0d 15323 |
. . . . . 6
โข (๐ โ (absโ(1 โ
๐)) = (1 โ ๐)) |
62 | 59 | simp2d 1144 |
. . . . . . 7
โข (๐ โ 0 โค ๐) |
63 | 4, 62 | absidd 15314 |
. . . . . 6
โข (๐ โ (absโ๐) = ๐) |
64 | 61, 63 | oveq12d 7380 |
. . . . 5
โข (๐ โ ((absโ(1 โ
๐)) ยท
(absโ๐)) = ((1
โ ๐) ยท ๐)) |
65 | | absresq 15194 |
. . . . . . 7
โข (((1 / 2)
โ ๐) โ โ
โ ((absโ((1 / 2) โ ๐))โ2) = (((1 / 2) โ ๐)โ2)) |
66 | 42, 65 | syl 17 |
. . . . . 6
โข (๐ โ ((absโ((1 / 2)
โ ๐))โ2) = (((1
/ 2) โ ๐)โ2)) |
67 | 66 | oveq2d 7378 |
. . . . 5
โข (๐ โ (((1 / 2)โ2) โ
((absโ((1 / 2) โ ๐))โ2)) = (((1 / 2)โ2) โ (((1
/ 2) โ ๐)โ2))) |
68 | 57, 64, 67 | 3eqtr4d 2787 |
. . . 4
โข (๐ โ ((absโ(1 โ
๐)) ยท
(absโ๐)) = (((1 /
2)โ2) โ ((absโ((1 / 2) โ ๐))โ2))) |
69 | 68 | oveq1d 7377 |
. . 3
โข (๐ โ (((absโ(1 โ
๐)) ยท
(absโ๐)) ยท
((absโ(๐ต โ
๐ด))โ2)) = ((((1 /
2)โ2) โ ((absโ((1 / 2) โ ๐))โ2)) ยท ((absโ(๐ต โ ๐ด))โ2))) |
70 | | 2cnd 12238 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ
โ) |
71 | | 2ne0 12264 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 2 โ 0) |
73 | 9, 70, 72 | divcan4d 11944 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ต ยท 2) / 2) = ๐ต) |
74 | 9 | times2d 12404 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ต ยท 2) = (๐ต + ๐ต)) |
75 | 74 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ต ยท 2) / 2) = ((๐ต + ๐ต) / 2)) |
76 | 73, 75 | eqtr3d 2779 |
. . . . . . . . . . 11
โข (๐ โ ๐ต = ((๐ต + ๐ต) / 2)) |
77 | | chordthmlem4.M |
. . . . . . . . . . 11
โข (๐ โ ๐ = ((๐ด + ๐ต) / 2)) |
78 | 76, 77 | oveq12d 7380 |
. . . . . . . . . 10
โข (๐ โ (๐ต โ ๐) = (((๐ต + ๐ต) / 2) โ ((๐ด + ๐ต) / 2))) |
79 | 9, 9 | addcld 11181 |
. . . . . . . . . . 11
โข (๐ โ (๐ต + ๐ต) โ โ) |
80 | 10, 9 | addcld 11181 |
. . . . . . . . . . 11
โข (๐ โ (๐ด + ๐ต) โ โ) |
81 | 79, 80, 70, 72 | divsubdird 11977 |
. . . . . . . . . 10
โข (๐ โ (((๐ต + ๐ต) โ (๐ด + ๐ต)) / 2) = (((๐ต + ๐ต) / 2) โ ((๐ด + ๐ต) / 2))) |
82 | 9, 10, 9 | pnpcan2d 11557 |
. . . . . . . . . . 11
โข (๐ โ ((๐ต + ๐ต) โ (๐ด + ๐ต)) = (๐ต โ ๐ด)) |
83 | 82 | oveq1d 7377 |
. . . . . . . . . 10
โข (๐ โ (((๐ต + ๐ต) โ (๐ด + ๐ต)) / 2) = ((๐ต โ ๐ด) / 2)) |
84 | 78, 81, 83 | 3eqtr2d 2783 |
. . . . . . . . 9
โข (๐ โ (๐ต โ ๐) = ((๐ต โ ๐ด) / 2)) |
85 | 11, 70, 72 | divrec2d 11942 |
. . . . . . . . 9
โข (๐ โ ((๐ต โ ๐ด) / 2) = ((1 / 2) ยท (๐ต โ ๐ด))) |
86 | 84, 85 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (๐ต โ ๐) = ((1 / 2) ยท (๐ต โ ๐ด))) |
87 | 86 | fveq2d 6851 |
. . . . . . 7
โข (๐ โ (absโ(๐ต โ ๐)) = (absโ((1 / 2) ยท (๐ต โ ๐ด)))) |
88 | 39, 11 | absmuld 15346 |
. . . . . . 7
โข (๐ โ (absโ((1 / 2)
ยท (๐ต โ ๐ด))) = ((absโ(1 / 2))
ยท (absโ(๐ต
โ ๐ด)))) |
89 | | 0red 11165 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ) |
90 | | halfgt0 12376 |
. . . . . . . . . . 11
โข 0 < (1
/ 2) |
91 | 90 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 0 < (1 /
2)) |
92 | 89, 41, 91 | ltled 11310 |
. . . . . . . . 9
โข (๐ โ 0 โค (1 /
2)) |
93 | 41, 92 | absidd 15314 |
. . . . . . . 8
โข (๐ โ (absโ(1 / 2)) = (1 /
2)) |
94 | 93 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ ((absโ(1 / 2))
ยท (absโ(๐ต
โ ๐ด))) = ((1 / 2)
ยท (absโ(๐ต
โ ๐ด)))) |
95 | 87, 88, 94 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ (absโ(๐ต โ ๐)) = ((1 / 2) ยท (absโ(๐ต โ ๐ด)))) |
96 | 95 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((absโ(๐ต โ ๐))โ2) = (((1 / 2) ยท
(absโ(๐ต โ ๐ด)))โ2)) |
97 | 39, 13 | sqmuld 14070 |
. . . . 5
โข (๐ โ (((1 / 2) ยท
(absโ(๐ต โ ๐ด)))โ2) = (((1 / 2)โ2)
ยท ((absโ(๐ต
โ ๐ด))โ2))) |
98 | 96, 97 | eqtrd 2777 |
. . . 4
โข (๐ โ ((absโ(๐ต โ ๐))โ2) = (((1 / 2)โ2) ยท
((absโ(๐ต โ
๐ด))โ2))) |
99 | 39, 14, 11 | subdird 11619 |
. . . . . . . . 9
โข (๐ โ (((1 / 2) โ ๐) ยท (๐ต โ ๐ด)) = (((1 / 2) ยท (๐ต โ ๐ด)) โ (๐ ยท (๐ต โ ๐ด)))) |
100 | 86, 30 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ ((๐ต โ ๐) โ (๐ต โ ๐)) = (((1 / 2) ยท (๐ต โ ๐ด)) โ (๐ ยท (๐ต โ ๐ด)))) |
101 | 80 | halfcld 12405 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด + ๐ต) / 2) โ โ) |
102 | 77, 101 | eqeltrd 2838 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
103 | 9, 102, 22 | nnncan1d 11553 |
. . . . . . . . 9
โข (๐ โ ((๐ต โ ๐) โ (๐ต โ ๐)) = (๐ โ ๐)) |
104 | 99, 100, 103 | 3eqtr2rd 2784 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) = (((1 / 2) โ ๐) ยท (๐ต โ ๐ด))) |
105 | 104 | fveq2d 6851 |
. . . . . . 7
โข (๐ โ (absโ(๐ โ ๐)) = (absโ(((1 / 2) โ ๐) ยท (๐ต โ ๐ด)))) |
106 | 43, 11 | absmuld 15346 |
. . . . . . 7
โข (๐ โ (absโ(((1 / 2)
โ ๐) ยท (๐ต โ ๐ด))) = ((absโ((1 / 2) โ ๐)) ยท (absโ(๐ต โ ๐ด)))) |
107 | 105, 106 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (absโ(๐ โ ๐)) = ((absโ((1 / 2) โ ๐)) ยท (absโ(๐ต โ ๐ด)))) |
108 | 107 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((absโ(๐ โ ๐))โ2) = (((absโ((1 / 2) โ
๐)) ยท
(absโ(๐ต โ ๐ด)))โ2)) |
109 | 45, 13 | sqmuld 14070 |
. . . . 5
โข (๐ โ (((absโ((1 / 2)
โ ๐)) ยท
(absโ(๐ต โ ๐ด)))โ2) = (((absโ((1 /
2) โ ๐))โ2)
ยท ((absโ(๐ต
โ ๐ด))โ2))) |
110 | 108, 109 | eqtrd 2777 |
. . . 4
โข (๐ โ ((absโ(๐ โ ๐))โ2) = (((absโ((1 / 2) โ
๐))โ2) ยท
((absโ(๐ต โ
๐ด))โ2))) |
111 | 98, 110 | oveq12d 7380 |
. . 3
โข (๐ โ (((absโ(๐ต โ ๐))โ2) โ ((absโ(๐ โ ๐))โ2)) = ((((1 / 2)โ2) ยท
((absโ(๐ต โ
๐ด))โ2)) โ
(((absโ((1 / 2) โ ๐))โ2) ยท ((absโ(๐ต โ ๐ด))โ2)))) |
112 | 48, 69, 111 | 3eqtr4rd 2788 |
. 2
โข (๐ โ (((absโ(๐ต โ ๐))โ2) โ ((absโ(๐ โ ๐))โ2)) = (((absโ(1 โ ๐)) ยท (absโ๐)) ยท ((absโ(๐ต โ ๐ด))โ2))) |
113 | 37, 112 | eqtr4d 2780 |
1
โข (๐ โ ((absโ(๐ โ ๐ด)) ยท (absโ(๐ โ ๐ต))) = (((absโ(๐ต โ ๐))โ2) โ ((absโ(๐ โ ๐))โ2))) |