Step | Hyp | Ref
| Expression |
1 | | simplr 767 |
. . . 4
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β
(cosβπ΄) =
0) |
2 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
π΄ β
(0[,]Ο)) |
3 | | 0re 11218 |
. . . . . . . . . . . . 13
β’ 0 β
β |
4 | | pire 25975 |
. . . . . . . . . . . . 13
β’ Ο
β β |
5 | 3, 4 | elicc2i 13392 |
. . . . . . . . . . . 12
β’ (π΄ β (0[,]Ο) β (π΄ β β β§ 0 β€
π΄ β§ π΄ β€ Ο)) |
6 | 2, 5 | sylib 217 |
. . . . . . . . . . 11
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(π΄ β β β§ 0
β€ π΄ β§ π΄ β€ Ο)) |
7 | 6 | simp1d 1142 |
. . . . . . . . . 10
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
π΄ β
β) |
8 | 7 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β π΄ β
β) |
9 | | simpr 485 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β 0 < π΄) |
10 | | simplr 767 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β π΄ < (Ο /
2)) |
11 | 3 | rexri 11274 |
. . . . . . . . . 10
β’ 0 β
β* |
12 | | halfpire 25981 |
. . . . . . . . . . 11
β’ (Ο /
2) β β |
13 | 12 | rexri 11274 |
. . . . . . . . . 10
β’ (Ο /
2) β β* |
14 | | elioo2 13367 |
. . . . . . . . . 10
β’ ((0
β β* β§ (Ο / 2) β β*) β
(π΄ β (0(,)(Ο / 2))
β (π΄ β β
β§ 0 < π΄ β§ π΄ < (Ο /
2)))) |
15 | 11, 13, 14 | mp2an 690 |
. . . . . . . . 9
β’ (π΄ β (0(,)(Ο / 2)) β
(π΄ β β β§ 0
< π΄ β§ π΄ < (Ο /
2))) |
16 | 8, 9, 10, 15 | syl3anbrc 1343 |
. . . . . . . 8
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β π΄ β (0(,)(Ο /
2))) |
17 | | sincosq1sgn 26015 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(0 < (sinβπ΄) β§
0 < (cosβπ΄))) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β (0 <
(sinβπ΄) β§ 0 <
(cosβπ΄))) |
19 | 18 | simprd 496 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β 0 <
(cosβπ΄)) |
20 | 19 | gt0ne0d 11780 |
. . . . 5
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
< π΄) β
(cosβπ΄) β
0) |
21 | | simpr 485 |
. . . . . . . 8
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
= π΄) β 0 = π΄) |
22 | 21 | fveq2d 6895 |
. . . . . . 7
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
= π΄) β (cosβ0) =
(cosβπ΄)) |
23 | | cos0 16095 |
. . . . . . 7
β’
(cosβ0) = 1 |
24 | 22, 23 | eqtr3di 2787 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
= π΄) β
(cosβπ΄) =
1) |
25 | | ax-1ne0 11181 |
. . . . . . 7
β’ 1 β
0 |
26 | 25 | a1i 11 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
= π΄) β 1 β
0) |
27 | 24, 26 | eqnetrd 3008 |
. . . . 5
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β§ 0
= π΄) β
(cosβπ΄) β
0) |
28 | 6 | simp2d 1143 |
. . . . . . 7
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β 0
β€ π΄) |
29 | | 0red 11219 |
. . . . . . . 8
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β 0
β β) |
30 | 29, 7 | leloed 11359 |
. . . . . . 7
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(0 β€ π΄ β (0 <
π΄ β¨ 0 = π΄))) |
31 | 28, 30 | mpbid 231 |
. . . . . 6
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(0 < π΄ β¨ 0 = π΄)) |
32 | 31 | adantr 481 |
. . . . 5
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β
(0 < π΄ β¨ 0 = π΄)) |
33 | 20, 27, 32 | mpjaodan 957 |
. . . 4
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β
(cosβπ΄) β
0) |
34 | 1, 33 | pm2.21ddne 3026 |
. . 3
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ < (Ο / 2)) β
π΄ = (Ο /
2)) |
35 | | simpr 485 |
. . 3
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
π΄ = (Ο / 2)) β
π΄ = (Ο /
2)) |
36 | | simplr 767 |
. . . 4
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β
(cosβπ΄) =
0) |
37 | 7 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β π΄ β
β) |
38 | | simplr 767 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β (Ο /
2) < π΄) |
39 | | simpr 485 |
. . . . . . . . 9
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β π΄ < Ο) |
40 | 4 | rexri 11274 |
. . . . . . . . . 10
β’ Ο
β β* |
41 | | elioo2 13367 |
. . . . . . . . . 10
β’ (((Ο /
2) β β* β§ Ο β β*) β
(π΄ β ((Ο /
2)(,)Ο) β (π΄ β
β β§ (Ο / 2) < π΄ β§ π΄ < Ο))) |
42 | 13, 40, 41 | mp2an 690 |
. . . . . . . . 9
β’ (π΄ β ((Ο / 2)(,)Ο)
β (π΄ β β
β§ (Ο / 2) < π΄
β§ π΄ <
Ο)) |
43 | 37, 38, 39, 42 | syl3anbrc 1343 |
. . . . . . . 8
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β π΄ β ((Ο /
2)(,)Ο)) |
44 | | sincosq2sgn 26016 |
. . . . . . . 8
β’ (π΄ β ((Ο / 2)(,)Ο)
β (0 < (sinβπ΄) β§ (cosβπ΄) < 0)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β (0 <
(sinβπ΄) β§
(cosβπ΄) <
0)) |
46 | 45 | simprd 496 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β
(cosβπ΄) <
0) |
47 | 46 | lt0ne0d 11781 |
. . . . 5
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ < Ο) β
(cosβπ΄) β
0) |
48 | | simpr 485 |
. . . . . . . 8
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ = Ο) β π΄ = Ο) |
49 | 48 | fveq2d 6895 |
. . . . . . 7
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ = Ο) β
(cosβπ΄) =
(cosβΟ)) |
50 | | cospi 25989 |
. . . . . . 7
β’
(cosβΟ) = -1 |
51 | 49, 50 | eqtrdi 2788 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ = Ο) β
(cosβπ΄) =
-1) |
52 | | neg1ne0 12330 |
. . . . . . 7
β’ -1 β
0 |
53 | 52 | a1i 11 |
. . . . . 6
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ = Ο) β -1 β
0) |
54 | 51, 53 | eqnetrd 3008 |
. . . . 5
β’ ((((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β§
π΄ = Ο) β
(cosβπ΄) β
0) |
55 | 6 | simp3d 1144 |
. . . . . . 7
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
π΄ β€
Ο) |
56 | 4 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
Ο β β) |
57 | 7, 56 | leloed 11359 |
. . . . . . 7
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(π΄ β€ Ο β (π΄ < Ο β¨ π΄ = Ο))) |
58 | 55, 57 | mpbid 231 |
. . . . . 6
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(π΄ < Ο β¨ π΄ = Ο)) |
59 | 58 | adantr 481 |
. . . . 5
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β
(π΄ < Ο β¨ π΄ = Ο)) |
60 | 47, 54, 59 | mpjaodan 957 |
. . . 4
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β
(cosβπ΄) β
0) |
61 | 36, 60 | pm2.21ddne 3026 |
. . 3
β’ (((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β§
(Ο / 2) < π΄) β
π΄ = (Ο /
2)) |
62 | 56 | rehalfcld 12461 |
. . . 4
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(Ο / 2) β β) |
63 | 7, 62 | lttri4d 11357 |
. . 3
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
(π΄ < (Ο / 2) β¨
π΄ = (Ο / 2) β¨ (Ο /
2) < π΄)) |
64 | 34, 35, 61, 63 | mpjao3dan 1431 |
. 2
β’ ((π΄ β (0[,]Ο) β§
(cosβπ΄) = 0) β
π΄ = (Ο /
2)) |
65 | | fveq2 6891 |
. . . 4
β’ (π΄ = (Ο / 2) β
(cosβπ΄) =
(cosβ(Ο / 2))) |
66 | | coshalfpi 25986 |
. . . 4
β’
(cosβ(Ο / 2)) = 0 |
67 | 65, 66 | eqtrdi 2788 |
. . 3
β’ (π΄ = (Ο / 2) β
(cosβπ΄) =
0) |
68 | 67 | adantl 482 |
. 2
β’ ((π΄ β (0[,]Ο) β§ π΄ = (Ο / 2)) β
(cosβπ΄) =
0) |
69 | 64, 68 | impbida 799 |
1
β’ (π΄ β (0[,]Ο) β
((cosβπ΄) = 0 β
π΄ = (Ο /
2))) |