Step | Hyp | Ref
| Expression |
1 | | cotval 47794 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (cotβπ΄) =
((cosβπ΄) /
(sinβπ΄))) |
2 | 1 | oveq1d 7424 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cotβπ΄)β2) = (((cosβπ΄) / (sinβπ΄))β2)) |
3 | 2 | oveq2d 7425 |
. 2
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + ((cotβπ΄)β2)) = (1 + (((cosβπ΄) / (sinβπ΄))β2))) |
4 | | sincossq 16119 |
. . . . 5
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
5 | 4 | oveq1d 7424 |
. . . 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 16069 |
. . . . . . . 8
β’ (π΄ β β β
(sinβπ΄) β
β) |
8 | 7 | sqcld 14109 |
. . . . . . 7
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((sinβπ΄)β2) β β) |
10 | | sqne0 14088 |
. . . . . . . 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 11988 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (((sinβπ΄)β2) / ((sinβπ΄)β2)) = 1) |
14 | 13 | oveq1d 7424 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((((sinβπ΄)β2) / ((sinβπ΄)β2)) + (((cosβπ΄)β2) / ((sinβπ΄)β2))) = (1 + (((cosβπ΄)β2) / ((sinβπ΄)β2)))) |
15 | | coscl 16070 |
. . . . . . 7
β’ (π΄ β β β
(cosβπ΄) β
β) |
16 | 15 | sqcld 14109 |
. . . . . 6
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cosβπ΄)β2) β β) |
18 | 9, 17, 9, 12 | divdird 12028 |
. . . 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 12489 |
. . . . . . . 8
β’ 2 β
β0 |
21 | | expdiv 14079 |
. . . . . . . 8
β’
(((cosβπ΄)
β β β§ ((sinβπ΄) β β β§ (sinβπ΄) β 0) β§ 2 β
β0) β (((cosβπ΄) / (sinβπ΄))β2) = (((cosβπ΄)β2) / ((sinβπ΄)β2))) |
22 | 20, 21 | mp3an3 1451 |
. . . . . . 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 7425 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + (((cosβπ΄)
/ (sinβπ΄))β2)) =
(1 + (((cosβπ΄)β2) / ((sinβπ΄)β2)))) |
26 | 14, 18, 25 | 3eqtr4rd 2784 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + (((cosβπ΄)
/ (sinβπ΄))β2)) =
((((sinβπ΄)β2) +
((cosβπ΄)β2)) /
((sinβπ΄)β2))) |
27 | | cscval 47793 |
. . . . 5
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (cscβπ΄) = (1 /
(sinβπ΄))) |
28 | 27 | oveq1d 7424 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = ((1 / (sinβπ΄))β2)) |
29 | | ax-1cn 11168 |
. . . . . . 7
β’ 1 β
β |
30 | | expdiv 14079 |
. . . . . . 7
β’ ((1
β β β§ ((sinβπ΄) β β β§ (sinβπ΄) β 0) β§ 2 β
β0) β ((1 / (sinβπ΄))β2) = ((1β2) / ((sinβπ΄)β2))) |
31 | 29, 20, 30 | mp3an13 1453 |
. . . . . 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 14159 |
. . . . . 6
β’
(1β2) = 1 |
34 | 33 | oveq1i 7419 |
. . . . 5
β’
((1β2) / ((sinβπ΄)β2)) = (1 / ((sinβπ΄)β2)) |
35 | 32, 34 | eqtrdi 2789 |
. . . 4
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((1 / (sinβπ΄))β2) = (1 / ((sinβπ΄)β2))) |
36 | 28, 35 | eqtrd 2773 |
. . 3
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = (1 / ((sinβπ΄)β2))) |
37 | 6, 26, 36 | 3eqtr4rd 2784 |
. 2
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β ((cscβπ΄)β2) = (1 + (((cosβπ΄) / (sinβπ΄))β2))) |
38 | 3, 37 | eqtr4d 2776 |
1
β’ ((π΄ β β β§
(sinβπ΄) β 0)
β (1 + ((cotβπ΄)β2)) = ((cscβπ΄)β2)) |