Step | Hyp | Ref
| Expression |
1 | | coscl 16072 |
. . . . . 6
β’ (π΄ β β β
(cosβπ΄) β
β) |
2 | 1 | ad2antrr 724 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (cosβπ΄) β
β) |
3 | | coscl 16072 |
. . . . . 6
β’ (π΅ β β β
(cosβπ΅) β
β) |
4 | 3 | ad2antlr 725 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (cosβπ΅) β
β) |
5 | 2, 4 | mulcld 11236 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((cosβπ΄)
Β· (cosβπ΅))
β β) |
6 | | sincl 16071 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) β
β) |
7 | 6 | ad2antrr 724 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (sinβπ΄) β
β) |
8 | | sincl 16071 |
. . . . . 6
β’ (π΅ β β β
(sinβπ΅) β
β) |
9 | 8 | ad2antlr 725 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (sinβπ΅) β
β) |
10 | 7, 9 | mulcld 11236 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((sinβπ΄)
Β· (sinβπ΅))
β β) |
11 | 5, 10 | subeq0ad 11583 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((((cosβπ΄)
Β· (cosβπ΅))
β ((sinβπ΄)
Β· (sinβπ΅))) =
0 β ((cosβπ΄)
Β· (cosβπ΅)) =
((sinβπ΄) Β·
(sinβπ΅)))) |
12 | | cosadd 16110 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(π΄ + π΅)) = (((cosβπ΄) Β· (cosβπ΅)) β ((sinβπ΄) Β· (sinβπ΅)))) |
13 | 12 | adantr 481 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (cosβ(π΄ +
π΅)) = (((cosβπ΄) Β· (cosβπ΅)) β ((sinβπ΄) Β· (sinβπ΅)))) |
14 | 13 | eqeq1d 2734 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((cosβ(π΄ +
π΅)) = 0 β
(((cosβπ΄) Β·
(cosβπ΅)) β
((sinβπ΄) Β·
(sinβπ΅))) =
0)) |
15 | | tanval 16073 |
. . . . . . . 8
β’ ((π΄ β β β§
(cosβπ΄) β 0)
β (tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
16 | 15 | ad2ant2r 745 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (tanβπ΄) =
((sinβπ΄) /
(cosβπ΄))) |
17 | | tanval 16073 |
. . . . . . . 8
β’ ((π΅ β β β§
(cosβπ΅) β 0)
β (tanβπ΅) =
((sinβπ΅) /
(cosβπ΅))) |
18 | 17 | ad2ant2l 744 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (tanβπ΅) =
((sinβπ΅) /
(cosβπ΅))) |
19 | 16, 18 | oveq12d 7429 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((tanβπ΄)
Β· (tanβπ΅)) =
(((sinβπ΄) /
(cosβπ΄)) Β·
((sinβπ΅) /
(cosβπ΅)))) |
20 | | simprl 769 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (cosβπ΄) β
0) |
21 | | simprr 771 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (cosβπ΅) β
0) |
22 | 7, 2, 9, 4, 20, 21 | divmuldivd 12033 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (((sinβπ΄) /
(cosβπ΄)) Β·
((sinβπ΅) /
(cosβπ΅))) =
(((sinβπ΄) Β·
(sinβπ΅)) /
((cosβπ΄) Β·
(cosβπ΅)))) |
23 | 19, 22 | eqtrd 2772 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((tanβπ΄)
Β· (tanβπ΅)) =
(((sinβπ΄) Β·
(sinβπ΅)) /
((cosβπ΄) Β·
(cosβπ΅)))) |
24 | 23 | eqeq1d 2734 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (((tanβπ΄)
Β· (tanβπ΅)) = 1
β (((sinβπ΄)
Β· (sinβπ΅)) /
((cosβπ΄) Β·
(cosβπ΅))) =
1)) |
25 | | 1cnd 11211 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β 1 β β) |
26 | 2, 4, 20, 21 | mulne0d 11868 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((cosβπ΄)
Β· (cosβπ΅))
β 0) |
27 | 10, 5, 25, 26 | divmuld 12014 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((((sinβπ΄)
Β· (sinβπ΅)) /
((cosβπ΄) Β·
(cosβπ΅))) = 1 β
(((cosβπ΄) Β·
(cosβπ΅)) Β· 1)
= ((sinβπ΄) Β·
(sinβπ΅)))) |
28 | 5 | mulridd 11233 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (((cosβπ΄)
Β· (cosβπ΅))
Β· 1) = ((cosβπ΄) Β· (cosβπ΅))) |
29 | 28 | eqeq1d 2734 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((((cosβπ΄)
Β· (cosβπ΅))
Β· 1) = ((sinβπ΄) Β· (sinβπ΅)) β ((cosβπ΄) Β· (cosβπ΅)) = ((sinβπ΄) Β· (sinβπ΅)))) |
30 | 24, 27, 29 | 3bitrd 304 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β (((tanβπ΄)
Β· (tanβπ΅)) = 1
β ((cosβπ΄)
Β· (cosβπ΅)) =
((sinβπ΄) Β·
(sinβπ΅)))) |
31 | 11, 14, 30 | 3bitr4d 310 |
. 2
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((cosβ(π΄ +
π΅)) = 0 β
((tanβπ΄) Β·
(tanβπ΅)) =
1)) |
32 | 31 | necon3bid 2985 |
1
β’ (((π΄ β β β§ π΅ β β) β§
((cosβπ΄) β 0 β§
(cosβπ΅) β 0))
β ((cosβ(π΄ +
π΅)) β 0 β
((tanβπ΄) Β·
(tanβπ΅)) β
1)) |