Step | Hyp | Ref
| Expression |
1 | | negpitopissre 25912 |
. . . . . 6
โข
(-ฯ(,]ฯ) โ โ |
2 | | chordthmlem.angdef |
. . . . . . 7
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) |
3 | | chordthmlem.Q |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
4 | | chordthmlem.M |
. . . . . . . . 9
โข (๐ โ ๐ = ((๐ด + ๐ต) / 2)) |
5 | | chordthmlem.A |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โ) |
6 | | chordthmlem.B |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
7 | 5, 6 | addcld 11181 |
. . . . . . . . . 10
โข (๐ โ (๐ด + ๐ต) โ โ) |
8 | 7 | halfcld 12405 |
. . . . . . . . 9
โข (๐ โ ((๐ด + ๐ต) / 2) โ โ) |
9 | 4, 8 | eqeltrd 2838 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
10 | 3, 9 | subcld 11519 |
. . . . . . 7
โข (๐ โ (๐ โ ๐) โ โ) |
11 | | chordthmlem.QneM |
. . . . . . . 8
โข (๐ โ ๐ โ ๐) |
12 | 3, 9, 11 | subne0d 11528 |
. . . . . . 7
โข (๐ โ (๐ โ ๐) โ 0) |
13 | 6, 9 | subcld 11519 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐) โ โ) |
14 | 4 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท 2) = (((๐ด + ๐ต) / 2) ยท 2)) |
15 | 9 | times2d 12404 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท 2) = (๐ + ๐)) |
16 | | 2cnd 12238 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ
โ) |
17 | | 2ne0 12264 |
. . . . . . . . . . . . . . . 16
โข 2 โ
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 2 โ 0) |
19 | 7, 16, 18 | divcan1d 11939 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ด + ๐ต) / 2) ยท 2) = (๐ด + ๐ต)) |
20 | 14, 15, 19 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + ๐) = (๐ด + ๐ต)) |
21 | | chordthmlem.AneB |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ ๐ต) |
22 | 5, 6, 6, 21 | addneintr2d 11370 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด + ๐ต) โ (๐ต + ๐ต)) |
23 | 20, 22 | eqnetrd 3012 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + ๐) โ (๐ต + ๐ต)) |
24 | 23 | neneqd 2949 |
. . . . . . . . . . 11
โข (๐ โ ยฌ (๐ + ๐) = (๐ต + ๐ต)) |
25 | | oveq12 7371 |
. . . . . . . . . . . 12
โข ((๐ = ๐ต โง ๐ = ๐ต) โ (๐ + ๐) = (๐ต + ๐ต)) |
26 | 25 | anidms 568 |
. . . . . . . . . . 11
โข (๐ = ๐ต โ (๐ + ๐) = (๐ต + ๐ต)) |
27 | 24, 26 | nsyl 140 |
. . . . . . . . . 10
โข (๐ โ ยฌ ๐ = ๐ต) |
28 | 27 | neqned 2951 |
. . . . . . . . 9
โข (๐ โ ๐ โ ๐ต) |
29 | 28 | necomd 3000 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐) |
30 | 6, 9, 29 | subne0d 11528 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐) โ 0) |
31 | 2, 10, 12, 13, 30 | angcld 26171 |
. . . . . 6
โข (๐ โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ (-ฯ(,]ฯ)) |
32 | 1, 31 | sselid 3947 |
. . . . 5
โข (๐ โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ โ) |
33 | 32 | recnd 11190 |
. . . 4
โข (๐ โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ โ) |
34 | 33 | coscld 16020 |
. . 3
โข (๐ โ (cosโ((๐ โ ๐)๐น(๐ต โ ๐))) โ โ) |
35 | 6, 9 | negsubdi2d 11535 |
. . . . . . 7
โข (๐ โ -(๐ต โ ๐) = (๐ โ ๐ต)) |
36 | 9, 9, 5, 6 | addsubeq4d 11570 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐) = (๐ด + ๐ต) โ (๐ด โ ๐) = (๐ โ ๐ต))) |
37 | 20, 36 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ด โ ๐) = (๐ โ ๐ต)) |
38 | 35, 37 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ -(๐ต โ ๐) = (๐ด โ ๐)) |
39 | 38 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((๐ โ ๐)๐น-(๐ต โ ๐)) = ((๐ โ ๐)๐น(๐ด โ ๐))) |
40 | 39 | fveq2d 6851 |
. . . 4
โข (๐ โ (cosโ((๐ โ ๐)๐น-(๐ต โ ๐))) = (cosโ((๐ โ ๐)๐น(๐ด โ ๐)))) |
41 | 2, 10, 12, 13, 30 | cosangneg2d 26173 |
. . . 4
โข (๐ โ (cosโ((๐ โ ๐)๐น-(๐ต โ ๐))) = -(cosโ((๐ โ ๐)๐น(๐ต โ ๐)))) |
42 | 5, 5, 6, 21 | addneintrd 11369 |
. . . . . . . . . 10
โข (๐ โ (๐ด + ๐ด) โ (๐ด + ๐ต)) |
43 | 42, 20 | neeqtrrd 3019 |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐ด) โ (๐ + ๐)) |
44 | 43 | necomd 3000 |
. . . . . . . 8
โข (๐ โ (๐ + ๐) โ (๐ด + ๐ด)) |
45 | 44 | neneqd 2949 |
. . . . . . 7
โข (๐ โ ยฌ (๐ + ๐) = (๐ด + ๐ด)) |
46 | | oveq12 7371 |
. . . . . . . 8
โข ((๐ = ๐ด โง ๐ = ๐ด) โ (๐ + ๐) = (๐ด + ๐ด)) |
47 | 46 | anidms 568 |
. . . . . . 7
โข (๐ = ๐ด โ (๐ + ๐) = (๐ด + ๐ด)) |
48 | 45, 47 | nsyl 140 |
. . . . . 6
โข (๐ โ ยฌ ๐ = ๐ด) |
49 | 48 | neqned 2951 |
. . . . 5
โข (๐ โ ๐ โ ๐ด) |
50 | | eqidd 2738 |
. . . . 5
โข (๐ โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐))) |
51 | 5, 9 | subcld 11519 |
. . . . . . 7
โข (๐ โ (๐ด โ ๐) โ โ) |
52 | 51 | absnegd 15341 |
. . . . . 6
โข (๐ โ (absโ-(๐ด โ ๐)) = (absโ(๐ด โ ๐))) |
53 | 5, 9 | negsubdi2d 11535 |
. . . . . . 7
โข (๐ โ -(๐ด โ ๐) = (๐ โ ๐ด)) |
54 | 53 | fveq2d 6851 |
. . . . . 6
โข (๐ โ (absโ-(๐ด โ ๐)) = (absโ(๐ โ ๐ด))) |
55 | 37 | fveq2d 6851 |
. . . . . 6
โข (๐ โ (absโ(๐ด โ ๐)) = (absโ(๐ โ ๐ต))) |
56 | 52, 54, 55 | 3eqtr3d 2785 |
. . . . 5
โข (๐ โ (absโ(๐ โ ๐ด)) = (absโ(๐ โ ๐ต))) |
57 | | chordthmlem.ABequidistQ |
. . . . 5
โข (๐ โ (absโ(๐ด โ ๐)) = (absโ(๐ต โ ๐))) |
58 | 2, 3, 9, 5, 3, 9, 6, 11, 49, 11, 28, 50, 56, 57 | ssscongptld 26188 |
. . . 4
โข (๐ โ (cosโ((๐ โ ๐)๐น(๐ด โ ๐))) = (cosโ((๐ โ ๐)๐น(๐ต โ ๐)))) |
59 | 40, 41, 58 | 3eqtr3rd 2786 |
. . 3
โข (๐ โ (cosโ((๐ โ ๐)๐น(๐ต โ ๐))) = -(cosโ((๐ โ ๐)๐น(๐ต โ ๐)))) |
60 | 34, 59 | eqnegad 11884 |
. 2
โข (๐ โ (cosโ((๐ โ ๐)๐น(๐ต โ ๐))) = 0) |
61 | | coseq0negpitopi 25876 |
. . 3
โข (((๐ โ ๐)๐น(๐ต โ ๐)) โ (-ฯ(,]ฯ) โ
((cosโ((๐ โ
๐)๐น(๐ต โ ๐))) = 0 โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ {(ฯ / 2), -(ฯ /
2)})) |
62 | 31, 61 | syl 17 |
. 2
โข (๐ โ ((cosโ((๐ โ ๐)๐น(๐ต โ ๐))) = 0 โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ {(ฯ / 2), -(ฯ /
2)})) |
63 | 60, 62 | mpbid 231 |
1
โข (๐ โ ((๐ โ ๐)๐น(๐ต โ ๐)) โ {(ฯ / 2), -(ฯ /
2)}) |