Step | Hyp | Ref
| Expression |
1 | | ang180lem1.3 |
. . . . . . . . . 10
โข ๐ = (((๐ / i) / (2 ยท ฯ)) โ (1 /
2)) |
2 | | ang.1 |
. . . . . . . . . . . . . . . 16
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) |
3 | | ang180lem1.2 |
. . . . . . . . . . . . . . . 16
โข ๐ = (((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด)) |
4 | 2, 3, 1 | ang180lem2 26658 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-2 < ๐ โง ๐ < 1)) |
5 | 4 | simprd 495 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ < 1) |
6 | | 1e0p1 12716 |
. . . . . . . . . . . . . 14
โข 1 = (0 +
1) |
7 | 5, 6 | breqtrdi 5179 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ < (0 + 1)) |
8 | 2, 3, 1 | ang180lem1 26657 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โ โค โง (๐ / i) โ โ)) |
9 | 8 | simpld 494 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โค) |
10 | | 0z 12566 |
. . . . . . . . . . . . . 14
โข 0 โ
โค |
11 | | zleltp1 12610 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 0 โ
โค) โ (๐ โค 0
โ ๐ < (0 +
1))) |
12 | 9, 10, 11 | sylancl 585 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โค 0 โ ๐ < (0 + 1))) |
13 | 7, 12 | mpbird 257 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โค 0) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ โค 0) |
15 | | zlem1lt 12611 |
. . . . . . . . . . . . . 14
โข ((0
โ โค โง ๐
โ โค) โ (0 โค ๐ โ (0 โ 1) < ๐)) |
16 | 10, 9, 15 | sylancr 586 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (0 โค ๐ โ (0 โ 1) < ๐)) |
17 | | df-neg 11444 |
. . . . . . . . . . . . . 14
โข -1 = (0
โ 1) |
18 | 17 | breq1i 5145 |
. . . . . . . . . . . . 13
โข (-1 <
๐ โ (0 โ 1) <
๐) |
19 | 16, 18 | bitr4di 289 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (0 โค ๐ โ -1 < ๐)) |
20 | 19 | biimpar 477 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ 0 โค ๐) |
21 | 9 | zred 12663 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
22 | 21 | adantr 480 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ โ โ) |
23 | | 0re 11213 |
. . . . . . . . . . . 12
โข 0 โ
โ |
24 | | letri3 11296 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 0 โ
โ) โ (๐ = 0
โ (๐ โค 0 โง 0
โค ๐))) |
25 | 22, 23, 24 | sylancl 585 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ = 0 โ (๐ โค 0 โง 0 โค ๐))) |
26 | 14, 20, 25 | mpbir2and 710 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ = 0) |
27 | 1, 26 | eqtr3id 2778 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= 0) |
28 | | ax-1cn 11164 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
29 | | simp1 1133 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ โ) |
30 | | subcl 11456 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
31 | 28, 29, 30 | sylancr 586 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ โ) |
32 | | simp3 1135 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 1) |
33 | 32 | necomd 2988 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ 1 โ ๐ด) |
34 | | subeq0 11483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((1
โ โ โง ๐ด
โ โ) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
35 | 28, 29, 34 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
36 | 35 | necon3bid 2977 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) โ 0 โ 1 โ ๐ด)) |
37 | 33, 36 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ 0) |
38 | 31, 37 | reccld 11980 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ
โ) |
39 | 31, 37 | recne0d 11981 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ 0) |
40 | 38, 39 | logcld 26421 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ(1 / (1 โ
๐ด))) โ
โ) |
41 | | subcl 11456 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด โ
1) โ โ) |
42 | 29, 28, 41 | sylancl 585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ โ) |
43 | | simp2 1134 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 0) |
44 | 42, 29, 43 | divcld 11987 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ โ) |
45 | | subeq0 11483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด โ
1) = 0 โ ๐ด =
1)) |
46 | 29, 28, 45 | sylancl 585 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) = 0 โ ๐ด = 1)) |
47 | 46 | necon3bid 2977 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) โ 0 โ ๐ด โ 1)) |
48 | 32, 47 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ 0) |
49 | 42, 29, 48, 43 | divne0d 12003 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ 0) |
50 | 44, 49 | logcld 26421 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ((๐ด โ 1) / ๐ด)) โ โ) |
51 | 40, 50 | addcld 11230 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) โ โ) |
52 | | logcl 26419 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
53 | 52 | 3adant3 1129 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ๐ด) โ โ) |
54 | 51, 53 | addcld 11230 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด)) โ โ) |
55 | 3, 54 | eqeltrid 2829 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
56 | | ax-icn 11165 |
. . . . . . . . . . . . . 14
โข i โ
โ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ
โ) |
58 | | ine0 11646 |
. . . . . . . . . . . . . 14
โข i โ
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ 0) |
60 | 55, 57, 59 | divcld 11987 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ / i) โ โ) |
61 | | 2cn 12284 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
62 | | picn 26311 |
. . . . . . . . . . . . . 14
โข ฯ
โ โ |
63 | 61, 62 | mulcli 11218 |
. . . . . . . . . . . . 13
โข (2
ยท ฯ) โ โ |
64 | 63 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
โ) |
65 | | 2ne0 12313 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
66 | | pire 26310 |
. . . . . . . . . . . . . . 15
โข ฯ
โ โ |
67 | | pipos 26312 |
. . . . . . . . . . . . . . 15
โข 0 <
ฯ |
68 | 66, 67 | gt0ne0ii 11747 |
. . . . . . . . . . . . . 14
โข ฯ โ
0 |
69 | 61, 62, 65, 68 | mulne0i 11854 |
. . . . . . . . . . . . 13
โข (2
ยท ฯ) โ 0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
0) |
71 | 60, 64, 70 | divcld 11987 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
72 | 71 | adantr 480 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
73 | | halfcn 12424 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
74 | | subeq0 11483 |
. . . . . . . . . 10
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (1 / 2) โ โ) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= 0 โ ((๐ / i) / (2
ยท ฯ)) = (1 / 2))) |
75 | 72, 73, 74 | sylancl 585 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= 0 โ ((๐ / i) / (2
ยท ฯ)) = (1 / 2))) |
76 | 27, 75 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((๐ / i) / (2 ยท ฯ)) = (1 /
2)) |
77 | 60 | adantr 480 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ / i) โ โ) |
78 | 63 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (2 ยท ฯ) โ
โ) |
79 | 73 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (1 / 2) โ
โ) |
80 | 69 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (2 ยท ฯ) โ
0) |
81 | 77, 78, 79, 80 | divmuld 12009 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (((๐ / i) / (2 ยท ฯ)) = (1 / 2) โ
((2 ยท ฯ) ยท (1 / 2)) = (๐ / i))) |
82 | 76, 81 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((2 ยท ฯ) ยท (1 /
2)) = (๐ /
i)) |
83 | 63, 61, 65 | divreci 11956 |
. . . . . . . 8
โข ((2
ยท ฯ) / 2) = ((2 ยท ฯ) ยท (1 / 2)) |
84 | 62, 61, 65 | divcan3i 11957 |
. . . . . . . 8
โข ((2
ยท ฯ) / 2) = ฯ |
85 | 83, 84 | eqtr3i 2754 |
. . . . . . 7
โข ((2
ยท ฯ) ยท (1 / 2)) = ฯ |
86 | 82, 85 | eqtr3di 2779 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ / i) = ฯ) |
87 | 55 | adantr 480 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ โ โ) |
88 | 56 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ i โ โ) |
89 | 62 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ฯ โ
โ) |
90 | 58 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ i โ 0) |
91 | 87, 88, 89, 90 | divmuld 12009 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((๐ / i) = ฯ โ (i ยท ฯ) =
๐)) |
92 | 86, 91 | mpbid 231 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (i ยท ฯ) = ๐) |
93 | 92 | eqcomd 2730 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ = (i ยท ฯ)) |
94 | 93 | olcd 871 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
95 | 62, 56 | mulneg1i 11657 |
. . . . . . 7
โข (-ฯ
ยท i) = -(ฯ ยท i) |
96 | 62, 56 | mulcomi 11219 |
. . . . . . . 8
โข (ฯ
ยท i) = (i ยท ฯ) |
97 | 96 | negeqi 11450 |
. . . . . . 7
โข -(ฯ
ยท i) = -(i ยท ฯ) |
98 | 95, 97 | eqtri 2752 |
. . . . . 6
โข (-ฯ
ยท i) = -(i ยท ฯ) |
99 | 73, 63 | mulneg1i 11657 |
. . . . . . . . . 10
โข (-(1 / 2)
ยท (2 ยท ฯ)) = -((1 / 2) ยท (2 ยท
ฯ)) |
100 | 28, 61, 65 | divcan1i 11955 |
. . . . . . . . . . . . 13
โข ((1 / 2)
ยท 2) = 1 |
101 | 100 | oveq1i 7411 |
. . . . . . . . . . . 12
โข (((1 / 2)
ยท 2) ยท ฯ) = (1 ยท ฯ) |
102 | 73, 61, 62 | mulassi 11222 |
. . . . . . . . . . . 12
โข (((1 / 2)
ยท 2) ยท ฯ) = ((1 / 2) ยท (2 ยท
ฯ)) |
103 | 62 | mullidi 11216 |
. . . . . . . . . . . 12
โข (1
ยท ฯ) = ฯ |
104 | 101, 102,
103 | 3eqtr3i 2760 |
. . . . . . . . . . 11
โข ((1 / 2)
ยท (2 ยท ฯ)) = ฯ |
105 | 104 | negeqi 11450 |
. . . . . . . . . 10
โข -((1 / 2)
ยท (2 ยท ฯ)) = -ฯ |
106 | 99, 105 | eqtri 2752 |
. . . . . . . . 9
โข (-(1 / 2)
ยท (2 ยท ฯ)) = -ฯ |
107 | 28, 73 | negsubdii 11542 |
. . . . . . . . . . . . 13
โข -(1
โ (1 / 2)) = (-1 + (1 / 2)) |
108 | | 1mhlfehlf 12428 |
. . . . . . . . . . . . . 14
โข (1
โ (1 / 2)) = (1 / 2) |
109 | 108 | negeqi 11450 |
. . . . . . . . . . . . 13
โข -(1
โ (1 / 2)) = -(1 / 2) |
110 | 107, 109 | eqtr3i 2754 |
. . . . . . . . . . . 12
โข (-1 + (1
/ 2)) = -(1 / 2) |
111 | | simpr 484 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -1 = ๐) |
112 | 111, 1 | eqtrdi 2780 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -1 = (((๐ / i) / (2 ยท ฯ)) โ (1 /
2))) |
113 | 112 | oveq1d 7416 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-1 + (1 / 2)) = ((((๐ / i) / (2 ยท ฯ))
โ (1 / 2)) + (1 / 2))) |
114 | 110, 113 | eqtr3id 2778 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(1 / 2) = ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2))) |
115 | | npcan 11466 |
. . . . . . . . . . . . 13
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (1 / 2) โ โ) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
116 | 71, 73, 115 | sylancl 585 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
117 | 116 | adantr 480 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
118 | 114, 117 | eqtrd 2764 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(1 / 2) = ((๐ / i) / (2 ยท ฯ))) |
119 | 118 | oveq1d 7416 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-(1 / 2) ยท (2 ยท
ฯ)) = (((๐ / i) / (2
ยท ฯ)) ยท (2 ยท ฯ))) |
120 | 106, 119 | eqtr3id 2778 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -ฯ = (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ))) |
121 | 60, 64, 70 | divcan1d 11988 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) = (๐ /
i)) |
122 | 121 | adantr 480 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) = (๐ /
i)) |
123 | 120, 122 | eqtrd 2764 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -ฯ = (๐ / i)) |
124 | 123 | oveq1d 7416 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-ฯ ยท i) = ((๐ / i) ยท
i)) |
125 | 98, 124 | eqtr3id 2778 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(i ยท ฯ) = ((๐ / i) ยท
i)) |
126 | 55, 57, 59 | divcan1d 11988 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) ยท i) = ๐) |
127 | 126 | adantr 480 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ((๐ / i) ยท i) = ๐) |
128 | 125, 127 | eqtr2d 2765 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ๐ = -(i ยท ฯ)) |
129 | 128 | orcd 870 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
130 | | df-2 12272 |
. . . . . . . 8
โข 2 = (1 +
1) |
131 | 130 | negeqi 11450 |
. . . . . . 7
โข -2 = -(1
+ 1) |
132 | | negdi2 11515 |
. . . . . . . 8
โข ((1
โ โ โง 1 โ โ) โ -(1 + 1) = (-1 โ
1)) |
133 | 28, 28, 132 | mp2an 689 |
. . . . . . 7
โข -(1 + 1)
= (-1 โ 1) |
134 | 131, 133 | eqtri 2752 |
. . . . . 6
โข -2 = (-1
โ 1) |
135 | 4 | simpld 494 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -2 < ๐) |
136 | 134, 135 | eqbrtrrid 5174 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โ 1) < ๐) |
137 | | neg1z 12595 |
. . . . . 6
โข -1 โ
โค |
138 | | zlem1lt 12611 |
. . . . . 6
โข ((-1
โ โค โง ๐
โ โค) โ (-1 โค ๐ โ (-1 โ 1) < ๐)) |
139 | 137, 9, 138 | sylancr 586 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โค ๐ โ (-1 โ 1) < ๐)) |
140 | 136, 139 | mpbird 257 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -1 โค ๐) |
141 | | neg1rr 12324 |
. . . . 5
โข -1 โ
โ |
142 | | leloe 11297 |
. . . . 5
โข ((-1
โ โ โง ๐
โ โ) โ (-1 โค ๐ โ (-1 < ๐ โจ -1 = ๐))) |
143 | 141, 21, 142 | sylancr 586 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โค ๐ โ (-1 < ๐ โจ -1 = ๐))) |
144 | 140, 143 | mpbid 231 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 < ๐ โจ -1 = ๐)) |
145 | 94, 129, 144 | mpjaodan 955 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
146 | 3 | ovexi 7435 |
. . 3
โข ๐ โ V |
147 | 146 | elpr 4643 |
. 2
โข (๐ โ {-(i ยท ฯ), (i
ยท ฯ)} โ (๐ =
-(i ยท ฯ) โจ ๐ =
(i ยท ฯ))) |
148 | 145, 147 | sylibr 233 |
1
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ {-(i ยท ฯ), (i ยท
ฯ)}) |