Step | Hyp | Ref
| Expression |
1 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
2 | | pire 25831 |
. . . . . . . . 9
β’ Ο
β β |
3 | 2 | rexri 11220 |
. . . . . . . 8
β’ Ο
β β* |
4 | | icossre 13352 |
. . . . . . . 8
β’ ((0
β β β§ Ο β β*) β (0[,)Ο) β
β) |
5 | 1, 3, 4 | mp2an 691 |
. . . . . . 7
β’
(0[,)Ο) β β |
6 | 5 | sseli 3945 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β π΄ β
β) |
7 | 6 | recnd 11190 |
. . . . 5
β’ (π΄ β (0[,)Ο) β π΄ β
β) |
8 | 7 | halfcld 12405 |
. . . 4
β’ (π΄ β (0[,)Ο) β (π΄ / 2) β
β) |
9 | 6 | rehalfcld 12407 |
. . . . . . 7
β’ (π΄ β (0[,)Ο) β (π΄ / 2) β
β) |
10 | 9 | rered 15116 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β
(ββ(π΄ / 2)) =
(π΄ / 2)) |
11 | | elico2 13335 |
. . . . . . . 8
β’ ((0
β β β§ Ο β β*) β (π΄ β (0[,)Ο) β (π΄ β β β§ 0 β€ π΄ β§ π΄ < Ο))) |
12 | 1, 3, 11 | mp2an 691 |
. . . . . . 7
β’ (π΄ β (0[,)Ο) β (π΄ β β β§ 0 β€
π΄ β§ π΄ < Ο)) |
13 | | pipos 25833 |
. . . . . . . . . . . . 13
β’ 0 <
Ο |
14 | | lt0neg2 11669 |
. . . . . . . . . . . . . 14
β’ (Ο
β β β (0 < Ο β -Ο < 0)) |
15 | 2, 14 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (0 <
Ο β -Ο < 0) |
16 | 13, 15 | mpbi 229 |
. . . . . . . . . . . 12
β’ -Ο
< 0 |
17 | 2 | renegcli 11469 |
. . . . . . . . . . . . 13
β’ -Ο
β β |
18 | | ltletr 11254 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β β§ 0 β β β§ π΄ β β) β ((-Ο < 0 β§
0 β€ π΄) β -Ο <
π΄)) |
19 | 17, 1, 18 | mp3an12 1452 |
. . . . . . . . . . . 12
β’ (π΄ β β β ((-Ο
< 0 β§ 0 β€ π΄)
β -Ο < π΄)) |
20 | 16, 19 | mpani 695 |
. . . . . . . . . . 11
β’ (π΄ β β β (0 β€
π΄ β -Ο < π΄)) |
21 | | 2re 12234 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
22 | | 2pos 12263 |
. . . . . . . . . . . . . 14
β’ 0 <
2 |
23 | 21, 22 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (2 β
β β§ 0 < 2) |
24 | | ltdiv1 12026 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β β§ π΄
β β β§ (2 β β β§ 0 < 2)) β (-Ο <
π΄ β (-Ο / 2) <
(π΄ / 2))) |
25 | 17, 23, 24 | mp3an13 1453 |
. . . . . . . . . . . 12
β’ (π΄ β β β (-Ο
< π΄ β (-Ο / 2)
< (π΄ /
2))) |
26 | | picn 25832 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
27 | | 2cn 12235 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
28 | | 2ne0 12264 |
. . . . . . . . . . . . . 14
β’ 2 β
0 |
29 | | divneg 11854 |
. . . . . . . . . . . . . 14
β’ ((Ο
β β β§ 2 β β β§ 2 β 0) β -(Ο / 2) =
(-Ο / 2)) |
30 | 26, 27, 28, 29 | mp3an 1462 |
. . . . . . . . . . . . 13
β’ -(Ο /
2) = (-Ο / 2) |
31 | 30 | breq1i 5117 |
. . . . . . . . . . . 12
β’ (-(Ο /
2) < (π΄ / 2) β
(-Ο / 2) < (π΄ /
2)) |
32 | 25, 31 | bitr4di 289 |
. . . . . . . . . . 11
β’ (π΄ β β β (-Ο
< π΄ β -(Ο / 2)
< (π΄ /
2))) |
33 | 20, 32 | sylibd 238 |
. . . . . . . . . 10
β’ (π΄ β β β (0 β€
π΄ β -(Ο / 2) <
(π΄ / 2))) |
34 | | ltdiv1 12026 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ Ο
β β β§ (2 β β β§ 0 < 2)) β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
35 | 2, 23, 34 | mp3an23 1454 |
. . . . . . . . . . 11
β’ (π΄ β β β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
36 | 35 | biimpd 228 |
. . . . . . . . . 10
β’ (π΄ β β β (π΄ < Ο β (π΄ / 2) < (Ο /
2))) |
37 | 33, 36 | anim12d 610 |
. . . . . . . . 9
β’ (π΄ β β β ((0 β€
π΄ β§ π΄ < Ο) β (-(Ο / 2) < (π΄ / 2) β§ (π΄ / 2) < (Ο / 2)))) |
38 | | rehalfcl 12386 |
. . . . . . . . . . 11
β’ (π΄ β β β (π΄ / 2) β
β) |
39 | 38 | rexrd 11212 |
. . . . . . . . . 10
β’ (π΄ β β β (π΄ / 2) β
β*) |
40 | | halfpire 25837 |
. . . . . . . . . . . . 13
β’ (Ο /
2) β β |
41 | 40 | renegcli 11469 |
. . . . . . . . . . . 12
β’ -(Ο /
2) β β |
42 | 41 | rexri 11220 |
. . . . . . . . . . 11
β’ -(Ο /
2) β β* |
43 | 40 | rexri 11220 |
. . . . . . . . . . 11
β’ (Ο /
2) β β* |
44 | | elioo5 13328 |
. . . . . . . . . . 11
β’ ((-(Ο
/ 2) β β* β§ (Ο / 2) β β*
β§ (π΄ / 2) β
β*) β ((π΄ / 2) β (-(Ο / 2)(,)(Ο / 2))
β (-(Ο / 2) < (π΄
/ 2) β§ (π΄ / 2) <
(Ο / 2)))) |
45 | 42, 43, 44 | mp3an12 1452 |
. . . . . . . . . 10
β’ ((π΄ / 2) β β*
β ((π΄ / 2) β
(-(Ο / 2)(,)(Ο / 2)) β (-(Ο / 2) < (π΄ / 2) β§ (π΄ / 2) < (Ο / 2)))) |
46 | 39, 45 | syl 17 |
. . . . . . . . 9
β’ (π΄ β β β ((π΄ / 2) β (-(Ο /
2)(,)(Ο / 2)) β (-(Ο / 2) < (π΄ / 2) β§ (π΄ / 2) < (Ο / 2)))) |
47 | 37, 46 | sylibrd 259 |
. . . . . . . 8
β’ (π΄ β β β ((0 β€
π΄ β§ π΄ < Ο) β (π΄ / 2) β (-(Ο / 2)(,)(Ο /
2)))) |
48 | 47 | 3impib 1117 |
. . . . . . 7
β’ ((π΄ β β β§ 0 β€
π΄ β§ π΄ < Ο) β (π΄ / 2) β (-(Ο / 2)(,)(Ο /
2))) |
49 | 12, 48 | sylbi 216 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β (π΄ / 2) β (-(Ο /
2)(,)(Ο / 2))) |
50 | 10, 49 | eqeltrd 2838 |
. . . . 5
β’ (π΄ β (0[,)Ο) β
(ββ(π΄ / 2))
β (-(Ο / 2)(,)(Ο / 2))) |
51 | | cosne0 25901 |
. . . . 5
β’ (((π΄ / 2) β β β§
(ββ(π΄ / 2))
β (-(Ο / 2)(,)(Ο / 2))) β (cosβ(π΄ / 2)) β 0) |
52 | 8, 50, 51 | syl2anc 585 |
. . . 4
β’ (π΄ β (0[,)Ο) β
(cosβ(π΄ / 2)) β
0) |
53 | | tanval 16017 |
. . . 4
β’ (((π΄ / 2) β β β§
(cosβ(π΄ / 2)) β 0)
β (tanβ(π΄ / 2))
= ((sinβ(π΄ / 2)) /
(cosβ(π΄ /
2)))) |
54 | 8, 52, 53 | syl2anc 585 |
. . 3
β’ (π΄ β (0[,)Ο) β
(tanβ(π΄ / 2)) =
((sinβ(π΄ / 2)) /
(cosβ(π΄ /
2)))) |
55 | | 0xr 11209 |
. . . . . . 7
β’ 0 β
β* |
56 | | elico1 13314 |
. . . . . . 7
β’ ((0
β β* β§ Ο β β*) β (π΄ β (0[,)Ο) β (π΄ β β*
β§ 0 β€ π΄ β§ π΄ < Ο))) |
57 | 55, 3, 56 | mp2an 691 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β (π΄ β β*
β§ 0 β€ π΄ β§ π΄ < Ο)) |
58 | 21, 2 | remulcli 11178 |
. . . . . . . . . . 11
β’ (2
Β· Ο) β β |
59 | 58 | rexri 11220 |
. . . . . . . . . 10
β’ (2
Β· Ο) β β* |
60 | | 1lt2 12331 |
. . . . . . . . . . . . 13
β’ 1 <
2 |
61 | | ltmulgt12 12023 |
. . . . . . . . . . . . . 14
β’ ((Ο
β β β§ 2 β β β§ 0 < Ο) β (1 < 2
β Ο < (2 Β· Ο))) |
62 | 2, 21, 13, 61 | mp3an 1462 |
. . . . . . . . . . . . 13
β’ (1 < 2
β Ο < (2 Β· Ο)) |
63 | 60, 62 | mpbi 229 |
. . . . . . . . . . . 12
β’ Ο <
(2 Β· Ο) |
64 | | xrlttr 13066 |
. . . . . . . . . . . . 13
β’ ((π΄ β β*
β§ Ο β β* β§ (2 Β· Ο) β
β*) β ((π΄ < Ο β§ Ο < (2 Β·
Ο)) β π΄ < (2
Β· Ο))) |
65 | 3, 64 | mp3an2 1450 |
. . . . . . . . . . . 12
β’ ((π΄ β β*
β§ (2 Β· Ο) β β*) β ((π΄ < Ο β§ Ο < (2 Β·
Ο)) β π΄ < (2
Β· Ο))) |
66 | 63, 65 | mpan2i 696 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ (2 Β· Ο) β β*) β (π΄ < Ο β π΄ < (2 Β· Ο))) |
67 | | xrltle 13075 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ (2 Β· Ο) β β*) β (π΄ < (2 Β· Ο) β π΄ β€ (2 Β·
Ο))) |
68 | 66, 67 | syld 47 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ (2 Β· Ο) β β*) β (π΄ < Ο β π΄ β€ (2 Β· Ο))) |
69 | 59, 68 | mpan2 690 |
. . . . . . . . 9
β’ (π΄ β β*
β (π΄ < Ο β
π΄ β€ (2 Β·
Ο))) |
70 | 69 | anim2d 613 |
. . . . . . . 8
β’ (π΄ β β*
β ((0 β€ π΄ β§
π΄ < Ο) β (0 β€
π΄ β§ π΄ β€ (2 Β· Ο)))) |
71 | | elicc4 13338 |
. . . . . . . . 9
β’ ((0
β β* β§ (2 Β· Ο) β β*
β§ π΄ β
β*) β (π΄ β (0[,](2 Β· Ο)) β (0
β€ π΄ β§ π΄ β€ (2 Β·
Ο)))) |
72 | 55, 59, 71 | mp3an12 1452 |
. . . . . . . 8
β’ (π΄ β β*
β (π΄ β (0[,](2
Β· Ο)) β (0 β€ π΄ β§ π΄ β€ (2 Β· Ο)))) |
73 | 70, 72 | sylibrd 259 |
. . . . . . 7
β’ (π΄ β β*
β ((0 β€ π΄ β§
π΄ < Ο) β π΄ β (0[,](2 Β·
Ο)))) |
74 | 73 | 3impib 1117 |
. . . . . 6
β’ ((π΄ β β*
β§ 0 β€ π΄ β§ π΄ < Ο) β π΄ β (0[,](2 Β·
Ο))) |
75 | 57, 74 | sylbi 216 |
. . . . 5
β’ (π΄ β (0[,)Ο) β π΄ β (0[,](2 Β·
Ο))) |
76 | | sin2h 36097 |
. . . . 5
β’ (π΄ β (0[,](2 Β· Ο))
β (sinβ(π΄ / 2))
= (ββ((1 β (cosβπ΄)) / 2))) |
77 | 75, 76 | syl 17 |
. . . 4
β’ (π΄ β (0[,)Ο) β
(sinβ(π΄ / 2)) =
(ββ((1 β (cosβπ΄)) / 2))) |
78 | 1, 2, 13 | ltleii 11285 |
. . . . . . . . . . 11
β’ 0 β€
Ο |
79 | | le0neg2 11671 |
. . . . . . . . . . . 12
β’ (Ο
β β β (0 β€ Ο β -Ο β€ 0)) |
80 | 2, 79 | ax-mp 5 |
. . . . . . . . . . 11
β’ (0 β€
Ο β -Ο β€ 0) |
81 | 78, 80 | mpbi 229 |
. . . . . . . . . 10
β’ -Ο
β€ 0 |
82 | 17 | rexri 11220 |
. . . . . . . . . . 11
β’ -Ο
β β* |
83 | | xrletr 13084 |
. . . . . . . . . . 11
β’ ((-Ο
β β* β§ 0 β β* β§ π΄ β β*)
β ((-Ο β€ 0 β§ 0 β€ π΄) β -Ο β€ π΄)) |
84 | 82, 55, 83 | mp3an12 1452 |
. . . . . . . . . 10
β’ (π΄ β β*
β ((-Ο β€ 0 β§ 0 β€ π΄) β -Ο β€ π΄)) |
85 | 81, 84 | mpani 695 |
. . . . . . . . 9
β’ (π΄ β β*
β (0 β€ π΄ β
-Ο β€ π΄)) |
86 | | xrltle 13075 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ Ο β β*) β (π΄ < Ο β π΄ β€ Ο)) |
87 | 3, 86 | mpan2 690 |
. . . . . . . . 9
β’ (π΄ β β*
β (π΄ < Ο β
π΄ β€
Ο)) |
88 | 85, 87 | anim12d 610 |
. . . . . . . 8
β’ (π΄ β β*
β ((0 β€ π΄ β§
π΄ < Ο) β (-Ο
β€ π΄ β§ π΄ β€ Ο))) |
89 | | elicc4 13338 |
. . . . . . . . 9
β’ ((-Ο
β β* β§ Ο β β* β§ π΄ β β*)
β (π΄ β
(-Ο[,]Ο) β (-Ο β€ π΄ β§ π΄ β€ Ο))) |
90 | 82, 3, 89 | mp3an12 1452 |
. . . . . . . 8
β’ (π΄ β β*
β (π΄ β
(-Ο[,]Ο) β (-Ο β€ π΄ β§ π΄ β€ Ο))) |
91 | 88, 90 | sylibrd 259 |
. . . . . . 7
β’ (π΄ β β*
β ((0 β€ π΄ β§
π΄ < Ο) β π΄ β
(-Ο[,]Ο))) |
92 | 91 | 3impib 1117 |
. . . . . 6
β’ ((π΄ β β*
β§ 0 β€ π΄ β§ π΄ < Ο) β π΄ β
(-Ο[,]Ο)) |
93 | 57, 92 | sylbi 216 |
. . . . 5
β’ (π΄ β (0[,)Ο) β π΄ β
(-Ο[,]Ο)) |
94 | | cos2h 36098 |
. . . . 5
β’ (π΄ β (-Ο[,]Ο) β
(cosβ(π΄ / 2)) =
(ββ((1 + (cosβπ΄)) / 2))) |
95 | 93, 94 | syl 17 |
. . . 4
β’ (π΄ β (0[,)Ο) β
(cosβ(π΄ / 2)) =
(ββ((1 + (cosβπ΄)) / 2))) |
96 | 77, 95 | oveq12d 7380 |
. . 3
β’ (π΄ β (0[,)Ο) β
((sinβ(π΄ / 2)) /
(cosβ(π΄ / 2))) =
((ββ((1 β (cosβπ΄)) / 2)) / (ββ((1 +
(cosβπ΄)) /
2)))) |
97 | 54, 96 | eqtrd 2777 |
. 2
β’ (π΄ β (0[,)Ο) β
(tanβ(π΄ / 2)) =
((ββ((1 β (cosβπ΄)) / 2)) / (ββ((1 +
(cosβπ΄)) /
2)))) |
98 | | 1re 11162 |
. . . . 5
β’ 1 β
β |
99 | 6 | recoscld 16033 |
. . . . 5
β’ (π΄ β (0[,)Ο) β
(cosβπ΄) β
β) |
100 | | resubcl 11472 |
. . . . 5
β’ ((1
β β β§ (cosβπ΄) β β) β (1 β
(cosβπ΄)) β
β) |
101 | 98, 99, 100 | sylancr 588 |
. . . 4
β’ (π΄ β (0[,)Ο) β (1
β (cosβπ΄))
β β) |
102 | 101 | rehalfcld 12407 |
. . 3
β’ (π΄ β (0[,)Ο) β ((1
β (cosβπ΄)) / 2)
β β) |
103 | | cosbnd 16070 |
. . . . . 6
β’ (π΄ β β β (-1 β€
(cosβπ΄) β§
(cosβπ΄) β€
1)) |
104 | 103 | simprd 497 |
. . . . 5
β’ (π΄ β β β
(cosβπ΄) β€
1) |
105 | | recoscl 16030 |
. . . . . 6
β’ (π΄ β β β
(cosβπ΄) β
β) |
106 | | subge0 11675 |
. . . . . . 7
β’ ((1
β β β§ (cosβπ΄) β β) β (0 β€ (1 β
(cosβπ΄)) β
(cosβπ΄) β€
1)) |
107 | | halfnneg2 12391 |
. . . . . . . 8
β’ ((1
β (cosβπ΄))
β β β (0 β€ (1 β (cosβπ΄)) β 0 β€ ((1 β
(cosβπ΄)) /
2))) |
108 | 100, 107 | syl 17 |
. . . . . . 7
β’ ((1
β β β§ (cosβπ΄) β β) β (0 β€ (1 β
(cosβπ΄)) β 0
β€ ((1 β (cosβπ΄)) / 2))) |
109 | 106, 108 | bitr3d 281 |
. . . . . 6
β’ ((1
β β β§ (cosβπ΄) β β) β ((cosβπ΄) β€ 1 β 0 β€ ((1
β (cosβπ΄)) /
2))) |
110 | 98, 105, 109 | sylancr 588 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄) β€ 1
β 0 β€ ((1 β (cosβπ΄)) / 2))) |
111 | 104, 110 | mpbid 231 |
. . . 4
β’ (π΄ β β β 0 β€
((1 β (cosβπ΄))
/ 2)) |
112 | 6, 111 | syl 17 |
. . 3
β’ (π΄ β (0[,)Ο) β 0 β€
((1 β (cosβπ΄))
/ 2)) |
113 | | readdcl 11141 |
. . . . . 6
β’ ((1
β β β§ (cosβπ΄) β β) β (1 +
(cosβπ΄)) β
β) |
114 | 98, 99, 113 | sylancr 588 |
. . . . 5
β’ (π΄ β (0[,)Ο) β (1 +
(cosβπ΄)) β
β) |
115 | 103 | simpld 496 |
. . . . . . . 8
β’ (π΄ β β β -1 β€
(cosβπ΄)) |
116 | 98 | renegcli 11469 |
. . . . . . . . . 10
β’ -1 β
β |
117 | | subge0 11675 |
. . . . . . . . . 10
β’
(((cosβπ΄)
β β β§ -1 β β) β (0 β€ ((cosβπ΄) β -1) β -1 β€
(cosβπ΄))) |
118 | 105, 116,
117 | sylancl 587 |
. . . . . . . . 9
β’ (π΄ β β β (0 β€
((cosβπ΄) β -1)
β -1 β€ (cosβπ΄))) |
119 | | recn 11148 |
. . . . . . . . . . . 12
β’ (π΄ β β β π΄ β
β) |
120 | 119 | coscld 16020 |
. . . . . . . . . . 11
β’ (π΄ β β β
(cosβπ΄) β
β) |
121 | | ax-1cn 11116 |
. . . . . . . . . . 11
β’ 1 β
β |
122 | | subneg 11457 |
. . . . . . . . . . . 12
β’
(((cosβπ΄)
β β β§ 1 β β) β ((cosβπ΄) β -1) = ((cosβπ΄) + 1)) |
123 | | addcom 11348 |
. . . . . . . . . . . 12
β’
(((cosβπ΄)
β β β§ 1 β β) β ((cosβπ΄) + 1) = (1 + (cosβπ΄))) |
124 | 122, 123 | eqtrd 2777 |
. . . . . . . . . . 11
β’
(((cosβπ΄)
β β β§ 1 β β) β ((cosβπ΄) β -1) = (1 + (cosβπ΄))) |
125 | 120, 121,
124 | sylancl 587 |
. . . . . . . . . 10
β’ (π΄ β β β
((cosβπ΄) β -1)
= (1 + (cosβπ΄))) |
126 | 125 | breq2d 5122 |
. . . . . . . . 9
β’ (π΄ β β β (0 β€
((cosβπ΄) β -1)
β 0 β€ (1 + (cosβπ΄)))) |
127 | 118, 126 | bitr3d 281 |
. . . . . . . 8
β’ (π΄ β β β (-1 β€
(cosβπ΄) β 0 β€
(1 + (cosβπ΄)))) |
128 | 115, 127 | mpbid 231 |
. . . . . . 7
β’ (π΄ β β β 0 β€ (1
+ (cosβπ΄))) |
129 | 6, 128 | syl 17 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β 0 β€
(1 + (cosβπ΄))) |
130 | | snunioo 13402 |
. . . . . . . . . 10
β’ ((0
β β* β§ Ο β β* β§ 0 <
Ο) β ({0} βͺ (0(,)Ο)) = (0[,)Ο)) |
131 | 55, 3, 13, 130 | mp3an 1462 |
. . . . . . . . 9
β’ ({0}
βͺ (0(,)Ο)) = (0[,)Ο) |
132 | 131 | eleq2i 2830 |
. . . . . . . 8
β’ (π΄ β ({0} βͺ (0(,)Ο))
β π΄ β
(0[,)Ο)) |
133 | | elun 4113 |
. . . . . . . 8
β’ (π΄ β ({0} βͺ (0(,)Ο))
β (π΄ β {0} β¨
π΄ β
(0(,)Ο))) |
134 | 132, 133 | bitr3i 277 |
. . . . . . 7
β’ (π΄ β (0[,)Ο) β (π΄ β {0} β¨ π΄ β
(0(,)Ο))) |
135 | | elsni 4608 |
. . . . . . . . 9
β’ (π΄ β {0} β π΄ = 0) |
136 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π΄ = 0 β (cosβπ΄) =
(cosβ0)) |
137 | | cos0 16039 |
. . . . . . . . . . . . 13
β’
(cosβ0) = 1 |
138 | 136, 137 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π΄ = 0 β (cosβπ΄) = 1) |
139 | 138 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π΄ = 0 β (1 +
(cosβπ΄)) = (1 +
1)) |
140 | | df-2 12223 |
. . . . . . . . . . 11
β’ 2 = (1 +
1) |
141 | 139, 140 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π΄ = 0 β (1 +
(cosβπ΄)) =
2) |
142 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ = 0 β 2 β
0) |
143 | 141, 142 | eqnetrd 3012 |
. . . . . . . . 9
β’ (π΄ = 0 β (1 +
(cosβπ΄)) β
0) |
144 | 135, 143 | syl 17 |
. . . . . . . 8
β’ (π΄ β {0} β (1 +
(cosβπ΄)) β
0) |
145 | | sinq12gt0 25880 |
. . . . . . . . 9
β’ (π΄ β (0(,)Ο) β 0 <
(sinβπ΄)) |
146 | | ltne 11259 |
. . . . . . . . . . 11
β’ ((0
β β β§ 0 < (sinβπ΄)) β (sinβπ΄) β 0) |
147 | 1, 146 | mpan 689 |
. . . . . . . . . 10
β’ (0 <
(sinβπ΄) β
(sinβπ΄) β
0) |
148 | | elioore 13301 |
. . . . . . . . . . . . 13
β’ (π΄ β (0(,)Ο) β π΄ β
β) |
149 | 148 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π΄ β (0(,)Ο) β π΄ β
β) |
150 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (-1 =
(cosβπ΄) β
(-1β2) = ((cosβπ΄)β2)) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (-1 =
(cosβπ΄) β
(-1β2) = ((cosβπ΄)β2))) |
152 | | df-neg 11395 |
. . . . . . . . . . . . . . 15
β’ -1 = (0
β 1) |
153 | 152 | eqeq1i 2742 |
. . . . . . . . . . . . . 14
β’ (-1 =
(cosβπ΄) β (0
β 1) = (cosβπ΄)) |
154 | | coscl 16016 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(cosβπ΄) β
β) |
155 | | 0cn 11154 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
156 | | subadd 11411 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β β§ 1 β β β§ (cosβπ΄) β β) β ((0 β 1) =
(cosβπ΄) β (1 +
(cosβπ΄)) =
0)) |
157 | 155, 121,
156 | mp3an12 1452 |
. . . . . . . . . . . . . . 15
β’
((cosβπ΄)
β β β ((0 β 1) = (cosβπ΄) β (1 + (cosβπ΄)) = 0)) |
158 | 154, 157 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β ((0
β 1) = (cosβπ΄)
β (1 + (cosβπ΄))
= 0)) |
159 | 153, 158 | bitrid 283 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (-1 =
(cosβπ΄) β (1 +
(cosβπ΄)) =
0)) |
160 | | sincl 16015 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(sinβπ΄) β
β) |
161 | 160 | sqcld 14056 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
162 | | 0cnd 11155 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β 0 β
β) |
163 | 154 | sqcld 14056 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
164 | 161, 162,
163 | addcan2d 11366 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(0 + ((cosβπ΄)β2)) β ((sinβπ΄)β2) = 0)) |
165 | | sincossq 16065 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
166 | | neg1sqe1 14107 |
. . . . . . . . . . . . . . . 16
β’
(-1β2) = 1 |
167 | 165, 166 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(-1β2)) |
168 | 163 | addid2d 11363 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β (0 +
((cosβπ΄)β2)) =
((cosβπ΄)β2)) |
169 | 167, 168 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
((((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(0 + ((cosβπ΄)β2)) β (-1β2) =
((cosβπ΄)β2))) |
170 | | sqeq0 14032 |
. . . . . . . . . . . . . . 15
β’
((sinβπ΄)
β β β (((sinβπ΄)β2) = 0 β (sinβπ΄) = 0)) |
171 | 160, 170 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β
(((sinβπ΄)β2) = 0
β (sinβπ΄) =
0)) |
172 | 164, 169,
171 | 3bitr3d 309 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
((-1β2) = ((cosβπ΄)β2) β (sinβπ΄) = 0)) |
173 | 151, 159,
172 | 3imtr3d 293 |
. . . . . . . . . . . 12
β’ (π΄ β β β ((1 +
(cosβπ΄)) = 0 β
(sinβπ΄) =
0)) |
174 | 149, 173 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)Ο) β ((1 +
(cosβπ΄)) = 0 β
(sinβπ΄) =
0)) |
175 | 174 | necon3d 2965 |
. . . . . . . . . 10
β’ (π΄ β (0(,)Ο) β
((sinβπ΄) β 0
β (1 + (cosβπ΄))
β 0)) |
176 | 147, 175 | syl5 34 |
. . . . . . . . 9
β’ (π΄ β (0(,)Ο) β (0
< (sinβπ΄) β
(1 + (cosβπ΄)) β
0)) |
177 | 145, 176 | mpd 15 |
. . . . . . . 8
β’ (π΄ β (0(,)Ο) β (1 +
(cosβπ΄)) β
0) |
178 | 144, 177 | jaoi 856 |
. . . . . . 7
β’ ((π΄ β {0} β¨ π΄ β (0(,)Ο)) β (1 +
(cosβπ΄)) β
0) |
179 | 134, 178 | sylbi 216 |
. . . . . 6
β’ (π΄ β (0[,)Ο) β (1 +
(cosβπ΄)) β
0) |
180 | 114, 129,
179 | ne0gt0d 11299 |
. . . . 5
β’ (π΄ β (0[,)Ο) β 0 <
(1 + (cosβπ΄))) |
181 | 114, 180 | elrpd 12961 |
. . . 4
β’ (π΄ β (0[,)Ο) β (1 +
(cosβπ΄)) β
β+) |
182 | 181 | rphalfcld 12976 |
. . 3
β’ (π΄ β (0[,)Ο) β ((1 +
(cosβπ΄)) / 2) β
β+) |
183 | 102, 112,
182 | sqrtdivd 15315 |
. 2
β’ (π΄ β (0[,)Ο) β
(ββ(((1 β (cosβπ΄)) / 2) / ((1 + (cosβπ΄)) / 2))) = ((ββ((1 β
(cosβπ΄)) / 2)) /
(ββ((1 + (cosβπ΄)) / 2)))) |
184 | 7 | coscld 16020 |
. . . . 5
β’ (π΄ β (0[,)Ο) β
(cosβπ΄) β
β) |
185 | | subcl 11407 |
. . . . 5
β’ ((1
β β β§ (cosβπ΄) β β) β (1 β
(cosβπ΄)) β
β) |
186 | 121, 184,
185 | sylancr 588 |
. . . 4
β’ (π΄ β (0[,)Ο) β (1
β (cosβπ΄))
β β) |
187 | | addcl 11140 |
. . . . 5
β’ ((1
β β β§ (cosβπ΄) β β) β (1 +
(cosβπ΄)) β
β) |
188 | 121, 184,
187 | sylancr 588 |
. . . 4
β’ (π΄ β (0[,)Ο) β (1 +
(cosβπ΄)) β
β) |
189 | | 2cnne0 12370 |
. . . . 5
β’ (2 β
β β§ 2 β 0) |
190 | | divcan7 11871 |
. . . . 5
β’ (((1
β (cosβπ΄))
β β β§ ((1 + (cosβπ΄)) β β β§ (1 +
(cosβπ΄)) β 0)
β§ (2 β β β§ 2 β 0)) β (((1 β (cosβπ΄)) / 2) / ((1 + (cosβπ΄)) / 2)) = ((1 β
(cosβπ΄)) / (1 +
(cosβπ΄)))) |
191 | 189, 190 | mp3an3 1451 |
. . . 4
β’ (((1
β (cosβπ΄))
β β β§ ((1 + (cosβπ΄)) β β β§ (1 +
(cosβπ΄)) β 0))
β (((1 β (cosβπ΄)) / 2) / ((1 + (cosβπ΄)) / 2)) = ((1 β (cosβπ΄)) / (1 + (cosβπ΄)))) |
192 | 186, 188,
179, 191 | syl12anc 836 |
. . 3
β’ (π΄ β (0[,)Ο) β (((1
β (cosβπ΄)) / 2)
/ ((1 + (cosβπ΄)) /
2)) = ((1 β (cosβπ΄)) / (1 + (cosβπ΄)))) |
193 | 192 | fveq2d 6851 |
. 2
β’ (π΄ β (0[,)Ο) β
(ββ(((1 β (cosβπ΄)) / 2) / ((1 + (cosβπ΄)) / 2))) = (ββ((1 β
(cosβπ΄)) / (1 +
(cosβπ΄))))) |
194 | 97, 183, 193 | 3eqtr2d 2783 |
1
β’ (π΄ β (0[,)Ο) β
(tanβ(π΄ / 2)) =
(ββ((1 β (cosβπ΄)) / (1 + (cosβπ΄))))) |