Step | Hyp | Ref
| Expression |
1 | | 0zd 12566 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 โ โค) |
2 | | pire 25959 |
. . . . . . . . . 10
โข ฯ
โ โ |
3 | 2 | renegcli 11517 |
. . . . . . . . 9
โข -ฯ
โ โ |
4 | | iccssre 13402 |
. . . . . . . . 9
โข ((-ฯ
โ โ โง ฯ โ โ) โ (-ฯ[,]ฯ) โ
โ) |
5 | 3, 2, 4 | mp2an 690 |
. . . . . . . 8
โข
(-ฯ[,]ฯ) โ โ |
6 | | eldifi 4125 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
(-ฯ[,]ฯ)) |
7 | 5, 6 | sselid 3979 |
. . . . . . 7
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
โ) |
8 | 7 | adantr 481 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
๐ด โ
โ) |
9 | | 2re 12282 |
. . . . . . . 8
โข 2 โ
โ |
10 | 9, 2 | remulcli 11226 |
. . . . . . 7
โข (2
ยท ฯ) โ โ |
11 | 10 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(2 ยท ฯ) โ โ) |
12 | | simpr 485 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < ๐ด) |
13 | | 2pos 12311 |
. . . . . . . 8
โข 0 <
2 |
14 | | pipos 25961 |
. . . . . . . 8
โข 0 <
ฯ |
15 | 9, 2, 13, 14 | mulgt0ii 11343 |
. . . . . . 7
โข 0 < (2
ยท ฯ) |
16 | 15 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < (2 ยท ฯ)) |
17 | 8, 11, 12, 16 | divgt0d 12145 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
0 < (๐ด / (2 ยท
ฯ))) |
18 | 11, 16 | elrpd 13009 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(2 ยท ฯ) โ โ+) |
19 | 2 | a1i 11 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ โ โ) |
20 | 10 | a1i 11 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ โ) |
21 | 3 | rexri 11268 |
. . . . . . . . . . . 12
โข -ฯ
โ โ* |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -ฯ โ โ*) |
23 | 19 | rexrd 11260 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ โ โ*) |
24 | | iccleub 13375 |
. . . . . . . . . . 11
โข ((-ฯ
โ โ* โง ฯ โ โ* โง ๐ด โ (-ฯ[,]ฯ)) โ
๐ด โค
ฯ) |
25 | 22, 23, 6, 24 | syl3anc 1371 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โค
ฯ) |
26 | | pirp 25962 |
. . . . . . . . . . 11
โข ฯ
โ โ+ |
27 | | 2timesgt 43984 |
. . . . . . . . . . 11
โข (ฯ
โ โ+ โ ฯ < (2 ยท ฯ)) |
28 | 26, 27 | mp1i 13 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ฯ < (2 ยท ฯ)) |
29 | 7, 19, 20, 25, 28 | lelttrd 11368 |
. . . . . . . . 9
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด < (2
ยท ฯ)) |
30 | 29 | adantr 481 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
๐ด < (2 ยท
ฯ)) |
31 | 8, 11, 18, 30 | ltdiv1dd 13069 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< ((2 ยท ฯ) / (2 ยท ฯ))) |
32 | 10 | recni 11224 |
. . . . . . . 8
โข (2
ยท ฯ) โ โ |
33 | 10, 15 | gt0ne0ii 11746 |
. . . . . . . 8
โข (2
ยท ฯ) โ 0 |
34 | 32, 33 | dividi 11943 |
. . . . . . 7
โข ((2
ยท ฯ) / (2 ยท ฯ)) = 1 |
35 | 31, 34 | breqtrdi 5188 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< 1) |
36 | | 0p1e1 12330 |
. . . . . 6
โข (0 + 1) =
1 |
37 | 35, 36 | breqtrrdi 5189 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
(๐ด / (2 ยท ฯ))
< (0 + 1)) |
38 | | btwnnz 12634 |
. . . . 5
โข ((0
โ โค โง 0 < (๐ด / (2 ยท ฯ)) โง (๐ด / (2 ยท ฯ)) < (0 +
1)) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
39 | 1, 17, 37, 38 | syl3anc 1371 |
. . . 4
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง 0 < ๐ด) โ
ยฌ (๐ด / (2 ยท
ฯ)) โ โค) |
40 | | simpl 483 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โ
((-ฯ[,]ฯ) โ {0})) |
41 | 7 | adantr 481 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โ
โ) |
42 | | 0red 11213 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ 0 โ โ) |
43 | | simpr 485 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ยฌ 0 < ๐ด) |
44 | 41, 42, 43 | nltled 11360 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด โค
0) |
45 | | eldifsni 4792 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
0) |
46 | 45 | necomd 2996 |
. . . . . . 7
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ 0 โ ๐ด) |
47 | 46 | adantr 481 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ 0 โ ๐ด) |
48 | 41, 42, 44, 47 | leneltd 11364 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ๐ด <
0) |
49 | | neg1z 12594 |
. . . . . . 7
โข -1 โ
โค |
50 | 49 | a1i 11 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-1 โ โค) |
51 | 33 | a1i 11 |
. . . . . . . . 9
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ 0) |
52 | 7, 20, 51 | redivcld 12038 |
. . . . . . . 8
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (๐ด / (2
ยท ฯ)) โ โ) |
53 | 52 | adantr 481 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
โ โ) |
54 | | 1red 11211 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
1 โ โ) |
55 | 7 | recnd 11238 |
. . . . . . . . . 10
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ๐ด โ
โ) |
56 | 55 | adantr 481 |
. . . . . . . . 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 11999 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-(๐ด / (2 ยท ฯ)) =
(-๐ด / (2 ยท
ฯ))) |
60 | 7 | renegcld 11637 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด โ
โ) |
61 | 60 | adantr 481 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-๐ด โ
โ) |
62 | 10 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ โ) |
63 | | 2rp 12975 |
. . . . . . . . . . . 12
โข 2 โ
โ+ |
64 | | rpmulcl 12993 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง ฯ โ โ+) โ (2
ยท ฯ) โ โ+) |
65 | 63, 26, 64 | mp2an 690 |
. . . . . . . . . . 11
โข (2
ยท ฯ) โ โ+ |
66 | 65 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(2 ยท ฯ) โ โ+) |
67 | | iccgelb 13376 |
. . . . . . . . . . . . . 14
โข ((-ฯ
โ โ* โง ฯ โ โ* โง ๐ด โ (-ฯ[,]ฯ)) โ
-ฯ โค ๐ด) |
68 | 22, 23, 6, 67 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -ฯ โค ๐ด) |
69 | 19, 7, 68 | lenegcon1d 11792 |
. . . . . . . . . . . 12
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด โค
ฯ) |
70 | 60, 19, 20, 69, 28 | lelttrd 11368 |
. . . . . . . . . . 11
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ -๐ด < (2
ยท ฯ)) |
71 | 70 | adantr 481 |
. . . . . . . . . 10
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-๐ด < (2 ยท
ฯ)) |
72 | 61, 62, 66, 71 | ltdiv1dd 13069 |
. . . . . . . . 9
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(-๐ด / (2 ยท ฯ))
< ((2 ยท ฯ) / (2 ยท ฯ))) |
73 | 72, 34 | breqtrdi 5188 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(-๐ด / (2 ยท ฯ))
< 1) |
74 | 59, 73 | eqbrtrd 5169 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-(๐ด / (2 ยท ฯ))
< 1) |
75 | 53, 54, 74 | ltnegcon1d 11790 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
-1 < (๐ด / (2 ยท
ฯ))) |
76 | 7 | adantr 481 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
๐ด โ
โ) |
77 | | simpr 485 |
. . . . . . . 8
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
๐ด < 0) |
78 | 76, 66, 77 | divlt0gt0d 43982 |
. . . . . . 7
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
< 0) |
79 | | neg1cn 12322 |
. . . . . . . . 9
โข -1 โ
โ |
80 | | ax-1cn 11164 |
. . . . . . . . 9
โข 1 โ
โ |
81 | 79, 80 | addcomi 11401 |
. . . . . . . 8
โข (-1 + 1)
= (1 + -1) |
82 | | 1pneg1e0 12327 |
. . . . . . . 8
โข (1 + -1)
= 0 |
83 | 81, 82 | eqtr2i 2761 |
. . . . . . 7
โข 0 = (-1 +
1) |
84 | 78, 83 | breqtrdi 5188 |
. . . . . 6
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
(๐ด / (2 ยท ฯ))
< (-1 + 1)) |
85 | | btwnnz 12634 |
. . . . . 6
โข ((-1
โ โค โง -1 < (๐ด / (2 ยท ฯ)) โง (๐ด / (2 ยท ฯ)) < (-1 +
1)) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
86 | 50, 75, 84, 85 | syl3anc 1371 |
. . . . 5
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ๐ด < 0) โ
ยฌ (๐ด / (2 ยท
ฯ)) โ โค) |
87 | 40, 48, 86 | syl2anc 584 |
. . . 4
โข ((๐ด โ ((-ฯ[,]ฯ) โ
{0}) โง ยฌ 0 < ๐ด)
โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
88 | 39, 87 | pm2.61dan 811 |
. . 3
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ยฌ (๐ด / (2
ยท ฯ)) โ โค) |
89 | 65 | a1i 11 |
. . . 4
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (2 ยท ฯ) โ โ+) |
90 | | mod0 13837 |
. . . 4
โข ((๐ด โ โ โง (2
ยท ฯ) โ โ+) โ ((๐ด mod (2 ยท ฯ)) = 0 โ (๐ด / (2 ยท ฯ)) โ
โค)) |
91 | 7, 89, 90 | syl2anc 584 |
. . 3
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ((๐ด mod (2
ยท ฯ)) = 0 โ (๐ด / (2 ยท ฯ)) โ
โค)) |
92 | 88, 91 | mtbird 324 |
. 2
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ ยฌ (๐ด mod (2
ยท ฯ)) = 0) |
93 | 92 | neqned 2947 |
1
โข (๐ด โ ((-ฯ[,]ฯ) โ
{0}) โ (๐ด mod (2
ยท ฯ)) โ 0) |