Step | Hyp | Ref
| Expression |
1 | | elioore 9911 |
. . . . . . 7
โข (๐ด โ (0(,)(2 ยท ฯ))
โ ๐ด โ
โ) |
2 | 1 | adantr 276 |
. . . . . 6
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โ ๐ด โ
โ) |
3 | 2 | adantr 276 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
๐ด โ
โ) |
4 | | pire 14177 |
. . . . . . 7
โข ฯ
โ โ |
5 | 4 | a1i 9 |
. . . . . 6
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
ฯ โ โ) |
6 | | simpr 110 |
. . . . . 6
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
ฯ < ๐ด) |
7 | 5, 3, 6 | ltled 8075 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
ฯ โค ๐ด) |
8 | | 0xr 8003 |
. . . . . . . 8
โข 0 โ
โ* |
9 | | 2re 8988 |
. . . . . . . . . 10
โข 2 โ
โ |
10 | 9, 4 | remulcli 7970 |
. . . . . . . . 9
โข (2
ยท ฯ) โ โ |
11 | 10 | rexri 8014 |
. . . . . . . 8
โข (2
ยท ฯ) โ โ* |
12 | | elioo2 9920 |
. . . . . . . 8
โข ((0
โ โ* โง (2 ยท ฯ) โ โ*)
โ (๐ด โ (0(,)(2
ยท ฯ)) โ (๐ด
โ โ โง 0 < ๐ด โง ๐ด < (2 ยท ฯ)))) |
13 | 8, 11, 12 | mp2an 426 |
. . . . . . 7
โข (๐ด โ (0(,)(2 ยท ฯ))
โ (๐ด โ โ
โง 0 < ๐ด โง ๐ด < (2 ยท
ฯ))) |
14 | 13 | simp3bi 1014 |
. . . . . 6
โข (๐ด โ (0(,)(2 ยท ฯ))
โ ๐ด < (2 ยท
ฯ)) |
15 | 14 | ad2antrr 488 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
๐ด < (2 ยท
ฯ)) |
16 | | elico2 9936 |
. . . . . 6
โข ((ฯ
โ โ โง (2 ยท ฯ) โ โ*) โ
(๐ด โ (ฯ[,)(2
ยท ฯ)) โ (๐ด
โ โ โง ฯ โค ๐ด โง ๐ด < (2 ยท ฯ)))) |
17 | 4, 11, 16 | mp2an 426 |
. . . . 5
โข (๐ด โ (ฯ[,)(2 ยท
ฯ)) โ (๐ด โ
โ โง ฯ โค ๐ด
โง ๐ด < (2 ยท
ฯ))) |
18 | 3, 7, 15, 17 | syl3anbrc 1181 |
. . . 4
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
๐ด โ (ฯ[,)(2
ยท ฯ))) |
19 | | cosq34lt1 14241 |
. . . 4
โข (๐ด โ (ฯ[,)(2 ยท
ฯ)) โ (cosโ๐ด)
< 1) |
20 | 18, 19 | syl 14 |
. . 3
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ฯ < ๐ด) โ
(cosโ๐ด) <
1) |
21 | 2 | adantr 276 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ๐ด < (3 ยท
(ฯ / 2))) โ ๐ด
โ โ) |
22 | | simplr 528 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ๐ด < (3 ยท
(ฯ / 2))) โ (ฯ / 2) < ๐ด) |
23 | | simpr 110 |
. . . . 5
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ๐ด < (3 ยท
(ฯ / 2))) โ ๐ด <
(3 ยท (ฯ / 2))) |
24 | | halfpire 14183 |
. . . . . . 7
โข (ฯ /
2) โ โ |
25 | 24 | rexri 8014 |
. . . . . 6
โข (ฯ /
2) โ โ* |
26 | | 3re 8992 |
. . . . . . . 8
โข 3 โ
โ |
27 | 26, 24 | remulcli 7970 |
. . . . . . 7
โข (3
ยท (ฯ / 2)) โ โ |
28 | 27 | rexri 8014 |
. . . . . 6
โข (3
ยท (ฯ / 2)) โ โ* |
29 | | elioo2 9920 |
. . . . . 6
โข (((ฯ /
2) โ โ* โง (3 ยท (ฯ / 2)) โ
โ*) โ (๐ด โ ((ฯ / 2)(,)(3 ยท (ฯ /
2))) โ (๐ด โ
โ โง (ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2))))) |
30 | 25, 28, 29 | mp2an 426 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (๐ด โ โ โง (ฯ / 2) < ๐ด โง ๐ด < (3 ยท (ฯ /
2)))) |
31 | 21, 22, 23, 30 | syl3anbrc 1181 |
. . . 4
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ๐ด < (3 ยท
(ฯ / 2))) โ ๐ด
โ ((ฯ / 2)(,)(3 ยท (ฯ / 2)))) |
32 | | elioore 9911 |
. . . . . 6
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ ๐ด โ โ) |
33 | 32 | recoscld 11731 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (cosโ๐ด) โ โ) |
34 | | 0red 7957 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ 0 โ โ) |
35 | | 1red 7971 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ 1 โ โ) |
36 | | cosq23lt0 14224 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (cosโ๐ด) < 0) |
37 | | 0lt1 8083 |
. . . . . 6
โข 0 <
1 |
38 | 37 | a1i 9 |
. . . . 5
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ 0 < 1) |
39 | 33, 34, 35, 36, 38 | lttrd 8082 |
. . . 4
โข (๐ด โ ((ฯ / 2)(,)(3
ยท (ฯ / 2))) โ (cosโ๐ด) < 1) |
40 | 31, 39 | syl 14 |
. . 3
โข (((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โง ๐ด < (3 ยท
(ฯ / 2))) โ (cosโ๐ด) < 1) |
41 | | 2lt3 9088 |
. . . . . 6
โข 2 <
3 |
42 | | 2pos 9009 |
. . . . . . . 8
โข 0 <
2 |
43 | 9, 42 | pm3.2i 272 |
. . . . . . 7
โข (2 โ
โ โง 0 < 2) |
44 | | 3pos 9012 |
. . . . . . . 8
โข 0 <
3 |
45 | 26, 44 | pm3.2i 272 |
. . . . . . 7
โข (3 โ
โ โง 0 < 3) |
46 | | pipos 14179 |
. . . . . . . 8
โข 0 <
ฯ |
47 | 4, 46 | pm3.2i 272 |
. . . . . . 7
โข (ฯ
โ โ โง 0 < ฯ) |
48 | | ltdiv2 8843 |
. . . . . . 7
โข (((2
โ โ โง 0 < 2) โง (3 โ โ โง 0 < 3) โง
(ฯ โ โ โง 0 < ฯ)) โ (2 < 3 โ (ฯ / 3)
< (ฯ / 2))) |
49 | 43, 45, 47, 48 | mp3an 1337 |
. . . . . 6
โข (2 < 3
โ (ฯ / 3) < (ฯ / 2)) |
50 | 41, 49 | mpbi 145 |
. . . . 5
โข (ฯ /
3) < (ฯ / 2) |
51 | | ltdivmul 8832 |
. . . . . 6
โข ((ฯ
โ โ โง (ฯ / 2) โ โ โง (3 โ โ โง 0
< 3)) โ ((ฯ / 3) < (ฯ / 2) โ ฯ < (3 ยท (ฯ
/ 2)))) |
52 | 4, 24, 45, 51 | mp3an 1337 |
. . . . 5
โข ((ฯ /
3) < (ฯ / 2) โ ฯ < (3 ยท (ฯ / 2))) |
53 | 50, 52 | mpbi 145 |
. . . 4
โข ฯ <
(3 ยท (ฯ / 2)) |
54 | | axltwlin 8024 |
. . . . 5
โข ((ฯ
โ โ โง (3 ยท (ฯ / 2)) โ โ โง ๐ด โ โ) โ (ฯ
< (3 ยท (ฯ / 2)) โ (ฯ < ๐ด โจ ๐ด < (3 ยท (ฯ /
2))))) |
55 | 4, 27, 2, 54 | mp3an12i 1341 |
. . . 4
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โ (ฯ < (3 ยท (ฯ / 2)) โ (ฯ < ๐ด โจ ๐ด < (3 ยท (ฯ /
2))))) |
56 | 53, 55 | mpi 15 |
. . 3
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โ (ฯ < ๐ด โจ
๐ด < (3 ยท (ฯ /
2)))) |
57 | 20, 40, 56 | mpjaodan 798 |
. 2
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง (ฯ / 2) < ๐ด)
โ (cosโ๐ด) <
1) |
58 | 4 | rexri 8014 |
. . . . . 6
โข ฯ
โ โ* |
59 | | 0re 7956 |
. . . . . . 7
โข 0 โ
โ |
60 | 59, 4, 46 | ltleii 8059 |
. . . . . 6
โข 0 โค
ฯ |
61 | | lbicc2 9983 |
. . . . . 6
โข ((0
โ โ* โง ฯ โ โ* โง 0 โค
ฯ) โ 0 โ (0[,]ฯ)) |
62 | 8, 58, 60, 61 | mp3an 1337 |
. . . . 5
โข 0 โ
(0[,]ฯ) |
63 | 62 | a1i 9 |
. . . 4
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ 0
โ (0[,]ฯ)) |
64 | 1 | adantr 276 |
. . . . 5
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
๐ด โ
โ) |
65 | | 0red 7957 |
. . . . . 6
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ 0
โ โ) |
66 | 13 | simp2bi 1013 |
. . . . . . 7
โข (๐ด โ (0(,)(2 ยท ฯ))
โ 0 < ๐ด) |
67 | 66 | adantr 276 |
. . . . . 6
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ 0
< ๐ด) |
68 | 65, 64, 67 | ltled 8075 |
. . . . 5
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ 0
โค ๐ด) |
69 | 4 | a1i 9 |
. . . . . 6
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
ฯ โ โ) |
70 | | simpr 110 |
. . . . . 6
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
๐ด <
ฯ) |
71 | 64, 69, 70 | ltled 8075 |
. . . . 5
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
๐ด โค
ฯ) |
72 | 59, 4 | elicc2i 9938 |
. . . . 5
โข (๐ด โ (0[,]ฯ) โ (๐ด โ โ โง 0 โค
๐ด โง ๐ด โค ฯ)) |
73 | 64, 68, 71, 72 | syl3anbrc 1181 |
. . . 4
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
๐ด โ
(0[,]ฯ)) |
74 | 63, 73, 67 | cosordlem 14240 |
. . 3
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
(cosโ๐ด) <
(cosโ0)) |
75 | | cos0 11737 |
. . 3
โข
(cosโ0) = 1 |
76 | 74, 75 | breqtrdi 4044 |
. 2
โข ((๐ด โ (0(,)(2 ยท ฯ))
โง ๐ด < ฯ) โ
(cosโ๐ด) <
1) |
77 | | pirp 14180 |
. . . 4
โข ฯ
โ โ+ |
78 | | rphalflt 9682 |
. . . 4
โข (ฯ
โ โ+ โ (ฯ / 2) < ฯ) |
79 | 77, 78 | ax-mp 5 |
. . 3
โข (ฯ /
2) < ฯ |
80 | | axltwlin 8024 |
. . . 4
โข (((ฯ /
2) โ โ โง ฯ โ โ โง ๐ด โ โ) โ ((ฯ / 2) <
ฯ โ ((ฯ / 2) < ๐ด โจ ๐ด < ฯ))) |
81 | 24, 4, 1, 80 | mp3an12i 1341 |
. . 3
โข (๐ด โ (0(,)(2 ยท ฯ))
โ ((ฯ / 2) < ฯ โ ((ฯ / 2) < ๐ด โจ ๐ด < ฯ))) |
82 | 79, 81 | mpi 15 |
. 2
โข (๐ด โ (0(,)(2 ยท ฯ))
โ ((ฯ / 2) < ๐ด
โจ ๐ด <
ฯ)) |
83 | 57, 76, 82 | mpjaodan 798 |
1
โข (๐ด โ (0(,)(2 ยท ฯ))
โ (cosโ๐ด) <
1) |