Step | Hyp | Ref
| Expression |
1 | | sinhval-named 47267 |
. . . . 5
β’ (π΄ β β β
(sinhβπ΄) =
((sinβ(i Β· π΄))
/ i)) |
2 | | sinhval 16041 |
. . . . 5
β’ (π΄ β β β
((sinβ(i Β· π΄))
/ i) = (((expβπ΄)
β (expβ-π΄)) /
2)) |
3 | 1, 2 | eqtrd 2773 |
. . . 4
β’ (π΄ β β β
(sinhβπ΄) =
(((expβπ΄) β
(expβ-π΄)) /
2)) |
4 | | coshval-named 47268 |
. . . . 5
β’ (π΄ β β β
(coshβπ΄) =
(cosβ(i Β· π΄))) |
5 | | coshval 16042 |
. . . . 5
β’ (π΄ β β β
(cosβ(i Β· π΄))
= (((expβπ΄) +
(expβ-π΄)) /
2)) |
6 | 4, 5 | eqtrd 2773 |
. . . 4
β’ (π΄ β β β
(coshβπ΄) =
(((expβπ΄) +
(expβ-π΄)) /
2)) |
7 | 3, 6 | oveq12d 7376 |
. . 3
β’ (π΄ β β β
((sinhβπ΄) +
(coshβπ΄)) =
((((expβπ΄) β
(expβ-π΄)) / 2) +
(((expβπ΄) +
(expβ-π΄)) /
2))) |
8 | | 2cn 12233 |
. . . 4
β’ 2 β
β |
9 | | 2ne0 12262 |
. . . 4
β’ 2 β
0 |
10 | | efcl 15970 |
. . . . . . 7
β’ (π΄ β β β
(expβπ΄) β
β) |
11 | | negcl 11406 |
. . . . . . . 8
β’ (π΄ β β β -π΄ β
β) |
12 | | efcl 15970 |
. . . . . . . 8
β’ (-π΄ β β β
(expβ-π΄) β
β) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(expβ-π΄) β
β) |
14 | 10, 13 | addcld 11179 |
. . . . . 6
β’ (π΄ β β β
((expβπ΄) +
(expβ-π΄)) β
β) |
15 | 10, 13 | subcld 11517 |
. . . . . . 7
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) β
β) |
16 | | divdir 11843 |
. . . . . . 7
β’
((((expβπ΄)
β (expβ-π΄))
β β β§ ((expβπ΄) + (expβ-π΄)) β β β§ (2 β β
β§ 2 β 0)) β ((((expβπ΄) β (expβ-π΄)) + ((expβπ΄) + (expβ-π΄))) / 2) = ((((expβπ΄) β (expβ-π΄)) / 2) + (((expβπ΄) + (expβ-π΄)) / 2))) |
17 | 15, 16 | syl3an1 1164 |
. . . . . 6
β’ ((π΄ β β β§
((expβπ΄) +
(expβ-π΄)) β
β β§ (2 β β β§ 2 β 0)) β ((((expβπ΄) β (expβ-π΄)) + ((expβπ΄) + (expβ-π΄))) / 2) = ((((expβπ΄) β (expβ-π΄)) / 2) + (((expβπ΄) + (expβ-π΄)) / 2))) |
18 | 14, 17 | syl3an2 1165 |
. . . . 5
β’ ((π΄ β β β§ π΄ β β β§ (2 β
β β§ 2 β 0)) β ((((expβπ΄) β (expβ-π΄)) + ((expβπ΄) + (expβ-π΄))) / 2) = ((((expβπ΄) β (expβ-π΄)) / 2) + (((expβπ΄) + (expβ-π΄)) / 2))) |
19 | 18 | 3anidm12 1420 |
. . . 4
β’ ((π΄ β β β§ (2 β
β β§ 2 β 0)) β ((((expβπ΄) β (expβ-π΄)) + ((expβπ΄) + (expβ-π΄))) / 2) = ((((expβπ΄) β (expβ-π΄)) / 2) + (((expβπ΄) + (expβ-π΄)) / 2))) |
20 | 8, 9, 19 | mpanr12 704 |
. . 3
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) +
((expβπ΄) +
(expβ-π΄))) / 2) =
((((expβπ΄) β
(expβ-π΄)) / 2) +
(((expβπ΄) +
(expβ-π΄)) /
2))) |
21 | 10 | 2timesd 12401 |
. . . . 5
β’ (π΄ β β β (2
Β· (expβπ΄)) =
((expβπ΄) +
(expβπ΄))) |
22 | 10, 13, 10 | nppcand 11542 |
. . . . 5
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) +
(expβπ΄)) +
(expβ-π΄)) =
((expβπ΄) +
(expβπ΄))) |
23 | 15, 10, 13 | addassd 11182 |
. . . . 5
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) +
(expβπ΄)) +
(expβ-π΄)) =
(((expβπ΄) β
(expβ-π΄)) +
((expβπ΄) +
(expβ-π΄)))) |
24 | 21, 22, 23 | 3eqtr2rd 2780 |
. . . 4
β’ (π΄ β β β
(((expβπ΄) β
(expβ-π΄)) +
((expβπ΄) +
(expβ-π΄))) = (2
Β· (expβπ΄))) |
25 | 24 | oveq1d 7373 |
. . 3
β’ (π΄ β β β
((((expβπ΄) β
(expβ-π΄)) +
((expβπ΄) +
(expβ-π΄))) / 2) = ((2
Β· (expβπ΄)) /
2)) |
26 | 7, 20, 25 | 3eqtr2d 2779 |
. 2
β’ (π΄ β β β
((sinhβπ΄) +
(coshβπ΄)) = ((2
Β· (expβπ΄)) /
2)) |
27 | 8 | a1i 11 |
. . 3
β’ (π΄ β β β 2 β
β) |
28 | 9 | a1i 11 |
. . 3
β’ (π΄ β β β 2 β
0) |
29 | 10, 27, 28 | divcan3d 11941 |
. 2
β’ (π΄ β β β ((2
Β· (expβπ΄)) /
2) = (expβπ΄)) |
30 | 26, 29 | eqtrd 2773 |
1
β’ (π΄ β β β
((sinhβπ΄) +
(coshβπ΄)) =
(expβπ΄)) |