Step | Hyp | Ref
| Expression |
1 | | coscl 16014 |
. . . . . . . . . 10
β’ (π΄ β β β
(cosβπ΄) β
β) |
2 | | sqeq0 14031 |
. . . . . . . . . 10
β’
((cosβπ΄)
β β β (((cosβπ΄)β2) = 0 β (cosβπ΄) = 0)) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
β’ (π΄ β β β
(((cosβπ΄)β2) = 0
β (cosβπ΄) =
0)) |
4 | 3 | necon3bid 2985 |
. . . . . . . 8
β’ (π΄ β β β
(((cosβπ΄)β2)
β 0 β (cosβπ΄)
β 0)) |
5 | 4 | biimpar 479 |
. . . . . . 7
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((cosβπ΄)β2) β 0) |
6 | 1 | sqcld 14055 |
. . . . . . . 8
β’ (π΄ β β β
((cosβπ΄)β2)
β β) |
7 | | divid 11847 |
. . . . . . . 8
β’
((((cosβπ΄)β2) β β β§
((cosβπ΄)β2) β
0) β (((cosβπ΄)β2) / ((cosβπ΄)β2)) = 1) |
8 | 6, 7 | sylan 581 |
. . . . . . 7
β’ ((π΄ β β β§
((cosβπ΄)β2) β
0) β (((cosβπ΄)β2) / ((cosβπ΄)β2)) = 1) |
9 | 5, 8 | syldan 592 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (((cosβπ΄)β2) / ((cosβπ΄)β2)) = 1) |
10 | 9 | eqcomd 2739 |
. . . . 5
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β 1 = (((cosβπ΄)β2) / ((cosβπ΄)β2))) |
11 | | tanval 16015 |
. . . . . . 7
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
12 | 11 | oveq1d 7373 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((tanβπ΄)β2) = (((sinβπ΄) / (cosβπ΄))β2)) |
13 | | 2nn0 12435 |
. . . . . . . . . 10
β’ 2 β
β0 |
14 | | sincl 16013 |
. . . . . . . . . . 11
β’ (π΄ β β β
(sinβπ΄) β
β) |
15 | | expdiv 14025 |
. . . . . . . . . . 11
β’
(((sinβπ΄)
β β β§ ((cosβπ΄) β β β§ (cosβπ΄) β 0) β§ 2 β
β0) β (((sinβπ΄) / (cosβπ΄))β2) = (((sinβπ΄)β2) / ((cosβπ΄)β2))) |
16 | 14, 15 | syl3an1 1164 |
. . . . . . . . . 10
β’ ((π΄ β β β§
((cosβπ΄) β
β β§ (cosβπ΄)
β 0) β§ 2 β β0) β (((sinβπ΄) / (cosβπ΄))β2) = (((sinβπ΄)β2) / ((cosβπ΄)β2))) |
17 | 13, 16 | mp3an3 1451 |
. . . . . . . . 9
β’ ((π΄ β β β§
((cosβπ΄) β
β β§ (cosβπ΄)
β 0)) β (((sinβπ΄) / (cosβπ΄))β2) = (((sinβπ΄)β2) / ((cosβπ΄)β2))) |
18 | 17 | 3impb 1116 |
. . . . . . . 8
β’ ((π΄ β β β§
(cosβπ΄) β
β β§ (cosβπ΄)
β 0) β (((sinβπ΄) / (cosβπ΄))β2) = (((sinβπ΄)β2) / ((cosβπ΄)β2))) |
19 | 1, 18 | syl3an2 1165 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β β β§
(cosβπ΄) β 0)
β (((sinβπ΄) /
(cosβπ΄))β2) =
(((sinβπ΄)β2) /
((cosβπ΄)β2))) |
20 | 19 | 3anidm12 1420 |
. . . . . 6
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (((sinβπ΄) /
(cosβπ΄))β2) =
(((sinβπ΄)β2) /
((cosβπ΄)β2))) |
21 | 12, 20 | eqtrd 2773 |
. . . . 5
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((tanβπ΄)β2) = (((sinβπ΄)β2) / ((cosβπ΄)β2))) |
22 | 10, 21 | oveq12d 7376 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (1 + ((tanβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
23 | 14 | sqcld 14055 |
. . . . . . . . . 10
β’ (π΄ β β β
((sinβπ΄)β2)
β β) |
24 | | divdir 11843 |
. . . . . . . . . . 11
β’
((((cosβπ΄)β2) β β β§
((sinβπ΄)β2)
β β β§ (((cosβπ΄)β2) β β β§
((cosβπ΄)β2) β
0)) β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
25 | 6, 24 | syl3an1 1164 |
. . . . . . . . . 10
β’ ((π΄ β β β§
((sinβπ΄)β2)
β β β§ (((cosβπ΄)β2) β β β§
((cosβπ΄)β2) β
0)) β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
26 | 23, 25 | syl3an2 1165 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β β β§
(((cosβπ΄)β2)
β β β§ ((cosβπ΄)β2) β 0)) β
((((cosβπ΄)β2) +
((sinβπ΄)β2)) /
((cosβπ΄)β2)) =
((((cosβπ΄)β2) /
((cosβπ΄)β2)) +
(((sinβπ΄)β2) /
((cosβπ΄)β2)))) |
27 | 26 | 3anidm12 1420 |
. . . . . . . 8
β’ ((π΄ β β β§
(((cosβπ΄)β2)
β β β§ ((cosβπ΄)β2) β 0)) β
((((cosβπ΄)β2) +
((sinβπ΄)β2)) /
((cosβπ΄)β2)) =
((((cosβπ΄)β2) /
((cosβπ΄)β2)) +
(((sinβπ΄)β2) /
((cosβπ΄)β2)))) |
28 | 27 | 3impb 1116 |
. . . . . . 7
β’ ((π΄ β β β§
((cosβπ΄)β2)
β β β§ ((cosβπ΄)β2) β 0) β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
29 | 6, 28 | syl3an2 1165 |
. . . . . 6
β’ ((π΄ β β β§ π΄ β β β§
((cosβπ΄)β2) β
0) β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
30 | 29 | 3anidm12 1420 |
. . . . 5
β’ ((π΄ β β β§
((cosβπ΄)β2) β
0) β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
31 | 5, 30 | syldan 592 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = ((((cosβπ΄)β2) / ((cosβπ΄)β2)) + (((sinβπ΄)β2) / ((cosβπ΄)β2)))) |
32 | 22, 31 | eqtr4d 2776 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (1 + ((tanβπ΄)β2)) = ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2))) |
33 | 23, 6 | addcomd 11362 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
(((cosβπ΄)β2) +
((sinβπ΄)β2))) |
34 | | sincossq 16063 |
. . . . . 6
β’ (π΄ β β β
(((sinβπ΄)β2) +
((cosβπ΄)β2)) =
1) |
35 | 33, 34 | eqtr3d 2775 |
. . . . 5
β’ (π΄ β β β
(((cosβπ΄)β2) +
((sinβπ΄)β2)) =
1) |
36 | 35 | oveq1d 7373 |
. . . 4
β’ (π΄ β β β
((((cosβπ΄)β2) +
((sinβπ΄)β2)) /
((cosβπ΄)β2)) =
(1 / ((cosβπ΄)β2))) |
37 | 36 | adantr 482 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((((cosβπ΄)β2) + ((sinβπ΄)β2)) / ((cosβπ΄)β2)) = (1 / ((cosβπ΄)β2))) |
38 | 32, 37 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (1 + ((tanβπ΄)β2)) = (1 / ((cosβπ΄)β2))) |
39 | | secval 47278 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (secβπ΄) = (1 /
(cosβπ΄))) |
40 | 39 | oveq1d 7373 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((secβπ΄)β2) = ((1 / (cosβπ΄))β2)) |
41 | | ax-1cn 11114 |
. . . . . 6
β’ 1 β
β |
42 | | expdiv 14025 |
. . . . . 6
β’ ((1
β β β§ ((cosβπ΄) β β β§ (cosβπ΄) β 0) β§ 2 β
β0) β ((1 / (cosβπ΄))β2) = ((1β2) / ((cosβπ΄)β2))) |
43 | 41, 13, 42 | mp3an13 1453 |
. . . . 5
β’
(((cosβπ΄)
β β β§ (cosβπ΄) β 0) β ((1 / (cosβπ΄))β2) = ((1β2) /
((cosβπ΄)β2))) |
44 | 1, 43 | sylan 581 |
. . . 4
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((1 / (cosβπ΄))β2) = ((1β2) / ((cosβπ΄)β2))) |
45 | | sq1 14105 |
. . . . 5
β’
(1β2) = 1 |
46 | 45 | oveq1i 7368 |
. . . 4
β’
((1β2) / ((cosβπ΄)β2)) = (1 / ((cosβπ΄)β2)) |
47 | 44, 46 | eqtrdi 2789 |
. . 3
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((1 / (cosβπ΄))β2) = (1 / ((cosβπ΄)β2))) |
48 | 40, 47 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β ((secβπ΄)β2) = (1 / ((cosβπ΄)β2))) |
49 | 38, 48 | eqtr4d 2776 |
1
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (1 + ((tanβπ΄)β2)) = ((secβπ΄)β2)) |