Step | Hyp | Ref
| Expression |
1 | | 2z 12543 |
. . . . 5
โข 2 โ
โค |
2 | | divides 16146 |
. . . . 5
โข ((2
โ โค โง ๐พ
โ โค) โ (2 โฅ ๐พ โ โ๐ โ โค (๐ ยท 2) = ๐พ)) |
3 | 1, 2 | mpan 689 |
. . . 4
โข (๐พ โ โค โ (2
โฅ ๐พ โ
โ๐ โ โค
(๐ ยท 2) = ๐พ)) |
4 | 3 | biimpa 478 |
. . 3
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ โ๐ โ โค (๐ ยท 2) = ๐พ) |
5 | | zcn 12512 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
6 | | 2cnd 12239 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ 2 โ
โ) |
7 | | picn 25839 |
. . . . . . . . . . . . . . 15
โข ฯ
โ โ |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ฯ
โ โ) |
9 | 5, 6, 8 | mulassd 11186 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ((๐ ยท 2) ยท ฯ) =
(๐ ยท (2 ยท
ฯ))) |
10 | 9 | eqcomd 2739 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ ยท (2 ยท ฯ)) =
((๐ ยท 2) ยท
ฯ)) |
11 | 10 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (๐ ยท (2 ยท ฯ)) = ((๐ ยท 2) ยท
ฯ)) |
12 | | oveq1 7368 |
. . . . . . . . . . . 12
โข ((๐ ยท 2) = ๐พ โ ((๐ ยท 2) ยท ฯ) = (๐พ ยท
ฯ)) |
13 | 12 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ ((๐ ยท 2) ยท ฯ) = (๐พ ยท
ฯ)) |
14 | 11, 13 | eqtr2d 2774 |
. . . . . . . . . 10
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (๐พ ยท ฯ) = (๐ ยท (2 ยท
ฯ))) |
15 | 14 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท ฯ)) = (cosโ(๐ ยท (2 ยท
ฯ)))) |
16 | | cos2kpi 25864 |
. . . . . . . . . 10
โข (๐ โ โค โ
(cosโ(๐ ยท (2
ยท ฯ))) = 1) |
17 | 16 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐ ยท (2 ยท ฯ))) =
1) |
18 | 15, 17 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท ฯ)) = 1) |
19 | 18 | 3adant1 1131 |
. . . . . . 7
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท ฯ)) = 1) |
20 | | iftrue 4496 |
. . . . . . . . 9
โข (2
โฅ ๐พ โ if(2
โฅ ๐พ, 1, -1) =
1) |
21 | 20 | eqcomd 2739 |
. . . . . . . 8
โข (2
โฅ ๐พ โ 1 = if(2
โฅ ๐พ, 1,
-1)) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . 7
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ 1 = if(2 โฅ ๐พ, 1, -1)) |
23 | 19, 22 | eqtrd 2773 |
. . . . . 6
โข ((2
โฅ ๐พ โง ๐ โ โค โง (๐ ยท 2) = ๐พ) โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ ๐พ, 1, -1)) |
24 | 23 | 3exp 1120 |
. . . . 5
โข (2
โฅ ๐พ โ (๐ โ โค โ ((๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ ๐พ, 1, -1)))) |
25 | 24 | adantl 483 |
. . . 4
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (๐ โ โค โ ((๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ ๐พ, 1, -1)))) |
26 | 25 | rexlimdv 3147 |
. . 3
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (โ๐ โ โค (๐ ยท 2) = ๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ ๐พ, 1, -1))) |
27 | 4, 26 | mpd 15 |
. 2
โข ((๐พ โ โค โง 2 โฅ
๐พ) โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ
๐พ, 1, -1)) |
28 | | odd2np1 16231 |
. . . 4
โข (๐พ โ โค โ (ยฌ 2
โฅ ๐พ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐พ)) |
29 | 28 | biimpa 478 |
. . 3
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐พ) |
30 | 6, 5 | mulcld 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (2
ยท ๐) โ
โ) |
31 | | 1cnd 11158 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ 1 โ
โ) |
32 | 30, 31, 8 | adddird 11188 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (((2
ยท ๐) + 1) ยท
ฯ) = (((2 ยท ๐)
ยท ฯ) + (1 ยท ฯ))) |
33 | 6, 5 | mulcomd 11184 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ (2
ยท ๐) = (๐ ยท 2)) |
34 | 33 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ ((2
ยท ๐) ยท ฯ)
= ((๐ ยท 2) ยท
ฯ)) |
35 | 34, 9 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ((2
ยท ๐) ยท ฯ)
= (๐ ยท (2 ยท
ฯ))) |
36 | 7 | mulid2i 11168 |
. . . . . . . . . . . . . . 15
โข (1
ยท ฯ) = ฯ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (1
ยท ฯ) = ฯ) |
38 | 35, 37 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (((2
ยท ๐) ยท ฯ)
+ (1 ยท ฯ)) = ((๐
ยท (2 ยท ฯ)) + ฯ)) |
39 | | 2cn 12236 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
40 | 39, 7 | mulcli 11170 |
. . . . . . . . . . . . . . . 16
โข (2
ยท ฯ) โ โ |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (2
ยท ฯ) โ โ) |
42 | 5, 41 | mulcld 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ ยท (2 ยท ฯ))
โ โ) |
43 | 42, 8 | addcomd 11365 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ((๐ ยท (2 ยท ฯ)) +
ฯ) = (ฯ + (๐ ยท
(2 ยท ฯ)))) |
44 | 32, 38, 43 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (ฯ +
(๐ ยท (2 ยท
ฯ))) = (((2 ยท ๐)
+ 1) ยท ฯ)) |
45 | 44 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (ฯ + (๐ ยท (2 ยท ฯ))) =
(((2 ยท ๐) + 1)
ยท ฯ)) |
46 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (((2
ยท ๐) + 1) = ๐พ โ (((2 ยท ๐) + 1) ยท ฯ) = (๐พ ยท
ฯ)) |
47 | 46 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (((2 ยท ๐) + 1) ยท ฯ) = (๐พ ยท
ฯ)) |
48 | 45, 47 | eqtr2d 2774 |
. . . . . . . . . 10
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (๐พ ยท ฯ) = (ฯ + (๐ ยท (2 ยท
ฯ)))) |
49 | 48 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท ฯ)) =
(cosโ(ฯ + (๐
ยท (2 ยท ฯ))))) |
50 | | cosper 25862 |
. . . . . . . . . . 11
โข ((ฯ
โ โ โง ๐
โ โค) โ (cosโ(ฯ + (๐ ยท (2 ยท ฯ)))) =
(cosโฯ)) |
51 | 7, 50 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โค โ
(cosโ(ฯ + (๐
ยท (2 ยท ฯ)))) = (cosโฯ)) |
52 | 51 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(ฯ +
(๐ ยท (2 ยท
ฯ)))) = (cosโฯ)) |
53 | | cospi 25852 |
. . . . . . . . . 10
โข
(cosโฯ) = -1 |
54 | 53 | a1i 11 |
. . . . . . . . 9
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโฯ) =
-1) |
55 | 49, 52, 54 | 3eqtrd 2777 |
. . . . . . . 8
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท ฯ)) =
-1) |
56 | 55 | 3adant1 1131 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐พ โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท ฯ)) =
-1) |
57 | | iffalse 4499 |
. . . . . . . . 9
โข (ยฌ 2
โฅ ๐พ โ if(2
โฅ ๐พ, 1, -1) =
-1) |
58 | 57 | eqcomd 2739 |
. . . . . . . 8
โข (ยฌ 2
โฅ ๐พ โ -1 = if(2
โฅ ๐พ, 1,
-1)) |
59 | 58 | 3ad2ant1 1134 |
. . . . . . 7
โข ((ยฌ 2
โฅ ๐พ โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ -1 = if(2 โฅ ๐พ, 1, -1)) |
60 | 56, 59 | eqtrd 2773 |
. . . . . 6
โข ((ยฌ 2
โฅ ๐พ โง ๐ โ โค โง ((2
ยท ๐) + 1) = ๐พ) โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ
๐พ, 1, -1)) |
61 | 60 | 3exp 1120 |
. . . . 5
โข (ยฌ 2
โฅ ๐พ โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ
๐พ, 1,
-1)))) |
62 | 61 | adantl 483 |
. . . 4
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ (๐ โ โค โ (((2
ยท ๐) + 1) = ๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ
๐พ, 1,
-1)))) |
63 | 62 | rexlimdv 3147 |
. . 3
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
(โ๐ โ โค
((2 ยท ๐) + 1) =
๐พ โ (cosโ(๐พ ยท ฯ)) = if(2 โฅ
๐พ, 1,
-1))) |
64 | 29, 63 | mpd 15 |
. 2
โข ((๐พ โ โค โง ยฌ 2
โฅ ๐พ) โ
(cosโ(๐พ ยท
ฯ)) = if(2 โฅ ๐พ, 1,
-1)) |
65 | 27, 64 | pm2.61dan 812 |
1
โข (๐พ โ โค โ
(cosโ(๐พ ยท
ฯ)) = if(2 โฅ ๐พ, 1,
-1)) |