Step | Hyp | Ref
| Expression |
1 | | tanrpcl 25884 |
. . . . . . . 8
β’ (π΄ β (0(,)(Ο / 2)) β
(tanβπ΄) β
β+) |
2 | 1 | adantl 483 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(tanβπ΄) β
β+) |
3 | 2 | rpreccld 12975 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(1 / (tanβπ΄)) β
β+) |
4 | 3 | rpcnd 12967 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(1 / (tanβπ΄)) β
β) |
5 | | ax-icn 11118 |
. . . . . 6
β’ i β
β |
6 | 5 | a1i 11 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
i β β) |
7 | | basel.n |
. . . . . . 7
β’ π = ((2 Β· π) + 1) |
8 | | 2nn 12234 |
. . . . . . . . 9
β’ 2 β
β |
9 | | simpl 484 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β) |
10 | | nnmulcl 12185 |
. . . . . . . . 9
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(2 Β· π) β
β) |
12 | 11 | peano2nnd 12178 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((2 Β· π) + 1) β
β) |
13 | 7, 12 | eqeltrid 2838 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β) |
14 | 13 | nnnn0d 12481 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β0) |
15 | | binom 15723 |
. . . . 5
β’ (((1 /
(tanβπ΄)) β
β β§ i β β β§ π β β0) β (((1 /
(tanβπ΄)) +
i)βπ) = Ξ£π β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) |
16 | 4, 6, 14, 15 | syl3anc 1372 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((1 / (tanβπ΄)) +
i)βπ) = Ξ£π β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) |
17 | | elioore 13303 |
. . . . . . . . . . 11
β’ (π΄ β (0(,)(Ο / 2)) β
π΄ β
β) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π΄ β
β) |
19 | 18 | recoscld 16034 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(cosβπ΄) β
β) |
20 | 19 | recnd 11191 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(cosβπ΄) β
β) |
21 | 18 | resincld 16033 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβπ΄) β
β) |
22 | 21 | recnd 11191 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβπ΄) β
β) |
23 | | mulcl 11143 |
. . . . . . . . 9
β’ ((i
β β β§ (sinβπ΄) β β) β (i Β·
(sinβπ΄)) β
β) |
24 | 5, 22, 23 | sylancr 588 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(i Β· (sinβπ΄))
β β) |
25 | 20, 24 | addcld 11182 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((cosβπ΄) + (i
Β· (sinβπ΄)))
β β) |
26 | | sincosq1sgn 25878 |
. . . . . . . . . 10
β’ (π΄ β (0(,)(Ο / 2)) β
(0 < (sinβπ΄) β§
0 < (cosβπ΄))) |
27 | 26 | adantl 483 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(0 < (sinβπ΄) β§
0 < (cosβπ΄))) |
28 | 27 | simpld 496 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
0 < (sinβπ΄)) |
29 | 28 | gt0ne0d 11727 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβπ΄) β
0) |
30 | 25, 22, 29, 14 | expdivd 14074 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((((cosβπ΄) + (i
Β· (sinβπ΄))) /
(sinβπ΄))βπ) = ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) / ((sinβπ΄)βπ))) |
31 | 20, 24, 22, 29 | divdird 11977 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβπ΄) + (i
Β· (sinβπ΄))) /
(sinβπ΄)) =
(((cosβπ΄) /
(sinβπ΄)) + ((i
Β· (sinβπ΄)) /
(sinβπ΄)))) |
32 | 18 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π΄ β
β) |
33 | 27 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
0 < (cosβπ΄)) |
34 | 33 | gt0ne0d 11727 |
. . . . . . . . . . . 12
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(cosβπ΄) β
0) |
35 | | tanval 16018 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
36 | 32, 34, 35 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
37 | 36 | oveq2d 7377 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(1 / (tanβπ΄)) = (1 /
((sinβπ΄) /
(cosβπ΄)))) |
38 | 22, 20, 29, 34 | recdivd 11956 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(1 / ((sinβπ΄) /
(cosβπ΄))) =
((cosβπ΄) /
(sinβπ΄))) |
39 | 37, 38 | eqtr2d 2774 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((cosβπ΄) /
(sinβπ΄)) = (1 /
(tanβπ΄))) |
40 | 6, 22, 29 | divcan4d 11945 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((i Β· (sinβπ΄))
/ (sinβπ΄)) =
i) |
41 | 39, 40 | oveq12d 7379 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβπ΄) /
(sinβπ΄)) + ((i
Β· (sinβπ΄)) /
(sinβπ΄))) = ((1 /
(tanβπ΄)) +
i)) |
42 | 31, 41 | eqtrd 2773 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβπ΄) + (i
Β· (sinβπ΄))) /
(sinβπ΄)) = ((1 /
(tanβπ΄)) +
i)) |
43 | 42 | oveq1d 7376 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((((cosβπ΄) + (i
Β· (sinβπ΄))) /
(sinβπ΄))βπ) = (((1 / (tanβπ΄)) + i)βπ)) |
44 | 13 | nnzd 12534 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β€) |
45 | | demoivre 16090 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β€) β
(((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) |
46 | 32, 44, 45 | syl2anc 585 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) |
47 | 46 | oveq1d 7376 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) / ((sinβπ΄)βπ)) = (((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) / ((sinβπ΄)βπ))) |
48 | 30, 43, 47 | 3eqtr3d 2781 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((1 / (tanβπ΄)) +
i)βπ) =
(((cosβ(π Β·
π΄)) + (i Β·
(sinβ(π Β·
π΄)))) / ((sinβπ΄)βπ))) |
49 | 13 | nnred 12176 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β) |
50 | 49, 18 | remulcld 11193 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π Β· π΄) β
β) |
51 | 50 | recoscld 16034 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(cosβ(π Β·
π΄)) β
β) |
52 | 51 | recnd 11191 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(cosβ(π Β·
π΄)) β
β) |
53 | 50 | resincld 16033 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβ(π Β·
π΄)) β
β) |
54 | 53 | recnd 11191 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβ(π Β·
π΄)) β
β) |
55 | | mulcl 11143 |
. . . . . . 7
β’ ((i
β β β§ (sinβ(π Β· π΄)) β β) β (i Β·
(sinβ(π Β·
π΄))) β
β) |
56 | 5, 54, 55 | sylancr 588 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(i Β· (sinβ(π
Β· π΄))) β
β) |
57 | 21, 28 | elrpd 12962 |
. . . . . . . 8
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(sinβπ΄) β
β+) |
58 | 57, 44 | rpexpcld 14159 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((sinβπ΄)βπ) β
β+) |
59 | 58 | rpcnd 12967 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((sinβπ΄)βπ) β
β) |
60 | 58 | rpne0d 12970 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((sinβπ΄)βπ) β 0) |
61 | 52, 56, 59, 60 | divdird 11977 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβ(π Β·
π΄)) + (i Β·
(sinβ(π Β·
π΄)))) / ((sinβπ΄)βπ)) = (((cosβ(π Β· π΄)) / ((sinβπ΄)βπ)) + ((i Β· (sinβ(π Β· π΄))) / ((sinβπ΄)βπ)))) |
62 | 6, 54, 59, 60 | divassd 11974 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((i Β· (sinβ(π
Β· π΄))) /
((sinβπ΄)βπ)) = (i Β·
((sinβ(π Β·
π΄)) / ((sinβπ΄)βπ)))) |
63 | 62 | oveq2d 7377 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((cosβ(π Β·
π΄)) / ((sinβπ΄)βπ)) + ((i Β· (sinβ(π Β· π΄))) / ((sinβπ΄)βπ))) = (((cosβ(π Β· π΄)) / ((sinβπ΄)βπ)) + (i Β· ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))))) |
64 | 48, 61, 63 | 3eqtrd 2777 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(((1 / (tanβπ΄)) +
i)βπ) =
(((cosβ(π Β·
π΄)) / ((sinβπ΄)βπ)) + (i Β· ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))))) |
65 | 16, 64 | eqtr3d 2775 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
Ξ£π β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))) = (((cosβ(π Β· π΄)) / ((sinβπ΄)βπ)) + (i Β· ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))))) |
66 | 65 | fveq2d 6850 |
. 2
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(ββΞ£π
β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = (ββ(((cosβ(π Β· π΄)) / ((sinβπ΄)βπ)) + (i Β· ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ)))))) |
67 | | oveq2 7369 |
. . . . . . 7
β’ (π = (π β (2 Β· π)) β (πCπ) = (πC(π β (2 Β· π)))) |
68 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = (π β (2 Β· π)) β (π β π) = (π β (π β (2 Β· π)))) |
69 | 68 | oveq2d 7377 |
. . . . . . . 8
β’ (π = (π β (2 Β· π)) β ((1 / (tanβπ΄))β(π β π)) = ((1 / (tanβπ΄))β(π β (π β (2 Β· π))))) |
70 | | oveq2 7369 |
. . . . . . . 8
β’ (π = (π β (2 Β· π)) β (iβπ) = (iβ(π β (2 Β· π)))) |
71 | 69, 70 | oveq12d 7379 |
. . . . . . 7
β’ (π = (π β (2 Β· π)) β (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)) = (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π))))) |
72 | 67, 71 | oveq12d 7379 |
. . . . . 6
β’ (π = (π β (2 Β· π)) β ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))) = ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))))) |
73 | 72 | fveq2d 6850 |
. . . . 5
β’ (π = (π β (2 Β· π)) β (ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = (ββ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π))))))) |
74 | | fzfid 13887 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(0...π) β
Fin) |
75 | | 2nn0 12438 |
. . . . . . . . . . . . 13
β’ 2 β
β0 |
76 | | elfznn0 13543 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β π β β0) |
77 | 76 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β0) |
78 | | nn0mulcl 12457 |
. . . . . . . . . . . . 13
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
79 | 75, 77, 78 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β0) |
80 | 79 | nn0red 12482 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β) |
81 | 11 | nnred 12176 |
. . . . . . . . . . . 12
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(2 Β· π) β
β) |
82 | 81 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β) |
83 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
84 | | elfzle2 13454 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β€ π) |
85 | 84 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β€ π) |
86 | 77 | nn0red 12482 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
87 | | nnre 12168 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
88 | 87 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
89 | | 2re 12235 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
90 | | 2pos 12264 |
. . . . . . . . . . . . . . 15
β’ 0 <
2 |
91 | 89, 90 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (2 β
β β§ 0 < 2) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 β β
β§ 0 < 2)) |
93 | | lemul2 12016 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β β§ (2 β
β β§ 0 < 2)) β (π β€ π β (2 Β· π) β€ (2 Β· π))) |
94 | 86, 88, 92, 93 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β€ π β (2 Β· π) β€ (2 Β· π))) |
95 | 85, 94 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β€ (2 Β· π)) |
96 | 82 | lep1d 12094 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β€ ((2 Β· π) + 1)) |
97 | 96, 7 | breqtrrdi 5151 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β€ π) |
98 | 80, 82, 83, 95, 97 | letrd 11320 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β€ π) |
99 | | nn0uz 12813 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
100 | 79, 99 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
(β€β₯β0)) |
101 | 44 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β€) |
102 | | elfz5 13442 |
. . . . . . . . . . 11
β’ (((2
Β· π) β
(β€β₯β0) β§ π β β€) β ((2 Β· π) β (0...π) β (2 Β· π) β€ π)) |
103 | 100, 101,
102 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((2 Β· π) β (0...π) β (2 Β· π) β€ π)) |
104 | 98, 103 | mpbird 257 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β (0...π)) |
105 | | fznn0sub2 13557 |
. . . . . . . . 9
β’ ((2
Β· π) β
(0...π) β (π β (2 Β· π)) β (0...π)) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β (2 Β· π)) β (0...π)) |
107 | 106 | ex 414 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π β (0...π) β (π β (2 Β· π)) β (0...π))) |
108 | 13 | nncnd 12177 |
. . . . . . . . . . 11
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
π β
β) |
109 | 108 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β π β β) |
110 | | 2cn 12236 |
. . . . . . . . . . 11
β’ 2 β
β |
111 | | elfzelz 13450 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β€) |
112 | 111 | zcnd 12616 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
113 | 112 | ad2antrl 727 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β π β β) |
114 | | mulcl 11143 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
115 | 110, 113,
114 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β (2 Β· π) β β) |
116 | 112 | ssriv 3952 |
. . . . . . . . . . . 12
β’
(0...π) β
β |
117 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β π β (0...π)) |
118 | 116, 117 | sselid 3946 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β π β β) |
119 | | mulcl 11143 |
. . . . . . . . . . 11
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
120 | 110, 118,
119 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β (2 Β· π) β β) |
121 | 109, 115,
120 | subcanad 11563 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β ((π β (2 Β· π)) = (π β (2 Β· π)) β (2 Β· π) = (2 Β· π))) |
122 | | 2cnne0 12371 |
. . . . . . . . . . 11
β’ (2 β
β β§ 2 β 0) |
123 | 122 | a1i 11 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β (2 β β β§ 2 β
0)) |
124 | | mulcan 11800 |
. . . . . . . . . 10
β’ ((π β β β§ π β β β§ (2 β
β β§ 2 β 0)) β ((2 Β· π) = (2 Β· π) β π = π)) |
125 | 113, 118,
123, 124 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β ((2 Β· π) = (2 Β· π) β π = π)) |
126 | 121, 125 | bitrd 279 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ π β (0...π))) β ((π β (2 Β· π)) = (π β (2 Β· π)) β π = π)) |
127 | 126 | ex 414 |
. . . . . . 7
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((π β (0...π) β§ π β (0...π)) β ((π β (2 Β· π)) = (π β (2 Β· π)) β π = π))) |
128 | 107, 127 | dom2lem 8938 |
. . . . . 6
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π β (0...π) β¦ (π β (2 Β· π))):(0...π)β1-1β(0...π)) |
129 | | f1f1orn 6799 |
. . . . . 6
β’ ((π β (0...π) β¦ (π β (2 Β· π))):(0...π)β1-1β(0...π) β (π β (0...π) β¦ (π β (2 Β· π))):(0...π)β1-1-ontoβran
(π β (0...π) β¦ (π β (2 Β· π)))) |
130 | 128, 129 | syl 17 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π β (0...π) β¦ (π β (2 Β· π))):(0...π)β1-1-ontoβran
(π β (0...π) β¦ (π β (2 Β· π)))) |
131 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π β (2 Β· π) = (2 Β· π)) |
132 | 131 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π β (2 Β· π)) = (π β (2 Β· π))) |
133 | | eqid 2733 |
. . . . . . 7
β’ (π β (0...π) β¦ (π β (2 Β· π))) = (π β (0...π) β¦ (π β (2 Β· π))) |
134 | | ovex 7394 |
. . . . . . 7
β’ (π β (2 Β· π)) β V |
135 | 132, 133,
134 | fvmpt 6952 |
. . . . . 6
β’ (π β (0...π) β ((π β (0...π) β¦ (π β (2 Β· π)))βπ) = (π β (2 Β· π))) |
136 | 135 | adantl 483 |
. . . . 5
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((π β (0...π) β¦ (π β (2 Β· π)))βπ) = (π β (2 Β· π))) |
137 | 106 | fmpttd 7067 |
. . . . . . . . . 10
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π β (0...π) β¦ (π β (2 Β· π))):(0...π)βΆ(0...π)) |
138 | 137 | frnd 6680 |
. . . . . . . . 9
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
ran (π β (0...π) β¦ (π β (2 Β· π))) β (0...π)) |
139 | 138 | sselda 3948 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ran (π β (0...π) β¦ (π β (2 Β· π)))) β π β (0...π)) |
140 | | bccl2 14232 |
. . . . . . . . . . 11
β’ (π β (0...π) β (πCπ) β β) |
141 | 140 | adantl 483 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πCπ) β β) |
142 | 141 | nncnd 12177 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πCπ) β β) |
143 | 2 | rprecred 12976 |
. . . . . . . . . . . 12
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(1 / (tanβπ΄)) β
β) |
144 | | fznn0sub 13482 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (π β π) β
β0) |
145 | | reexpcl 13993 |
. . . . . . . . . . . 12
β’ (((1 /
(tanβπ΄)) β
β β§ (π β
π) β
β0) β ((1 / (tanβπ΄))β(π β π)) β β) |
146 | 143, 144,
145 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((1 / (tanβπ΄))β(π β π)) β β) |
147 | 146 | recnd 11191 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((1 / (tanβπ΄))β(π β π)) β β) |
148 | | elfznn0 13543 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β0) |
149 | 148 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β0) |
150 | | expcl 13994 |
. . . . . . . . . . 11
β’ ((i
β β β§ π
β β0) β (iβπ) β β) |
151 | 5, 149, 150 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβπ) β
β) |
152 | 147, 151 | mulcld 11183 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((1 /
(tanβπ΄))β(π β π)) Β· (iβπ)) β β) |
153 | 142, 152 | mulcld 11183 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))) β β) |
154 | 139, 153 | syldan 592 |
. . . . . . 7
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ran (π β (0...π) β¦ (π β (2 Β· π)))) β ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))) β β) |
155 | 154 | imcld 15089 |
. . . . . 6
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ran (π β (0...π) β¦ (π β (2 Β· π)))) β (ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) β β) |
156 | 155 | recnd 11191 |
. . . . 5
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ran (π β (0...π) β¦ (π β (2 Β· π)))) β (ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) β β) |
157 | 73, 74, 130, 136, 156 | fsumf1o 15616 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
Ξ£π β ran (π β (0...π) β¦ (π β (2 Β· π)))(ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = Ξ£π β (0...π)(ββ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π))))))) |
158 | | eldifi 4090 |
. . . . . . . 8
β’ (π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π)))) β π β (0...π)) |
159 | 141 | nnred 12176 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πCπ) β β) |
160 | 158, 159 | sylan2 594 |
. . . . . . 7
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β (πCπ) β β) |
161 | 158, 146 | sylan2 594 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β ((1 / (tanβπ΄))β(π β π)) β β) |
162 | | eldif 3924 |
. . . . . . . . 9
β’ (π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π)))) β (π β (0...π) β§ Β¬ π β ran (π β (0...π) β¦ (π β (2 Β· π))))) |
163 | | elfzelz 13450 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β€) |
164 | 163 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β€) |
165 | | zeo 12597 |
. . . . . . . . . . . . . 14
β’ (π β β€ β ((π / 2) β β€ β¨
((π + 1) / 2) β
β€)) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((π / 2) β β€ β¨ ((π + 1) / 2) β
β€)) |
167 | | i2 14115 |
. . . . . . . . . . . . . . . . . 18
β’
(iβ2) = -1 |
168 | 167 | oveq1i 7371 |
. . . . . . . . . . . . . . . . 17
β’
((iβ2)β(π
/ 2)) = (-1β(π /
2)) |
169 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (π / 2) β
β€) |
170 | 148 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β π β
β0) |
171 | | nn0re 12430 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β π β
β) |
172 | | nn0ge0 12446 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β 0 β€ π) |
173 | | divge0 12032 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ 0 β€
π) β§ (2 β β
β§ 0 < 2)) β 0 β€ (π / 2)) |
174 | 89, 90, 173 | mpanr12 704 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ 0 β€
π) β 0 β€ (π / 2)) |
175 | 171, 172,
174 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β 0 β€ (π /
2)) |
176 | 170, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β 0 β€ (π / 2)) |
177 | | elnn0z 12520 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π / 2) β β0
β ((π / 2) β
β€ β§ 0 β€ (π /
2))) |
178 | 169, 176,
177 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (π / 2) β
β0) |
179 | | expmul 14022 |
. . . . . . . . . . . . . . . . . . 19
β’ ((i
β β β§ 2 β β0 β§ (π / 2) β β0) β
(iβ(2 Β· (π /
2))) = ((iβ2)β(π
/ 2))) |
180 | 5, 75, 178, 179 | mp3an12i 1466 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (iβ(2
Β· (π / 2))) =
((iβ2)β(π /
2))) |
181 | 170 | nn0cnd 12483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β π β
β) |
182 | | 2ne0 12265 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β
0 |
183 | | divcan2 11829 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ 2 β
β β§ 2 β 0) β (2 Β· (π / 2)) = π) |
184 | 110, 182,
183 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (2
Β· (π / 2)) = π) |
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (2 Β·
(π / 2)) = π) |
186 | 185 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (iβ(2
Β· (π / 2))) =
(iβπ)) |
187 | 180, 186 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β
((iβ2)β(π / 2)) =
(iβπ)) |
188 | 168, 187 | eqtr3id 2787 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (-1β(π / 2)) = (iβπ)) |
189 | | neg1rr 12276 |
. . . . . . . . . . . . . . . . 17
β’ -1 β
β |
190 | | reexpcl 13993 |
. . . . . . . . . . . . . . . . 17
β’ ((-1
β β β§ (π /
2) β β0) β (-1β(π / 2)) β β) |
191 | 189, 178,
190 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (-1β(π / 2)) β
β) |
192 | 188, 191 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ (π / 2) β β€)) β (iβπ) β
β) |
193 | 192 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((π / 2) β β€ β (iβπ) β
β)) |
194 | | 0zd 12519 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 0 β
β€) |
195 | | nnz 12528 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β€) |
196 | 195 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β€) |
197 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β) |
198 | 148 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β0) |
199 | 198 | nn0cnd 12483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β) |
200 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 1 β
β) |
201 | 197, 199,
200 | pnpcan2d 11558 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π + 1) β (π + 1)) = (π β π)) |
202 | | 2t1e2 12324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (2
Β· 1) = 2 |
203 | | df-2 12224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 = (1 +
1) |
204 | 202, 203 | eqtr2i 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (1 + 1) =
(2 Β· 1) |
205 | 204 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((2
Β· π) + (1 + 1)) =
((2 Β· π) + (2
Β· 1)) |
206 | 7 | oveq1i 7371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π + 1) = (((2 Β· π) + 1) + 1) |
207 | 11 | nncnd 12177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(2 Β· π) β
β) |
208 | 207 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2
Β· π) β
β) |
209 | 208, 200,
200 | addassd 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (((2
Β· π) + 1) + 1) = ((2
Β· π) + (1 +
1))) |
210 | 206, 209 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) = ((2 Β· π) + (1 + 1))) |
211 | | 2cnd 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 2 β
β) |
212 | | nncn 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β
β) |
213 | 212 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β) |
214 | 211, 213,
200 | adddid 11187 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2
Β· (π + 1)) = ((2
Β· π) + (2 Β·
1))) |
215 | 205, 210,
214 | 3eqtr4a 2799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) = (2 Β· (π + 1))) |
216 | 215 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π + 1) β (π + 1)) = ((2 Β· (π + 1)) β (π + 1))) |
217 | 201, 216 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) = ((2 Β· (π + 1)) β (π + 1))) |
218 | 217 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) = (((2 Β· (π + 1)) β (π + 1)) / 2)) |
219 | 196 | peano2zd 12618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) β
β€) |
220 | 219 | zcnd 12616 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) β
β) |
221 | | mulcl 11143 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((2
β β β§ (π +
1) β β) β (2 Β· (π + 1)) β β) |
222 | 110, 220,
221 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2
Β· (π + 1)) β
β) |
223 | | peano2cn 11335 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β (π + 1) β
β) |
224 | 199, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) β
β) |
225 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2 β
β β§ 2 β 0)) |
226 | | divsubdir 11857 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((2
Β· (π + 1)) β
β β§ (π + 1)
β β β§ (2 β β β§ 2 β 0)) β (((2 Β·
(π + 1)) β (π + 1)) / 2) = (((2 Β·
(π + 1)) / 2) β
((π + 1) /
2))) |
227 | 222, 224,
225, 226 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (((2
Β· (π + 1)) β
(π + 1)) / 2) = (((2
Β· (π + 1)) / 2)
β ((π + 1) /
2))) |
228 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 2 β
0) |
229 | 220, 211,
228 | divcan3d 11944 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((2
Β· (π + 1)) / 2) =
(π + 1)) |
230 | 229 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (((2
Β· (π + 1)) / 2)
β ((π + 1) / 2)) =
((π + 1) β ((π + 1) / 2))) |
231 | 218, 227,
230 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) = ((π + 1) β ((π + 1) / 2))) |
232 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π + 1) / 2) β
β€) |
233 | 219, 232 | zsubcld 12620 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π + 1) β ((π + 1) / 2)) β
β€) |
234 | 231, 233 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) β β€) |
235 | 144 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) β
β0) |
236 | | nn0re 12430 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π) β β0 β (π β π) β β) |
237 | | nn0ge0 12446 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π) β β0 β 0 β€
(π β π)) |
238 | | divge0 12032 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π) β β β§ 0 β€ (π β π)) β§ (2 β β β§ 0 < 2))
β 0 β€ ((π β
π) / 2)) |
239 | 89, 90, 238 | mpanr12 704 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β π) β β β§ 0 β€ (π β π)) β 0 β€ ((π β π) / 2)) |
240 | 236, 237,
239 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π) β β0 β 0 β€
((π β π) / 2)) |
241 | 235, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 0 β€
((π β π) / 2)) |
242 | 235 | nn0red 12482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) β β) |
243 | 49 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β) |
244 | | peano2re 11336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (π + 1) β
β) |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) β
β) |
246 | 198, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β 0 β€
π) |
247 | 198 | nn0red 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β
β) |
248 | 243, 247 | subge02d 11755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (0 β€
π β (π β π) β€ π)) |
249 | 246, 248 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) β€ π) |
250 | 243 | ltp1d 12093 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π < (π + 1)) |
251 | 242, 243,
245, 249, 250 | lelttrd 11321 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) < (π + 1)) |
252 | 251, 215 | breqtrd 5135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) < (2 Β· (π + 1))) |
253 | 219 | zred 12615 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π + 1) β
β) |
254 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2 β
β β§ 0 < 2)) |
255 | | ltdivmul 12038 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β π) β β β§ (π + 1) β β β§ (2 β β
β§ 0 < 2)) β (((π β π) / 2) < (π + 1) β (π β π) < (2 Β· (π + 1)))) |
256 | 242, 253,
254, 255 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (((π β π) / 2) < (π + 1) β (π β π) < (2 Β· (π + 1)))) |
257 | 252, 256 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) < (π + 1)) |
258 | | zleltp1 12562 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π) / 2) β β€ β§ π β β€) β (((π β π) / 2) β€ π β ((π β π) / 2) < (π + 1))) |
259 | 234, 196,
258 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (((π β π) / 2) β€ π β ((π β π) / 2) < (π + 1))) |
260 | 257, 259 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) β€ π) |
261 | 194, 196,
234, 241, 260 | elfzd 13441 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β π) / 2) β (0...π)) |
262 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = ((π β π) / 2) β (2 Β· π) = (2 Β· ((π β π) / 2))) |
263 | 262 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = ((π β π) / 2) β (π β (2 Β· π)) = (π β (2 Β· ((π β π) / 2)))) |
264 | | ovex 7394 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (2 Β· ((π β π) / 2))) β V |
265 | 263, 133,
264 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π) / 2) β (0...π) β ((π β (0...π) β¦ (π β (2 Β· π)))β((π β π) / 2)) = (π β (2 Β· ((π β π) / 2)))) |
266 | 261, 265 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β (0...π) β¦ (π β (2 Β· π)))β((π β π) / 2)) = (π β (2 Β· ((π β π) / 2)))) |
267 | 235 | nn0cnd 12483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β π) β β) |
268 | 267, 211,
228 | divcan2d 11941 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (2
Β· ((π β π) / 2)) = (π β π)) |
269 | 268 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β (2 Β· ((π β π) / 2))) = (π β (π β π))) |
270 | 197, 199 | nncand 11525 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β (π β (π β π)) = π) |
271 | 266, 269,
270 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β (0...π) β¦ (π β (2 Β· π)))β((π β π) / 2)) = π) |
272 | 137 | ffnd 6673 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(π β (0...π) β¦ (π β (2 Β· π))) Fn (0...π)) |
273 | | fnfvelrn 7035 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (0...π) β¦ (π β (2 Β· π))) Fn (0...π) β§ ((π β π) / 2) β (0...π)) β ((π β (0...π) β¦ (π β (2 Β· π)))β((π β π) / 2)) β ran (π β (0...π) β¦ (π β (2 Β· π)))) |
274 | 272, 261,
273 | syl2an2r 684 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β ((π β (0...π) β¦ (π β (2 Β· π)))β((π β π) / 2)) β ran (π β (0...π) β¦ (π β (2 Β· π)))) |
275 | 271, 274 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ ((π + 1) / 2) β β€)) β π β ran (π β (0...π) β¦ (π β (2 Β· π)))) |
276 | 275 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((π + 1) / 2) β β€ β π β ran (π β (0...π) β¦ (π β (2 Β· π))))) |
277 | 193, 276 | orim12d 964 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((π / 2) β β€ β¨ ((π + 1) / 2) β β€)
β ((iβπ) β
β β¨ π β ran
(π β (0...π) β¦ (π β (2 Β· π)))))) |
278 | 166, 277 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((iβπ) β β β¨ π β ran (π β (0...π) β¦ (π β (2 Β· π))))) |
279 | 278 | orcomd 870 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β ran (π β (0...π) β¦ (π β (2 Β· π))) β¨ (iβπ) β β)) |
280 | 279 | ord 863 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (Β¬ π β ran (π β (0...π) β¦ (π β (2 Β· π))) β (iβπ) β β)) |
281 | 280 | impr 456 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
(π β (0...π) β§ Β¬ π β ran (π β (0...π) β¦ (π β (2 Β· π))))) β (iβπ) β β) |
282 | 162, 281 | sylan2b 595 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β (iβπ) β β) |
283 | 161, 282 | remulcld 11193 |
. . . . . . 7
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)) β β) |
284 | 160, 283 | remulcld 11193 |
. . . . . 6
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))) β β) |
285 | 284 | reim0d 15119 |
. . . . 5
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β ((0...π) β ran (π β (0...π) β¦ (π β (2 Β· π))))) β (ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = 0) |
286 | | fzfid 13887 |
. . . . 5
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(0...π) β
Fin) |
287 | 138, 156,
285, 286 | fsumss 15618 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
Ξ£π β ran (π β (0...π) β¦ (π β (2 Β· π)))(ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = Ξ£π β (0...π)(ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))))) |
288 | | elfznn0 13543 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β β0) |
289 | 288 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β0) |
290 | | nn0mulcl 12457 |
. . . . . . . . . . . . . . . . 17
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
291 | 75, 289, 290 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β0) |
292 | 291 | nn0zd 12533 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β€) |
293 | | bccl 14231 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ (2 Β· π) β
β€) β (πC(2
Β· π)) β
β0) |
294 | 14, 292, 293 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πC(2 Β· π)) β
β0) |
295 | 294 | nn0red 12482 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πC(2 Β· π)) β β) |
296 | | fznn0sub 13482 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β (π β π) β
β0) |
297 | 296 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β π) β
β0) |
298 | | reexpcl 13993 |
. . . . . . . . . . . . . 14
β’ ((-1
β β β§ (π
β π) β
β0) β (-1β(π β π)) β β) |
299 | 189, 297,
298 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (-1β(π β π)) β β) |
300 | 295, 299 | remulcld 11193 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((πC(2 Β· π)) Β· (-1β(π β π))) β β) |
301 | | 2z 12543 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β€ |
302 | | znegcl 12546 |
. . . . . . . . . . . . . . . 16
β’ (2 β
β€ β -2 β β€) |
303 | 301, 302 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ -2 β
β€ |
304 | | rpexpcl 13995 |
. . . . . . . . . . . . . . 15
β’
(((tanβπ΄)
β β+ β§ -2 β β€) β ((tanβπ΄)β-2) β
β+) |
305 | 2, 303, 304 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((tanβπ΄)β-2)
β β+) |
306 | 305 | rpred 12965 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((tanβπ΄)β-2)
β β) |
307 | | reexpcl 13993 |
. . . . . . . . . . . . 13
β’
((((tanβπ΄)β-2) β β β§ π β β0)
β (((tanβπ΄)β-2)βπ) β β) |
308 | 306, 288,
307 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((tanβπ΄)β-2)βπ) β
β) |
309 | 300, 308 | remulcld 11193 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) β β) |
310 | 309 | recnd 11191 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) β β) |
311 | | mulcl 11143 |
. . . . . . . . . 10
β’ ((i
β β β§ (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) β β) β (i Β·
(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) β β) |
312 | 5, 310, 311 | sylancr 588 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β· (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) β β) |
313 | 312 | addlidd 11364 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (0 + (i Β·
(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)))) = (i Β· (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)))) |
314 | 294 | nn0cnd 12483 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πC(2 Β· π)) β β) |
315 | 299 | recnd 11191 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (-1β(π β π)) β β) |
316 | 308 | recnd 11191 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((tanβπ΄)β-2)βπ) β
β) |
317 | 314, 315,
316 | mulassd 11186 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) = ((πC(2 Β· π)) Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ)))) |
318 | 317 | oveq2d 7377 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β· (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) = (i Β· ((πC(2 Β· π)) Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ))))) |
319 | 5 | a1i 11 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β i β
β) |
320 | 315, 316 | mulcld 11183 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ)) β β) |
321 | 319, 314,
320 | mul12d 11372 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β· ((πC(2 Β· π)) Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ)))) = ((πC(2 Β· π)) Β· (i Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ))))) |
322 | 318, 321 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β· (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) = ((πC(2 Β· π)) Β· (i Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ))))) |
323 | | bccmpl 14218 |
. . . . . . . . . 10
β’ ((π β β0
β§ (2 Β· π) β
β€) β (πC(2
Β· π)) = (πC(π β (2 Β· π)))) |
324 | 14, 292, 323 | syl2an2r 684 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (πC(2 Β· π)) = (πC(π β (2 Β· π)))) |
325 | 108 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
326 | 291 | nn0cnd 12483 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β) |
327 | 325, 326 | nncand 11525 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β (π β (2 Β· π))) = (2 Β· π)) |
328 | 327 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) = ((1 / (tanβπ΄))β(2 Β· π))) |
329 | 2 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (tanβπ΄) β
β+) |
330 | 329 | rpcnd 12967 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (tanβπ΄) β
β) |
331 | | expneg 13984 |
. . . . . . . . . . . . . 14
β’
(((tanβπ΄)
β β β§ (2 Β· π) β β0) β
((tanβπ΄)β-(2
Β· π)) = (1 /
((tanβπ΄)β(2
Β· π)))) |
332 | 330, 291,
331 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((tanβπ΄)β-(2 Β· π)) = (1 / ((tanβπ΄)β(2 Β· π)))) |
333 | 289 | nn0cnd 12483 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
334 | | mulneg1 11599 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ π
β β) β (-2 Β· π) = -(2 Β· π)) |
335 | 110, 333,
334 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (-2 Β· π) = -(2 Β· π)) |
336 | 335 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((tanβπ΄)β(-2 Β· π)) = ((tanβπ΄)β-(2 Β· π))) |
337 | 329 | rpne0d 12970 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (tanβπ΄) β 0) |
338 | 330, 337,
292 | exprecd 14068 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((1 / (tanβπ΄))β(2 Β· π)) = (1 / ((tanβπ΄)β(2 Β· π)))) |
339 | 332, 336,
338 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((tanβπ΄)β(-2 Β· π)) = ((1 / (tanβπ΄))β(2 Β· π))) |
340 | 303 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β -2 β
β€) |
341 | 289 | nn0zd 12533 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β€) |
342 | | expmulz 14023 |
. . . . . . . . . . . . 13
β’
((((tanβπ΄)
β β β§ (tanβπ΄) β 0) β§ (-2 β β€ β§
π β β€)) β
((tanβπ΄)β(-2
Β· π)) =
(((tanβπ΄)β-2)βπ)) |
343 | 330, 337,
340, 341, 342 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((tanβπ΄)β(-2 Β· π)) = (((tanβπ΄)β-2)βπ)) |
344 | 328, 339,
343 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) = (((tanβπ΄)β-2)βπ)) |
345 | 7 | oveq1i 7371 |
. . . . . . . . . . . . . . 15
β’ (π β (2 Β· π)) = (((2 Β· π) + 1) β (2 Β· π)) |
346 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β) |
347 | 346 | nncnd 12177 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· π) β
β) |
348 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β 1 β
β) |
349 | 347, 348,
326 | addsubd 11541 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((2 Β· π) + 1) β (2 Β· π)) = (((2 Β· π) β (2 Β· π)) + 1)) |
350 | | 2cnd 12239 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β 2 β
β) |
351 | 212 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β π β β) |
352 | 350, 351,
333 | subdid 11619 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· (π β π)) = ((2 Β· π) β (2 Β· π))) |
353 | 352 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((2 Β· (π β π)) + 1) = (((2 Β· π) β (2 Β· π)) + 1)) |
354 | 349, 353 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((2 Β· π) + 1) β (2 Β· π)) = ((2 Β· (π β π)) + 1)) |
355 | 345, 354 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (π β (2 Β· π)) = ((2 Β· (π β π)) + 1)) |
356 | 355 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ(π β (2 Β· π))) = (iβ((2 Β·
(π β π)) + 1))) |
357 | | nn0mulcl 12457 |
. . . . . . . . . . . . . . 15
β’ ((2
β β0 β§ (π β π) β β0) β (2
Β· (π β π)) β
β0) |
358 | 75, 297, 357 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (2 Β· (π β π)) β
β0) |
359 | | expp1 13983 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ (2 Β· (π β π)) β β0) β
(iβ((2 Β· (π
β π)) + 1)) =
((iβ(2 Β· (π
β π))) Β·
i)) |
360 | 5, 358, 359 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ((2 Β·
(π β π)) + 1)) = ((iβ(2 Β·
(π β π))) Β·
i)) |
361 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β 2 β
β0) |
362 | 319, 297,
361 | expmuld 14063 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ(2 Β·
(π β π))) = ((iβ2)β(π β π))) |
363 | 167 | oveq1i 7371 |
. . . . . . . . . . . . . . 15
β’
((iβ2)β(π
β π)) =
(-1β(π β π)) |
364 | 362, 363 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ(2 Β·
(π β π))) = (-1β(π β π))) |
365 | 364 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((iβ(2 Β·
(π β π))) Β· i) =
((-1β(π β π)) Β· i)) |
366 | 356, 360,
365 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ(π β (2 Β· π))) = ((-1β(π β π)) Β· i)) |
367 | | mulcom 11145 |
. . . . . . . . . . . . 13
β’
(((-1β(π
β π)) β β
β§ i β β) β ((-1β(π β π)) Β· i) = (i Β· (-1β(π β π)))) |
368 | 315, 5, 367 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((-1β(π β π)) Β· i) = (i Β· (-1β(π β π)))) |
369 | 366, 368 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (iβ(π β (2 Β· π))) = (i Β·
(-1β(π β π)))) |
370 | 344, 369 | oveq12d 7379 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (((1 /
(tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))) = ((((tanβπ΄)β-2)βπ) Β· (i Β· (-1β(π β π))))) |
371 | | mulcl 11143 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (-1β(π β π)) β β) β (i Β·
(-1β(π β π))) β
β) |
372 | 5, 315, 371 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β·
(-1β(π β π))) β
β) |
373 | 372, 316 | mulcomd 11184 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((i Β·
(-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) = ((((tanβπ΄)β-2)βπ) Β· (i Β·
(-1β(π β π))))) |
374 | 319, 315,
316 | mulassd 11186 |
. . . . . . . . . 10
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((i Β·
(-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) = (i Β·
((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ)))) |
375 | 370, 373,
374 | 3eqtr2rd 2780 |
. . . . . . . . 9
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (i Β·
((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ))) = (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π))))) |
376 | 324, 375 | oveq12d 7379 |
. . . . . . . 8
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β ((πC(2 Β· π)) Β· (i Β· ((-1β(π β π)) Β· (((tanβπ΄)β-2)βπ)))) = ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))))) |
377 | 313, 322,
376 | 3eqtrd 2777 |
. . . . . . 7
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (0 + (i Β·
(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)))) = ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))))) |
378 | 377 | fveq2d 6850 |
. . . . . 6
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (ββ(0 + (i
Β· (((πC(2 Β·
π)) Β·
(-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))))) = (ββ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π))))))) |
379 | | 0re 11165 |
. . . . . . 7
β’ 0 β
β |
380 | | crim 15009 |
. . . . . . 7
β’ ((0
β β β§ (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) β β) β (ββ(0 +
(i Β· (((πC(2
Β· π)) Β·
(-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))))) = (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
381 | 379, 309,
380 | sylancr 588 |
. . . . . 6
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (ββ(0 + (i
Β· (((πC(2 Β·
π)) Β·
(-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))))) = (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
382 | 378, 381 | eqtr3d 2775 |
. . . . 5
β’ (((π β β β§ π΄ β (0(,)(Ο / 2))) β§
π β (0...π)) β (ββ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))))) = (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
383 | 382 | sumeq2dv 15596 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
Ξ£π β (0...π)(ββ((πC(π β (2 Β· π))) Β· (((1 / (tanβπ΄))β(π β (π β (2 Β· π)))) Β· (iβ(π β (2 Β· π)))))) = Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
384 | 157, 287,
383 | 3eqtr3d 2781 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
Ξ£π β (0...π)(ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
385 | 286, 153 | fsumim 15702 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(ββΞ£π
β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = Ξ£π β (0...π)(ββ((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ))))) |
386 | 305 | rpcnd 12967 |
. . . 4
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((tanβπ΄)β-2)
β β) |
387 | | oveq1 7368 |
. . . . . . 7
β’ (π‘ = ((tanβπ΄)β-2) β (π‘βπ) = (((tanβπ΄)β-2)βπ)) |
388 | 387 | oveq2d 7377 |
. . . . . 6
β’ (π‘ = ((tanβπ΄)β-2) β (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (π‘βπ)) = (((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
389 | 388 | sumeq2sdv 15597 |
. . . . 5
β’ (π‘ = ((tanβπ΄)β-2) β Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (π‘βπ)) = Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
390 | | basel.p |
. . . . 5
β’ π = (π‘ β β β¦ Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (π‘βπ))) |
391 | | sumex 15581 |
. . . . 5
β’
Ξ£π β
(0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ)) β V |
392 | 389, 390,
391 | fvmpt 6952 |
. . . 4
β’
(((tanβπ΄)β-2) β β β (πβ((tanβπ΄)β-2)) = Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
393 | 386, 392 | syl 17 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(πβ((tanβπ΄)β-2)) = Ξ£π β (0...π)(((πC(2 Β· π)) Β· (-1β(π β π))) Β· (((tanβπ΄)β-2)βπ))) |
394 | 384, 385,
393 | 3eqtr4d 2783 |
. 2
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(ββΞ£π
β (0...π)((πCπ) Β· (((1 / (tanβπ΄))β(π β π)) Β· (iβπ)))) = (πβ((tanβπ΄)β-2))) |
395 | 51, 58 | rerpdivcld 12996 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((cosβ(π Β·
π΄)) / ((sinβπ΄)βπ)) β β) |
396 | 53, 58 | rerpdivcld 12996 |
. . 3
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
((sinβ(π Β·
π΄)) / ((sinβπ΄)βπ)) β β) |
397 | 395, 396 | crimd 15126 |
. 2
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(ββ(((cosβ(π Β· π΄)) / ((sinβπ΄)βπ)) + (i Β· ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))))) = ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))) |
398 | 66, 394, 397 | 3eqtr3d 2781 |
1
β’ ((π β β β§ π΄ β (0(,)(Ο / 2))) β
(πβ((tanβπ΄)β-2)) = ((sinβ(π Β· π΄)) / ((sinβπ΄)βπ))) |