Step | Hyp | Ref
| Expression |
1 | | cotval 46509 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (cotβπ΄) =
((cosβπ΄) /
(sinβπ΄))) |
2 | 1 | oveq1d 7322 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cotβπ΄)β2) = (((cosβπ΄) / (sinβπ΄))β2)) |
3 | 2 | oveq2d 7323 |
. 2
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + ((cotβπ΄)β2)) = (1 + (((cosβπ΄) / (sinβπ΄))β2))) |
4 | | sincossq 15930 |
. . . . 5
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
5 | 4 | oveq1d 7322 |
. . . 4
β’ (π΄ β β β
((((sinβπ΄)β2) +
((cosβπ΄)β2)) /
((sinβπ΄)β2)) =
(1 / ((sinβπ΄)β2))) |
6 | 5 | adantr 482 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((((sinβπ΄)β2) + ((cosβπ΄)β2)) / ((sinβπ΄)β2)) = (1 / ((sinβπ΄)β2))) |
7 | | sincl 15880 |
. . . . . . . 8
β’ (π΄ β β β
(sinβπ΄) β
β) |
8 | 7 | sqcld 13908 |
. . . . . . 7
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((sinβπ΄)β2) β β) |
10 | | sqne0 13889 |
. . . . . . . 8
β’
((sinβπ΄)
β β β (((sinβπ΄)β2) β 0 β (sinβπ΄) β 0)) |
11 | 7, 10 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(((sinβπ΄)β2)
β 0 β (sinβπ΄)
β 0)) |
12 | 11 | biimpar 479 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((sinβπ΄)β2) β 0) |
13 | 9, 12 | dividd 11795 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (((sinβπ΄)β2) / ((sinβπ΄)β2)) = 1) |
14 | 13 | oveq1d 7322 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((((sinβπ΄)β2) / ((sinβπ΄)β2)) + (((cosβπ΄)β2) / ((sinβπ΄)β2))) = (1 + (((cosβπ΄)β2) / ((sinβπ΄)β2)))) |
15 | | coscl 15881 |
. . . . . . 7
β’ (π΄ β β β
(cosβπ΄) β
β) |
16 | 15 | sqcld 13908 |
. . . . . 6
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cosβπ΄)β2) β β) |
18 | 9, 17, 9, 12 | divdird 11835 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((((sinβπ΄)β2) + ((cosβπ΄)β2)) / ((sinβπ΄)β2)) = ((((sinβπ΄)β2) / ((sinβπ΄)β2)) + (((cosβπ΄)β2) / ((sinβπ΄)β2)))) |
19 | 15, 7 | jca 513 |
. . . . . 6
β’ (π΄ β β β
((cosβπ΄) β
β β§ (sinβπ΄)
β β)) |
20 | | 2nn0 12296 |
. . . . . . . 8
β’ 2 β
β0 |
21 | | expdiv 13880 |
. . . . . . . 8
β’
(((cosβπ΄)
β β β§ ((sinβπ΄) β β β§ (sinβπ΄) β 0) β§ 2 β
β0) β (((cosβπ΄) / (sinβπ΄))β2) = (((cosβπ΄)β2) / ((sinβπ΄)β2))) |
22 | 20, 21 | mp3an3 1450 |
. . . . . . 7
β’
(((cosβπ΄)
β β β§ ((sinβπ΄) β β β§ (sinβπ΄) β 0)) β
(((cosβπ΄) /
(sinβπ΄))β2) =
(((cosβπ΄)β2) /
((sinβπ΄)β2))) |
23 | 22 | anassrs 469 |
. . . . . 6
β’
((((cosβπ΄)
β β β§ (sinβπ΄) β β) β§ (sinβπ΄) β 0) β
(((cosβπ΄) /
(sinβπ΄))β2) =
(((cosβπ΄)β2) /
((sinβπ΄)β2))) |
24 | 19, 23 | sylan 581 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (((cosβπ΄) /
(sinβπ΄))β2) =
(((cosβπ΄)β2) /
((sinβπ΄)β2))) |
25 | 24 | oveq2d 7323 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + (((cosβπ΄)
/ (sinβπ΄))β2)) =
(1 + (((cosβπ΄)β2) / ((sinβπ΄)β2)))) |
26 | 14, 18, 25 | 3eqtr4rd 2787 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + (((cosβπ΄)
/ (sinβπ΄))β2)) =
((((sinβπ΄)β2) +
((cosβπ΄)β2)) /
((sinβπ΄)β2))) |
27 | | cscval 46508 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (cscβπ΄) = (1 /
(sinβπ΄))) |
28 | 27 | oveq1d 7322 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = ((1 / (sinβπ΄))β2)) |
29 | | ax-1cn 10975 |
. . . . . . 7
β’ 1 β
β |
30 | | expdiv 13880 |
. . . . . . 7
β’ ((1
β β β§ ((sinβπ΄) β β β§ (sinβπ΄) β 0) β§ 2 β
β0) β ((1 / (sinβπ΄))β2) = ((1β2) / ((sinβπ΄)β2))) |
31 | 29, 20, 30 | mp3an13 1452 |
. . . . . 6
β’
(((sinβπ΄)
β β β§ (sinβπ΄) β 0) β ((1 / (sinβπ΄))β2) = ((1β2) /
((sinβπ΄)β2))) |
32 | 7, 31 | sylan 581 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((1 / (sinβπ΄))β2) = ((1β2) / ((sinβπ΄)β2))) |
33 | | sq1 13958 |
. . . . . 6
β’
(1β2) = 1 |
34 | 33 | oveq1i 7317 |
. . . . 5
β’
((1β2) / ((sinβπ΄)β2)) = (1 / ((sinβπ΄)β2)) |
35 | 32, 34 | eqtrdi 2792 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((1 / (sinβπ΄))β2) = (1 / ((sinβπ΄)β2))) |
36 | 28, 35 | eqtrd 2776 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = (1 / ((sinβπ΄)β2))) |
37 | 6, 26, 36 | 3eqtr4rd 2787 |
. 2
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = (1 + (((cosβπ΄) / (sinβπ΄))β2))) |
38 | 3, 37 | eqtr4d 2779 |
1
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + ((cotβπ΄)β2)) = ((cscβπ΄)β2)) |