let x be real number ; :: thesis: for n being Element of NAT holds
( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) )
let n be Element of NAT ; :: thesis: ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) )
A1: ((cosh x) + (sinh x)) |^ n = ((cosh . x) + (sinh x)) |^ n by SIN_COS2:def 4
.= ((cosh . x) + (sinh . x)) |^ n by SIN_COS2:def 2
.= (cosh . (n * x)) + (sinh . (n * x)) by SIN_COS2:29
.= (cosh (n * x)) + (sinh . (n * x)) by SIN_COS2:def 4
.= (cosh (n * x)) + (sinh (n * x)) by SIN_COS2:def 2 ;
((cosh x) - (sinh x)) |^ n = ((cosh x) + (- (sinh x))) |^ n
.= ((cosh x) + (sinh (- x))) |^ n by Lm8
.= ((cosh . x) + (sinh (- x))) |^ n by SIN_COS2:def 4
.= ((cosh . x) + (sinh . (- x))) |^ n by SIN_COS2:def 2
.= ((cosh . (- x)) + (sinh . (- x))) |^ n by SIN_COS2:19
.= (cosh . (n * (- x))) + (sinh . (- (n * x))) by SIN_COS2:29
.= (cosh . (n * x)) + (sinh . (- (n * x))) by SIN_COS2:19
.= (cosh . (n * x)) + (- (sinh . (n * x))) by SIN_COS2:19
.= (cosh . (n * x)) - (sinh . (n * x))
.= (cosh (n * x)) - (sinh . (n * x)) by SIN_COS2:def 4
.= (cosh (n * x)) - (sinh (n * x)) by SIN_COS2:def 2 ;
hence ( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) ) by A1; :: thesis: verum