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 26315 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-2 < ๐ โง ๐ < 1)) |
5 | 4 | simprd 497 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ < 1) |
6 | | 1e0p1 12719 |
. . . . . . . . . . . . . 14
โข 1 = (0 +
1) |
7 | 5, 6 | breqtrdi 5190 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ < (0 + 1)) |
8 | 2, 3, 1 | ang180lem1 26314 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โ โค โง (๐ / i) โ โ)) |
9 | 8 | simpld 496 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โค) |
10 | | 0z 12569 |
. . . . . . . . . . . . . 14
โข 0 โ
โค |
11 | | zleltp1 12613 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง 0 โ
โค) โ (๐ โค 0
โ ๐ < (0 +
1))) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ โค 0 โ ๐ < (0 + 1))) |
13 | 7, 12 | mpbird 257 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โค 0) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ โค 0) |
15 | | zlem1lt 12614 |
. . . . . . . . . . . . . 14
โข ((0
โ โค โง ๐
โ โค) โ (0 โค ๐ โ (0 โ 1) < ๐)) |
16 | 10, 9, 15 | sylancr 588 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (0 โค ๐ โ (0 โ 1) < ๐)) |
17 | | df-neg 11447 |
. . . . . . . . . . . . . 14
โข -1 = (0
โ 1) |
18 | 17 | breq1i 5156 |
. . . . . . . . . . . . 13
โข (-1 <
๐ โ (0 โ 1) <
๐) |
19 | 16, 18 | bitr4di 289 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (0 โค ๐ โ -1 < ๐)) |
20 | 19 | biimpar 479 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ 0 โค ๐) |
21 | 9 | zred 12666 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
22 | 21 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ โ โ) |
23 | | 0re 11216 |
. . . . . . . . . . . 12
โข 0 โ
โ |
24 | | letri3 11299 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 0 โ
โ) โ (๐ = 0
โ (๐ โค 0 โง 0
โค ๐))) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ = 0 โ (๐ โค 0 โง 0 โค ๐))) |
26 | 14, 20, 25 | mpbir2and 712 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ = 0) |
27 | 1, 26 | eqtr3id 2787 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= 0) |
28 | | ax-1cn 11168 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
29 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ โ) |
30 | | subcl 11459 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง ๐ด
โ โ) โ (1 โ ๐ด) โ โ) |
31 | 28, 29, 30 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ โ) |
32 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 1) |
33 | 32 | necomd 2997 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ 1 โ ๐ด) |
34 | | subeq0 11486 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((1
โ โ โง ๐ด
โ โ) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
35 | 28, 29, 34 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) = 0 โ 1 = ๐ด)) |
36 | 35 | necon3bid 2986 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((1 โ ๐ด) โ 0 โ 1 โ ๐ด)) |
37 | 33, 36 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 โ ๐ด) โ 0) |
38 | 31, 37 | reccld 11983 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ
โ) |
39 | 31, 37 | recne0d 11984 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (1 / (1 โ ๐ด)) โ 0) |
40 | 38, 39 | logcld 26079 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ(1 / (1 โ
๐ด))) โ
โ) |
41 | | subcl 11459 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง 1 โ
โ) โ (๐ด โ
1) โ โ) |
42 | 29, 28, 41 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ โ) |
43 | | simp2 1138 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ด โ 0) |
44 | 42, 29, 43 | divcld 11990 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ โ) |
45 | | subeq0 11486 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด โ
1) = 0 โ ๐ด =
1)) |
46 | 29, 28, 45 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) = 0 โ ๐ด = 1)) |
47 | 46 | necon3bid 2986 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) โ 0 โ ๐ด โ 1)) |
48 | 32, 47 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ด โ 1) โ 0) |
49 | 42, 29, 48, 43 | divne0d 12006 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ด โ 1) / ๐ด) โ 0) |
50 | 44, 49 | logcld 26079 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ((๐ด โ 1) / ๐ด)) โ โ) |
51 | 40, 50 | addcld 11233 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) โ โ) |
52 | | logcl 26077 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ด โ 0) โ (logโ๐ด) โ
โ) |
53 | 52 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (logโ๐ด) โ โ) |
54 | 51, 53 | addcld 11233 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((logโ(1 / (1 โ
๐ด))) + (logโ((๐ด โ 1) / ๐ด))) + (logโ๐ด)) โ โ) |
55 | 3, 54 | eqeltrid 2838 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ โ) |
56 | | ax-icn 11169 |
. . . . . . . . . . . . . 14
โข i โ
โ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ
โ) |
58 | | ine0 11649 |
. . . . . . . . . . . . . 14
โข i โ
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ i โ 0) |
60 | 55, 57, 59 | divcld 11990 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ / i) โ โ) |
61 | | 2cn 12287 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
62 | | picn 25969 |
. . . . . . . . . . . . . 14
โข ฯ
โ โ |
63 | 61, 62 | mulcli 11221 |
. . . . . . . . . . . . 13
โข (2
ยท ฯ) โ โ |
64 | 63 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
โ) |
65 | | 2ne0 12316 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
66 | | pire 25968 |
. . . . . . . . . . . . . . 15
โข ฯ
โ โ |
67 | | pipos 25970 |
. . . . . . . . . . . . . . 15
โข 0 <
ฯ |
68 | 66, 67 | gt0ne0ii 11750 |
. . . . . . . . . . . . . 14
โข ฯ โ
0 |
69 | 61, 62, 65, 68 | mulne0i 11857 |
. . . . . . . . . . . . 13
โข (2
ยท ฯ) โ 0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (2 ยท ฯ) โ
0) |
71 | 60, 64, 70 | divcld 11990 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
72 | 71 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((๐ / i) / (2 ยท ฯ)) โ
โ) |
73 | | halfcn 12427 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
74 | | subeq0 11486 |
. . . . . . . . . 10
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (1 / 2) โ โ) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
= 0 โ ((๐ / i) / (2
ยท ฯ)) = (1 / 2))) |
75 | 72, 73, 74 | sylancl 587 |
. . . . . . . . 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 482 |
. . . . . . . . 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 12012 |
. . . . . . . 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 11959 |
. . . . . . . 8
โข ((2
ยท ฯ) / 2) = ((2 ยท ฯ) ยท (1 / 2)) |
84 | 62, 61, 65 | divcan3i 11960 |
. . . . . . . 8
โข ((2
ยท ฯ) / 2) = ฯ |
85 | 83, 84 | eqtr3i 2763 |
. . . . . . 7
โข ((2
ยท ฯ) ยท (1 / 2)) = ฯ |
86 | 82, 85 | eqtr3di 2788 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ / i) = ฯ) |
87 | 55 | adantr 482 |
. . . . . . 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 12012 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ((๐ / i) = ฯ โ (i ยท ฯ) =
๐)) |
92 | 86, 91 | mpbid 231 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (i ยท ฯ) = ๐) |
93 | 92 | eqcomd 2739 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ ๐ = (i ยท ฯ)) |
94 | 93 | olcd 873 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 < ๐) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
95 | 62, 56 | mulneg1i 11660 |
. . . . . . 7
โข (-ฯ
ยท i) = -(ฯ ยท i) |
96 | 62, 56 | mulcomi 11222 |
. . . . . . . 8
โข (ฯ
ยท i) = (i ยท ฯ) |
97 | 96 | negeqi 11453 |
. . . . . . 7
โข -(ฯ
ยท i) = -(i ยท ฯ) |
98 | 95, 97 | eqtri 2761 |
. . . . . 6
โข (-ฯ
ยท i) = -(i ยท ฯ) |
99 | 73, 63 | mulneg1i 11660 |
. . . . . . . . . 10
โข (-(1 / 2)
ยท (2 ยท ฯ)) = -((1 / 2) ยท (2 ยท
ฯ)) |
100 | 28, 61, 65 | divcan1i 11958 |
. . . . . . . . . . . . 13
โข ((1 / 2)
ยท 2) = 1 |
101 | 100 | oveq1i 7419 |
. . . . . . . . . . . 12
โข (((1 / 2)
ยท 2) ยท ฯ) = (1 ยท ฯ) |
102 | 73, 61, 62 | mulassi 11225 |
. . . . . . . . . . . 12
โข (((1 / 2)
ยท 2) ยท ฯ) = ((1 / 2) ยท (2 ยท
ฯ)) |
103 | 62 | mullidi 11219 |
. . . . . . . . . . . 12
โข (1
ยท ฯ) = ฯ |
104 | 101, 102,
103 | 3eqtr3i 2769 |
. . . . . . . . . . 11
โข ((1 / 2)
ยท (2 ยท ฯ)) = ฯ |
105 | 104 | negeqi 11453 |
. . . . . . . . . 10
โข -((1 / 2)
ยท (2 ยท ฯ)) = -ฯ |
106 | 99, 105 | eqtri 2761 |
. . . . . . . . 9
โข (-(1 / 2)
ยท (2 ยท ฯ)) = -ฯ |
107 | 28, 73 | negsubdii 11545 |
. . . . . . . . . . . . 13
โข -(1
โ (1 / 2)) = (-1 + (1 / 2)) |
108 | | 1mhlfehlf 12431 |
. . . . . . . . . . . . . 14
โข (1
โ (1 / 2)) = (1 / 2) |
109 | 108 | negeqi 11453 |
. . . . . . . . . . . . 13
โข -(1
โ (1 / 2)) = -(1 / 2) |
110 | 107, 109 | eqtr3i 2763 |
. . . . . . . . . . . 12
โข (-1 + (1
/ 2)) = -(1 / 2) |
111 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -1 = ๐) |
112 | 111, 1 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -1 = (((๐ / i) / (2 ยท ฯ)) โ (1 /
2))) |
113 | 112 | oveq1d 7424 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-1 + (1 / 2)) = ((((๐ / i) / (2 ยท ฯ))
โ (1 / 2)) + (1 / 2))) |
114 | 110, 113 | eqtr3id 2787 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(1 / 2) = ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2))) |
115 | | npcan 11469 |
. . . . . . . . . . . . 13
โข ((((๐ / i) / (2 ยท ฯ))
โ โ โง (1 / 2) โ โ) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
116 | 71, 73, 115 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
117 | 116 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ((((๐ / i) / (2 ยท ฯ)) โ (1 / 2))
+ (1 / 2)) = ((๐ / i) / (2
ยท ฯ))) |
118 | 114, 117 | eqtrd 2773 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(1 / 2) = ((๐ / i) / (2 ยท ฯ))) |
119 | 118 | oveq1d 7424 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-(1 / 2) ยท (2 ยท
ฯ)) = (((๐ / i) / (2
ยท ฯ)) ยท (2 ยท ฯ))) |
120 | 106, 119 | eqtr3id 2787 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -ฯ = (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ))) |
121 | 60, 64, 70 | divcan1d 11991 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) = (๐ /
i)) |
122 | 121 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (((๐ / i) / (2 ยท ฯ)) ยท (2
ยท ฯ)) = (๐ /
i)) |
123 | 120, 122 | eqtrd 2773 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -ฯ = (๐ / i)) |
124 | 123 | oveq1d 7424 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (-ฯ ยท i) = ((๐ / i) ยท
i)) |
125 | 98, 124 | eqtr3id 2787 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ -(i ยท ฯ) = ((๐ / i) ยท
i)) |
126 | 55, 57, 59 | divcan1d 11991 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ((๐ / i) ยท i) = ๐) |
127 | 126 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ((๐ / i) ยท i) = ๐) |
128 | 125, 127 | eqtr2d 2774 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ ๐ = -(i ยท ฯ)) |
129 | 128 | orcd 872 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โง -1 = ๐) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
130 | | df-2 12275 |
. . . . . . . 8
โข 2 = (1 +
1) |
131 | 130 | negeqi 11453 |
. . . . . . 7
โข -2 = -(1
+ 1) |
132 | | negdi2 11518 |
. . . . . . . 8
โข ((1
โ โ โง 1 โ โ) โ -(1 + 1) = (-1 โ
1)) |
133 | 28, 28, 132 | mp2an 691 |
. . . . . . 7
โข -(1 + 1)
= (-1 โ 1) |
134 | 131, 133 | eqtri 2761 |
. . . . . 6
โข -2 = (-1
โ 1) |
135 | 4 | simpld 496 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -2 < ๐) |
136 | 134, 135 | eqbrtrrid 5185 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โ 1) < ๐) |
137 | | neg1z 12598 |
. . . . . 6
โข -1 โ
โค |
138 | | zlem1lt 12614 |
. . . . . 6
โข ((-1
โ โค โง ๐
โ โค) โ (-1 โค ๐ โ (-1 โ 1) < ๐)) |
139 | 137, 9, 138 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โค ๐ โ (-1 โ 1) < ๐)) |
140 | 136, 139 | mpbird 257 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ -1 โค ๐) |
141 | | neg1rr 12327 |
. . . . 5
โข -1 โ
โ |
142 | | leloe 11300 |
. . . . 5
โข ((-1
โ โ โง ๐
โ โ) โ (-1 โค ๐ โ (-1 < ๐ โจ -1 = ๐))) |
143 | 141, 21, 142 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 โค ๐ โ (-1 < ๐ โจ -1 = ๐))) |
144 | 140, 143 | mpbid 231 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (-1 < ๐ โจ -1 = ๐)) |
145 | 94, 129, 144 | mpjaodan 958 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ (๐ = -(i ยท ฯ) โจ ๐ = (i ยท ฯ))) |
146 | 3 | ovexi 7443 |
. . 3
โข ๐ โ V |
147 | 146 | elpr 4652 |
. 2
โข (๐ โ {-(i ยท ฯ), (i
ยท ฯ)} โ (๐ =
-(i ยท ฯ) โจ ๐ =
(i ยท ฯ))) |
148 | 145, 147 | sylibr 233 |
1
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ด โ 1) โ ๐ โ {-(i ยท ฯ), (i ยท
ฯ)}) |