Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ 2 โฅ ๐พ) |
2 | | 2z 12543 |
. . . . 5
โข 2 โ
โค |
3 | | simpl 484 |
. . . . 5
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ ๐พ โ โค) |
4 | | divides 16146 |
. . . . 5
โข ((2
โ โค โง ๐พ
โ โค) โ (2 โฅ ๐พ โ โ๐ โ โค (๐ ยท 2) = ๐พ)) |
5 | 2, 3, 4 | sylancr 588 |
. . . 4
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (2 โฅ ๐พ โ โ๐ โ โค (๐ ยท 2) = ๐พ)) |
6 | 1, 5 | mpbid 231 |
. . 3
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ โ๐ โ โค (๐ ยท 2) = ๐พ) |
7 | | zcn 12512 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
8 | | negcl 11409 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ -๐ โ
โ) |
9 | | 2cn 12236 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
10 | | picn 25839 |
. . . . . . . . . . . . . . . . 17
โข ฯ
โ โ |
11 | 9, 10 | mulcli 11170 |
. . . . . . . . . . . . . . . 16
โข (2
ยท ฯ) โ โ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท ฯ) โ โ) |
13 | 8, 12 | mulcld 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (-๐ ยท (2 ยท ฯ))
โ โ) |
14 | 13 | addid2d 11364 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0 +
(-๐ ยท (2 ยท
ฯ))) = (-๐ ยท (2
ยท ฯ))) |
15 | | 2cnd 12239 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 2 โ
โ) |
16 | 10 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ฯ
โ โ) |
17 | 8, 15, 16 | mulassd 11186 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((-๐ ยท 2) ยท ฯ) =
(-๐ ยท (2 ยท
ฯ))) |
18 | 17 | eqcomd 2739 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (-๐ ยท (2 ยท ฯ)) =
((-๐ ยท 2) ยท
ฯ)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
20 | 19, 15 | mulneg1d 11616 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (-๐ ยท 2) = -(๐ ยท 2)) |
21 | 20 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((-๐ ยท 2) ยท ฯ) =
(-(๐ ยท 2) ยท
ฯ)) |
22 | 14, 18, 21 | 3eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (0 +
(-๐ ยท (2 ยท
ฯ))) = (-(๐ ยท 2)
ยท ฯ)) |
23 | 7, 22 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ (0 +
(-๐ ยท (2 ยท
ฯ))) = (-(๐ ยท 2)
ยท ฯ)) |
24 | 23 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (0 + (-๐ ยท (2 ยท ฯ))) = (-(๐ ยท 2) ยท
ฯ)) |
25 | 19, 15 | mulcld 11183 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ ยท 2) โ
โ) |
26 | | mulneg12 11601 |
. . . . . . . . . . . . 13
โข (((๐ ยท 2) โ โ
โง ฯ โ โ) โ (-(๐ ยท 2) ยท ฯ) = ((๐ ยท 2) ยท
-ฯ)) |
27 | 25, 16, 26 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (-(๐ ยท 2) ยท ฯ) =
((๐ ยท 2) ยท
-ฯ)) |
28 | 7, 27 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โค โ (-(๐ ยท 2) ยท ฯ) =
((๐ ยท 2) ยท
-ฯ)) |
29 | 28 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (-(๐ ยท 2) ยท ฯ) = ((๐ ยท 2) ยท
-ฯ)) |
30 | | oveq1 7368 |
. . . . . . . . . . 11
โข ((๐ ยท 2) = ๐พ โ ((๐ ยท 2) ยท -ฯ) = (๐พ ยท
-ฯ)) |
31 | 30 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ ((๐ ยท 2) ยท -ฯ) = (๐พ ยท
-ฯ)) |
32 | 24, 29, 31 | 3eqtrrd 2778 |
. . . . . . . . 9
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (๐พ ยท -ฯ) = (0 + (-๐ ยท (2 ยท
ฯ)))) |
33 | 32 | fveq2d 6850 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) = (cosโ(0 + (-๐ ยท (2 ยท
ฯ))))) |
34 | 33 | 3adant1 1131 |
. . . . . . 7
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) = (cosโ(0 + (-๐ ยท (2 ยท
ฯ))))) |
35 | | 0cnd 11156 |
. . . . . . . . 9
โข (๐ โ โค โ 0 โ
โ) |
36 | | znegcl 12546 |
. . . . . . . . 9
โข (๐ โ โค โ -๐ โ
โค) |
37 | | cosper 25862 |
. . . . . . . . 9
โข ((0
โ โ โง -๐
โ โค) โ (cosโ(0 + (-๐ ยท (2 ยท ฯ)))) =
(cosโ0)) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . . 8
โข (๐ โ โค โ
(cosโ(0 + (-๐
ยท (2 ยท ฯ)))) = (cosโ0)) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . 7
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(0 + (-๐ ยท (2 ยท ฯ)))) =
(cosโ0)) |
40 | | cos0 16040 |
. . . . . . . . 9
โข
(cosโ0) = 1 |
41 | | iftrue 4496 |
. . . . . . . . 9
โข (2
โฅ ๐พ โ if(2
โฅ ๐พ, 1, -1) =
1) |
42 | 40, 41 | eqtr4id 2792 |
. . . . . . . 8
โข (2
โฅ ๐พ โ
(cosโ0) = if(2 โฅ ๐พ, 1, -1)) |
43 | 42 | 3ad2ant1 1134 |
. . . . . . 7
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ0) = if(2 โฅ ๐พ, 1, -1)) |
44 | 34, 39, 43 | 3eqtrd 2777 |
. . . . . 6
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ ๐พ, 1, -1)) |
45 | 44 | 3exp 1120 |
. . . . 5
โข (2
โฅ ๐พ โ (๐ โ โค โ ((๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ ๐พ, 1, -1)))) |
46 | 45 | adantl 483 |
. . . 4
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (๐ โ โค โ ((๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ ๐พ, 1, -1)))) |
47 | 46 | rexlimdv 3147 |
. . 3
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (โ๐ โ โค (๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ ๐พ, 1, -1))) |
48 | 6, 47 | mpd 15 |
. 2
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ
๐พ, 1, -1)) |
49 | | odd2np1 16231 |
. . . 4
โข (๐พ โ โค โ (ยฌ 2
โฅ ๐พ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐พ)) |
50 | 49 | biimpa 478 |
. . 3
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐พ) |
51 | | oveq1 7368 |
. . . . . . . . . . 11
โข (((2
ยท ๐) + 1) = ๐พ โ (((2 ยท ๐) + 1) ยท -ฯ) = (๐พ ยท
-ฯ)) |
52 | 51 | eqcomd 2739 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) = ๐พ โ (๐พ ยท -ฯ) = (((2 ยท ๐) + 1) ยท
-ฯ)) |
53 | 52 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (๐พ ยท -ฯ) = (((2 ยท ๐) + 1) ยท
-ฯ)) |
54 | 15, 19 | mulcld 11183 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
55 | | 1cnd 11158 |
. . . . . . . . . . . 12
โข (๐ โ โ โ 1 โ
โ) |
56 | | negpicn 25842 |
. . . . . . . . . . . . 13
โข -ฯ
โ โ |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ -ฯ
โ โ) |
58 | 54, 55, 57 | adddird 11188 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((2
ยท ๐) + 1) ยท
-ฯ) = (((2 ยท ๐)
ยท -ฯ) + (1 ยท -ฯ))) |
59 | 7, 58 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โค โ (((2
ยท ๐) + 1) ยท
-ฯ) = (((2 ยท ๐)
ยท -ฯ) + (1 ยท -ฯ))) |
60 | 59 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (((2 ยท ๐) + 1) ยท -ฯ) = (((2
ยท ๐) ยท -ฯ)
+ (1 ยท -ฯ))) |
61 | | mulneg12 11601 |
. . . . . . . . . . . . . . . 16
โข (((2
ยท ๐) โ โ
โง ฯ โ โ) โ (-(2 ยท ๐) ยท ฯ) = ((2 ยท ๐) ยท
-ฯ)) |
62 | 54, 16, 61 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (-(2
ยท ๐) ยท ฯ)
= ((2 ยท ๐) ยท
-ฯ)) |
63 | 62 | eqcomd 2739 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท ๐) ยท -ฯ)
= (-(2 ยท ๐) ยท
ฯ)) |
64 | 15, 19 | mulneg2d 11617 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท -๐) = -(2 ยท
๐)) |
65 | 15, 8 | mulcomd 11184 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท -๐) = (-๐ ยท 2)) |
66 | 64, 65 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ -(2
ยท ๐) = (-๐ ยท 2)) |
67 | 66 | oveq1d 7376 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (-(2
ยท ๐) ยท ฯ)
= ((-๐ ยท 2) ยท
ฯ)) |
68 | 63, 67, 17 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท ๐) ยท -ฯ)
= (-๐ ยท (2 ยท
ฯ))) |
69 | 57 | mulid2d 11181 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1
ยท -ฯ) = -ฯ) |
70 | 68, 69 | oveq12d 7379 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((2
ยท ๐) ยท -ฯ)
+ (1 ยท -ฯ)) = ((-๐ ยท (2 ยท ฯ)) +
-ฯ)) |
71 | 13, 57 | addcomd 11365 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((-๐ ยท (2 ยท ฯ)) +
-ฯ) = (-ฯ + (-๐
ยท (2 ยท ฯ)))) |
72 | 70, 71 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((2
ยท ๐) ยท -ฯ)
+ (1 ยท -ฯ)) = (-ฯ + (-๐ ยท (2 ยท
ฯ)))) |
73 | 7, 72 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โค โ (((2
ยท ๐) ยท -ฯ)
+ (1 ยท -ฯ)) = (-ฯ + (-๐ ยท (2 ยท
ฯ)))) |
74 | 73 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (((2 ยท ๐) ยท -ฯ) + (1 ยท
-ฯ)) = (-ฯ + (-๐
ยท (2 ยท ฯ)))) |
75 | 53, 60, 74 | 3eqtrd 2777 |
. . . . . . . 8
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (๐พ ยท -ฯ) = (-ฯ + (-๐ ยท (2 ยท
ฯ)))) |
76 | 75 | 3adant1 1131 |
. . . . . . 7
โข ((๐พ โ โค โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (๐พ ยท -ฯ) = (-ฯ + (-๐ ยท (2 ยท
ฯ)))) |
77 | 76 | fveq2d 6850 |
. . . . . 6
โข ((๐พ โ โค โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) =
(cosโ(-ฯ + (-๐
ยท (2 ยท ฯ))))) |
78 | 77 | 3adant1r 1178 |
. . . . 5
โข (((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) =
(cosโ(-ฯ + (-๐
ยท (2 ยท ฯ))))) |
79 | | cosper 25862 |
. . . . . . 7
โข ((-ฯ
โ โ โง -๐
โ โค) โ (cosโ(-ฯ + (-๐ ยท (2 ยท ฯ)))) =
(cosโ-ฯ)) |
80 | 56, 36, 79 | sylancr 588 |
. . . . . 6
โข (๐ โ โค โ
(cosโ(-ฯ + (-๐
ยท (2 ยท ฯ)))) = (cosโ-ฯ)) |
81 | 80 | 3ad2ant2 1135 |
. . . . 5
โข (((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(-ฯ +
(-๐ ยท (2 ยท
ฯ)))) = (cosโ-ฯ)) |
82 | | cosnegpi 44198 |
. . . . . . . 8
โข
(cosโ-ฯ) = -1 |
83 | | iffalse 4499 |
. . . . . . . 8
โข (ยฌ 2
โฅ ๐พ โ if(2
โฅ ๐พ, 1, -1) =
-1) |
84 | 82, 83 | eqtr4id 2792 |
. . . . . . 7
โข (ยฌ 2
โฅ ๐พ โ
(cosโ-ฯ) = if(2 โฅ ๐พ, 1, -1)) |
85 | 84 | adantl 483 |
. . . . . 6
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
(cosโ-ฯ) = if(2 โฅ ๐พ, 1, -1)) |
86 | 85 | 3ad2ant1 1134 |
. . . . 5
โข (((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ-ฯ) =
if(2 โฅ ๐พ, 1,
-1)) |
87 | 78, 81, 86 | 3eqtrd 2777 |
. . . 4
โข (((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ
๐พ, 1, -1)) |
88 | 87 | rexlimdv3a 3153 |
. . 3
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐พ โ (cosโ(๐พ ยท -ฯ)) = if(2 โฅ
๐พ, 1,
-1))) |
89 | 50, 88 | mpd 15 |
. 2
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
(cosโ(๐พ ยท
-ฯ)) = if(2 โฅ ๐พ,
1, -1)) |
90 | 48, 89 | pm2.61dan 812 |
1
โข (๐พ โ โค โ
(cosโ(๐พ ยท
-ฯ)) = if(2 โฅ ๐พ,
1, -1)) |