Step | Hyp | Ref
| Expression |
1 | | chordthmlem3.Q |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
2 | | chordthmlem3.M |
. . . . . . . . . 10
โข (๐ โ ๐ = ((๐ด + ๐ต) / 2)) |
3 | | chordthmlem3.A |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
4 | | chordthmlem3.B |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ โ) |
5 | 3, 4 | addcld 11181 |
. . . . . . . . . . 11
โข (๐ โ (๐ด + ๐ต) โ โ) |
6 | 5 | halfcld 12405 |
. . . . . . . . . 10
โข (๐ โ ((๐ด + ๐ต) / 2) โ โ) |
7 | 2, 6 | eqeltrd 2838 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
8 | 1, 7 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) โ โ) |
9 | 8 | abscld 15328 |
. . . . . . 7
โข (๐ โ (absโ(๐ โ ๐)) โ โ) |
10 | 9 | recnd 11190 |
. . . . . 6
โข (๐ โ (absโ(๐ โ ๐)) โ โ) |
11 | 10 | sqcld 14056 |
. . . . 5
โข (๐ โ ((absโ(๐ โ ๐))โ2) โ โ) |
12 | 11 | adantr 482 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) โ โ) |
13 | 12 | addid1d 11362 |
. . 3
โข ((๐ โง ๐ = ๐) โ (((absโ(๐ โ ๐))โ2) + 0) = ((absโ(๐ โ ๐))โ2)) |
14 | | chordthmlem3.P |
. . . . . . . . 9
โข (๐ โ ๐ = ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต))) |
15 | | chordthmlem3.X |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
16 | 15 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
17 | 16, 3 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท ๐ด) โ โ) |
18 | | 1cnd 11157 |
. . . . . . . . . . . 12
โข (๐ โ 1 โ
โ) |
19 | 18, 16 | subcld 11519 |
. . . . . . . . . . 11
โข (๐ โ (1 โ ๐) โ
โ) |
20 | 19, 4 | mulcld 11182 |
. . . . . . . . . 10
โข (๐ โ ((1 โ ๐) ยท ๐ต) โ โ) |
21 | 17, 20 | addcld 11181 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต)) โ โ) |
22 | 14, 21 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
23 | 22 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ = ๐) โ ๐ โ โ) |
24 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ = ๐) โ ๐ = ๐) |
25 | 23, 24 | subeq0bd 11588 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ (๐ โ ๐) = 0) |
26 | 25 | abs00bd 15183 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = 0) |
27 | 26 | sq0id 14105 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = 0) |
28 | 27 | oveq2d 7378 |
. . 3
โข ((๐ โง ๐ = ๐) โ (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2)) = (((absโ(๐ โ ๐))โ2) + 0)) |
29 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ ๐ โ โ) |
30 | 29, 23 | abssubd 15345 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐))) |
31 | 24 | oveq2d 7378 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ (๐ โ ๐) = (๐ โ ๐)) |
32 | 31 | fveq2d 6851 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐))) |
33 | 30, 32 | eqtr3d 2779 |
. . . 4
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐))) |
34 | 33 | oveq1d 7377 |
. . 3
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = ((absโ(๐ โ ๐))โ2)) |
35 | 13, 28, 34 | 3eqtr4rd 2788 |
. 2
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2))) |
36 | 22, 7 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) โ โ) |
37 | 36 | abscld 15328 |
. . . . . . 7
โข (๐ โ (absโ(๐ โ ๐)) โ โ) |
38 | 37 | recnd 11190 |
. . . . . 6
โข (๐ โ (absโ(๐ โ ๐)) โ โ) |
39 | 38 | sqcld 14056 |
. . . . 5
โข (๐ โ ((absโ(๐ โ ๐))โ2) โ โ) |
40 | 39 | adantr 482 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) โ โ) |
41 | 40 | addid2d 11363 |
. . 3
โข ((๐ โง ๐ = ๐) โ (0 + ((absโ(๐ โ ๐))โ2)) = ((absโ(๐ โ ๐))โ2)) |
42 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ = ๐) โ ๐ โ โ) |
43 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ = ๐) โ ๐ = ๐) |
44 | 42, 43 | subeq0bd 11588 |
. . . . . 6
โข ((๐ โง ๐ = ๐) โ (๐ โ ๐) = 0) |
45 | 44 | abs00bd 15183 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = 0) |
46 | 45 | sq0id 14105 |
. . . 4
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = 0) |
47 | 46 | oveq1d 7377 |
. . 3
โข ((๐ โง ๐ = ๐) โ (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2)) = (0 + ((absโ(๐ โ ๐))โ2))) |
48 | 43 | oveq2d 7378 |
. . . . 5
โข ((๐ โง ๐ = ๐) โ (๐ โ ๐) = (๐ โ ๐)) |
49 | 48 | fveq2d 6851 |
. . . 4
โข ((๐ โง ๐ = ๐) โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐))) |
50 | 49 | oveq1d 7377 |
. . 3
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = ((absโ(๐ โ ๐))โ2)) |
51 | 41, 47, 50 | 3eqtr4rd 2788 |
. 2
โข ((๐ โง ๐ = ๐) โ ((absโ(๐ โ ๐))โ2) = (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2))) |
52 | 22 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ โ) |
53 | 1 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ โ) |
54 | 7 | adantr 482 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ โ) |
55 | | simprl 770 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
56 | | simprr 772 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
57 | | eqid 2737 |
. . . 4
โข (๐ฅ โ (โ โ {0}),
๐ฆ โ (โ โ
{0}) โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) |
58 | 3 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ด โ โ) |
59 | 4 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ต โ โ) |
60 | 15 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ โ) |
61 | 2 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ = ((๐ด + ๐ต) / 2)) |
62 | 14 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ = ((๐ ยท ๐ด) + ((1 โ ๐) ยท ๐ต))) |
63 | | chordthmlem3.ABequidistQ |
. . . . 5
โข (๐ โ (absโ(๐ด โ ๐)) = (absโ(๐ต โ ๐))) |
64 | 63 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (absโ(๐ด โ ๐)) = (absโ(๐ต โ ๐))) |
65 | 57, 58, 59, 53, 60, 61, 62, 64, 55, 56 | chordthmlem2 26199 |
. . 3
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ ๐)(๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ))))(๐ โ ๐)) โ {(ฯ / 2), -(ฯ /
2)}) |
66 | | eqid 2737 |
. . . 4
โข
(absโ(๐
โ ๐)) =
(absโ(๐ โ ๐)) |
67 | | eqid 2737 |
. . . 4
โข
(absโ(๐
โ ๐)) =
(absโ(๐ โ ๐)) |
68 | | eqid 2737 |
. . . 4
โข
(absโ(๐
โ ๐)) =
(absโ(๐ โ ๐)) |
69 | | eqid 2737 |
. . . 4
โข ((๐ โ ๐)(๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ))))(๐ โ ๐)) = ((๐ โ ๐)(๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ))))(๐ โ ๐)) |
70 | 57, 66, 67, 68, 69 | pythag 26183 |
. . 3
โข (((๐ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐ โ ๐ โง ๐ โ ๐) โง ((๐ โ ๐)(๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ))))(๐ โ ๐)) โ {(ฯ / 2), -(ฯ / 2)}) โ
((absโ(๐ โ
๐))โ2) =
(((absโ(๐ โ
๐))โ2) +
((absโ(๐ โ
๐))โ2))) |
71 | 52, 53, 54, 55, 56, 65, 70 | syl321anc 1393 |
. 2
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ((absโ(๐ โ ๐))โ2) = (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2))) |
72 | 35, 51, 71 | pm2.61da2ne 3034 |
1
โข (๐ โ ((absโ(๐ โ ๐))โ2) = (((absโ(๐ โ ๐))โ2) + ((absโ(๐ โ ๐))โ2))) |