Step | Hyp | Ref
| Expression |
1 | | 0zd 12567 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 โ โค) |
2 | | pire 26310 |
. . . . . . . . . 10
โข ฯ
โ โ |
3 | 2 | renegcli 11518 |
. . . . . . . . 9
โข -ฯ
โ โ |
4 | | iccssre 13403 |
. . . . . . . . 9
โข ((-ฯ
โ โ โง ฯ โ โ) โ (-ฯ[,]ฯ) โ
โ) |
5 | 3, 2, 4 | mp2an 689 |
. . . . . . . 8
โข
(-ฯ[,]ฯ) โ โ |
6 | | eldifi 4118 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
(-ฯ[,]ฯ)) |
7 | 5, 6 | sselid 3972 |
. . . . . . 7
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
โ) |
8 | 7 | adantr 480 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
๐ด โ
โ) |
9 | | 2re 12283 |
. . . . . . . 8
โข 2 โ
โ |
10 | 9, 2 | remulcli 11227 |
. . . . . . 7
โข (2
ยท ฯ) โ โ |
11 | 10 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(2 ยท ฯ) โ โ) |
12 | | simpr 484 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < ๐ด) |
13 | | 2pos 12312 |
. . . . . . . 8
โข 0 <
2 |
14 | | pipos 26312 |
. . . . . . . 8
โข 0 <
ฯ |
15 | 9, 2, 13, 14 | mulgt0ii 11344 |
. . . . . . 7
โข 0 < (2
ยท ฯ) |
16 | 15 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < (2 ยท ฯ)) |
17 | 8, 11, 12, 16 | divgt0d 12146 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < (๐ด / (2 ยท
ฯ))) |
18 | 11, 16 | elrpd 13010 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(2 ยท ฯ) โ โ+) |
19 | 2 | a1i 11 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ โ โ) |
20 | 10 | a1i 11 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ โ) |
21 | 3 | rexri 11269 |
. . . . . . . . . . . 12
โข -ฯ
โ โ* |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -ฯ โ โ*) |
23 | 19 | rexrd 11261 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ โ โ*) |
24 | | iccleub 13376 |
. . . . . . . . . . 11
โข ((-ฯ
โ โ* โง ฯ โ โ* โง ๐ด โ (-ฯ[,]ฯ)) โ
๐ด โค
ฯ) |
25 | 22, 23, 6, 24 | syl3anc 1368 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โค
ฯ) |
26 | | pirp 26313 |
. . . . . . . . . . 11
โข ฯ
โ โ+ |
27 | | 2timesgt 44483 |
. . . . . . . . . . 11
โข (ฯ
โ โ+ โ ฯ < (2 ยท ฯ)) |
28 | 26, 27 | mp1i 13 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ < (2 ยท ฯ)) |
29 | 7, 19, 20, 25, 28 | lelttrd 11369 |
. . . . . . . . 9
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด < (2
ยท ฯ)) |
30 | 29 | adantr 480 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
๐ด < (2 ยท
ฯ)) |
31 | 8, 11, 18, 30 | ltdiv1dd 13070 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< ((2 ยท ฯ) / (2 ยท ฯ))) |
32 | 10 | recni 11225 |
. . . . . . . 8
โข (2
ยท ฯ) โ โ |
33 | 10, 15 | gt0ne0ii 11747 |
. . . . . . . 8
โข (2
ยท ฯ) โ 0 |
34 | 32, 33 | dividi 11944 |
. . . . . . 7
โข ((2
ยท ฯ) / (2 ยท ฯ)) = 1 |
35 | 31, 34 | breqtrdi 5179 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< 1) |
36 | | 0p1e1 12331 |
. . . . . 6
โข (0 + 1) =
1 |
37 | 35, 36 | breqtrrdi 5180 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< (0 + 1)) |
38 | | btwnnz 12635 |
. . . . 5
โข ((0
โ โค โง 0 < (๐ด / (2 ยท ฯ)) โง (๐ด / (2 ยท ฯ)) < (0 +
1)) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
39 | 1, 17, 37, 38 | syl3anc 1368 |
. . . 4
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
ยฌ (๐ด / (2 ยท
ฯ)) โ โค) |
40 | | simpl 482 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โ
((-ฯ[,]ฯ) โ {0})) |
41 | 7 | adantr 480 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โ
โ) |
42 | | 0red 11214 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ 0 โ โ) |
43 | | simpr 484 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ยฌ 0 < ๐ด) |
44 | 41, 42, 43 | nltled 11361 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โค
0) |
45 | | eldifsni 4785 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
0) |
46 | 45 | necomd 2988 |
. . . . . . 7
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ 0 โ ๐ด) |
47 | 46 | adantr 480 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ 0 โ ๐ด) |
48 | 41, 42, 44, 47 | leneltd 11365 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด <
0) |
49 | | neg1z 12595 |
. . . . . . 7
โข -1 โ
โค |
50 | 49 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-1 โ โค) |
51 | 33 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ 0) |
52 | 7, 20, 51 | redivcld 12039 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (๐ด / (2
ยท ฯ)) โ โ) |
53 | 52 | adantr 480 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
โ โ) |
54 | | 1red 11212 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
1 โ โ) |
55 | 7 | recnd 11239 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
โ) |
56 | 55 | adantr 480 |
. . . . . . . . 9
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
๐ด โ
โ) |
57 | 32 | a1i 11 |
. . . . . . . . 9
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ โ) |
58 | 33 | a1i 11 |
. . . . . . . . 9
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ 0) |
59 | 56, 57, 58 | divnegd 12000 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-(๐ด / (2 ยท ฯ)) =
(-๐ด / (2 ยท
ฯ))) |
60 | 7 | renegcld 11638 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด โ
โ) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-๐ด โ
โ) |
62 | 10 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ โ) |
63 | | 2rp 12976 |
. . . . . . . . . . . 12
โข 2 โ
โ+ |
64 | | rpmulcl 12994 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง ฯ โ โ+) โ (2
ยท ฯ) โ โ+) |
65 | 63, 26, 64 | mp2an 689 |
. . . . . . . . . . 11
โข (2
ยท ฯ) โ โ+ |
66 | 65 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ โ+) |
67 | | iccgelb 13377 |
. . . . . . . . . . . . . 14
โข ((-ฯ
โ โ* โง ฯ โ โ* โง ๐ด โ (-ฯ[,]ฯ)) โ
-ฯ โค ๐ด) |
68 | 22, 23, 6, 67 | syl3anc 1368 |
. . . . . . . . . . . . 13
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -ฯ โค ๐ด) |
69 | 19, 7, 68 | lenegcon1d 11793 |
. . . . . . . . . . . 12
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด โค
ฯ) |
70 | 60, 19, 20, 69, 28 | lelttrd 11369 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด < (2
ยท ฯ)) |
71 | 70 | adantr 480 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-๐ด < (2 ยท
ฯ)) |
72 | 61, 62, 66, 71 | ltdiv1dd 13070 |
. . . . . . . . 9
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(-๐ด / (2 ยท ฯ))
< ((2 ยท ฯ) / (2 ยท ฯ))) |
73 | 72, 34 | breqtrdi 5179 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(-๐ด / (2 ยท ฯ))
< 1) |
74 | 59, 73 | eqbrtrd 5160 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-(๐ด / (2 ยท ฯ))
< 1) |
75 | 53, 54, 74 | ltnegcon1d 11791 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-1 < (๐ด / (2 ยท
ฯ))) |
76 | 7 | adantr 480 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
๐ด โ
โ) |
77 | | simpr 484 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
๐ด < 0) |
78 | 76, 66, 77 | divlt0gt0d 44481 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
< 0) |
79 | | neg1cn 12323 |
. . . . . . . . 9
โข -1 โ
โ |
80 | | ax-1cn 11164 |
. . . . . . . . 9
โข 1 โ
โ |
81 | 79, 80 | addcomi 11402 |
. . . . . . . 8
โข (-1 + 1)
= (1 + -1) |
82 | | 1pneg1e0 12328 |
. . . . . . . 8
โข (1 + -1)
= 0 |
83 | 81, 82 | eqtr2i 2753 |
. . . . . . 7
โข 0 = (-1 +
1) |
84 | 78, 83 | breqtrdi 5179 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
< (-1 + 1)) |
85 | | btwnnz 12635 |
. . . . . 6
โข ((-1
โ โค โง -1 < (๐ด / (2 ยท ฯ)) โง (๐ด / (2 ยท ฯ)) < (-1 +
1)) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
86 | 50, 75, 84, 85 | syl3anc 1368 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
ยฌ (๐ด / (2 ยท
ฯ)) โ โค) |
87 | 40, 48, 86 | syl2anc 583 |
. . . 4
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
88 | 39, 87 | pm2.61dan 810 |
. . 3
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
89 | 65 | a1i 11 |
. . . 4
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ โ+) |
90 | | mod0 13838 |
. . . 4
โข ((๐ด โ โ โง (2
ยท ฯ) โ โ+) โ ((๐ด mod (2 ยท ฯ)) = 0 โ (๐ด / (2 ยท ฯ)) โ
โค)) |
91 | 7, 89, 90 | syl2anc 583 |
. . 3
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ((๐ด mod (2
ยท ฯ)) = 0 โ (๐ด / (2 ยท ฯ)) โ
โค)) |
92 | 88, 91 | mtbird 325 |
. 2
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ยฌ (๐ด mod (2
ยท ฯ)) = 0) |
93 | 92 | neqned 2939 |
1
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (๐ด mod (2
ยท ฯ)) โ 0) |