Step | Hyp | Ref
| Expression |
1 | | 0re 7957 |
. . . . 5
โข 0 โ
โ |
2 | 1 | ltnri 8050 |
. . . 4
โข ยฌ 0
< 0 |
3 | | elioore 9912 |
. . . . . . 7
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ ๐ด โ โ) |
4 | 3 | adantr 276 |
. . . . . 6
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ ๐ด โ โ) |
5 | | halfpire 14216 |
. . . . . 6
โข (ฯ /
2) โ โ |
6 | | reaplt 8545 |
. . . . . 6
โข ((๐ด โ โ โง (ฯ / 2)
โ โ) โ (๐ด #
(ฯ / 2) โ (๐ด <
(ฯ / 2) โจ (ฯ / 2) < ๐ด))) |
7 | 4, 5, 6 | sylancl 413 |
. . . . 5
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ (๐ด # (ฯ / 2) โ (๐ด < (ฯ / 2) โจ (ฯ / 2) < ๐ด))) |
8 | 3 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ ๐ด โ โ) |
9 | | neghalfpirx 14218 |
. . . . . . . . . . . . . 14
โข -(ฯ /
2) โ โ* |
10 | | 3re 8993 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
11 | 10, 5 | remulcli 7971 |
. . . . . . . . . . . . . . 15
โข (3
ยท (ฯ / 2)) โ โ |
12 | 11 | rexri 8015 |
. . . . . . . . . . . . . 14
โข (3
ยท (ฯ / 2)) โ โ* |
13 | | elioo2 9921 |
. . . . . . . . . . . . . 14
โข ((-(ฯ
/ 2) โ โ* โง (3 ยท (ฯ / 2)) โ
โ*) โ (๐ด โ (-(ฯ / 2)(,)(3 ยท (ฯ /
2))) โ (๐ด โ
โ โง -(ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2))))) |
14 | 9, 12, 13 | mp2an 426 |
. . . . . . . . . . . . 13
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (๐ด โ โ โง -(ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2)))) |
15 | 14 | simp2bi 1013 |
. . . . . . . . . . . 12
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ -(ฯ / 2) < ๐ด) |
16 | 15 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ -(ฯ / 2) <
๐ด) |
17 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ ๐ด < (ฯ / 2)) |
18 | 9 | a1i 9 |
. . . . . . . . . . . 12
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ -(ฯ / 2) โ
โ*) |
19 | 5 | rexri 8015 |
. . . . . . . . . . . 12
โข (ฯ /
2) โ โ* |
20 | | elioo2 9921 |
. . . . . . . . . . . 12
โข ((-(ฯ
/ 2) โ โ* โง (ฯ / 2) โ โ*)
โ (๐ด โ (-(ฯ /
2)(,)(ฯ / 2)) โ (๐ด
โ โ โง -(ฯ / 2) < ๐ด โง ๐ด < (ฯ / 2)))) |
21 | 18, 19, 20 | sylancl 413 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ (๐ด โ (-(ฯ / 2)(,)(ฯ / 2)) โ
(๐ด โ โ โง
-(ฯ / 2) < ๐ด โง
๐ด < (ฯ /
2)))) |
22 | 8, 16, 17, 21 | mpbir3and 1180 |
. . . . . . . . . 10
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ ๐ด โ (-(ฯ / 2)(,)(ฯ /
2))) |
23 | | cosq14gt0 14256 |
. . . . . . . . . 10
โข (๐ด โ (-(ฯ / 2)(,)(ฯ /
2)) โ 0 < (cosโ๐ด)) |
24 | 22, 23 | syl 14 |
. . . . . . . . 9
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด < (ฯ / 2)) โ 0 <
(cosโ๐ด)) |
25 | 24 | adantlr 477 |
. . . . . . . 8
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง ๐ด < (ฯ / 2)) โ 0 <
(cosโ๐ด)) |
26 | | simplr 528 |
. . . . . . . 8
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง ๐ด < (ฯ / 2)) โ (cosโ๐ด) = 0) |
27 | 25, 26 | breqtrd 4030 |
. . . . . . 7
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง ๐ด < (ฯ / 2)) โ 0 <
0) |
28 | 27 | ex 115 |
. . . . . 6
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ (๐ด < (ฯ / 2) โ 0 <
0)) |
29 | | simplr 528 |
. . . . . . . 8
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง (ฯ / 2) < ๐ด) โ (cosโ๐ด) = 0) |
30 | 3 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (ฯ / 2) < ๐ด) โ ๐ด โ โ) |
31 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (ฯ / 2) < ๐ด) โ (ฯ / 2) < ๐ด) |
32 | 14 | simp3bi 1014 |
. . . . . . . . . . . 12
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ ๐ด < (3 ยท (ฯ /
2))) |
33 | 32 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (ฯ / 2) < ๐ด) โ ๐ด < (3 ยท (ฯ /
2))) |
34 | | elioo2 9921 |
. . . . . . . . . . . 12
โข (((ฯ /
2) โ โ* โง (3 ยท (ฯ / 2)) โ
โ*) โ (๐ด โ ((ฯ / 2)(,)(3 ยท (ฯ /
2))) โ (๐ด โ
โ โง (ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2))))) |
35 | 19, 12, 34 | mp2an 426 |
. . . . . . . . . . 11
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (๐ด โ โ โง (ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2)))) |
36 | 30, 31, 33, 35 | syl3anbrc 1181 |
. . . . . . . . . 10
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (ฯ / 2) < ๐ด) โ ๐ด โ ((ฯ / 2)(,)(3 ยท (ฯ /
2)))) |
37 | | cosq23lt0 14257 |
. . . . . . . . . 10
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (cosโ๐ด) < 0) |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (ฯ / 2) < ๐ด) โ (cosโ๐ด) < 0) |
39 | 38 | adantlr 477 |
. . . . . . . 8
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง (ฯ / 2) < ๐ด) โ (cosโ๐ด) < 0) |
40 | 29, 39 | eqbrtrrd 4028 |
. . . . . . 7
โข (((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โง (ฯ / 2) < ๐ด) โ 0 <
0) |
41 | 40 | ex 115 |
. . . . . 6
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ ((ฯ / 2) < ๐ด โ 0 <
0)) |
42 | 28, 41 | jaod 717 |
. . . . 5
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ ((๐ด < (ฯ / 2) โจ (ฯ / 2) < ๐ด) โ 0 <
0)) |
43 | 7, 42 | sylbid 150 |
. . . 4
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ (๐ด # (ฯ / 2) โ 0 <
0)) |
44 | 2, 43 | mtoi 664 |
. . 3
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ ยฌ ๐ด # (ฯ / 2)) |
45 | 3 | recnd 7986 |
. . . 4
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ ๐ด โ โ) |
46 | | picn 14211 |
. . . . 5
โข ฯ
โ โ |
47 | | halfcl 9145 |
. . . . 5
โข (ฯ
โ โ โ (ฯ / 2) โ โ) |
48 | 46, 47 | mp1i 10 |
. . . 4
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ (ฯ / 2) โ
โ) |
49 | | apti 8579 |
. . . 4
โข ((๐ด โ โ โง (ฯ / 2)
โ โ) โ (๐ด =
(ฯ / 2) โ ยฌ ๐ด #
(ฯ / 2))) |
50 | 45, 48, 49 | syl2an2r 595 |
. . 3
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ (๐ด = (ฯ / 2) โ ยฌ ๐ด # (ฯ / 2))) |
51 | 44, 50 | mpbird 167 |
. 2
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง (cosโ๐ด) = 0) โ ๐ด = (ฯ / 2)) |
52 | | fveq2 5516 |
. . . 4
โข (๐ด = (ฯ / 2) โ
(cosโ๐ด) =
(cosโ(ฯ / 2))) |
53 | | coshalfpi 14221 |
. . . 4
โข
(cosโ(ฯ / 2)) = 0 |
54 | 52, 53 | eqtrdi 2226 |
. . 3
โข (๐ด = (ฯ / 2) โ
(cosโ๐ด) =
0) |
55 | 54 | adantl 277 |
. 2
โข ((๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โง ๐ด = (ฯ / 2)) โ (cosโ๐ด) = 0) |
56 | 51, 55 | impbida 596 |
1
โข (๐ด โ (-(ฯ / 2)(,)(3
ยท (ฯ / 2))) โ ((cosโ๐ด) = 0 โ ๐ด = (ฯ / 2))) |