let p be Real; :: thesis: for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
let n be Nat; :: thesis: ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))
defpred S₁[ Nat] means for p being Real holds ((cosh . p) + (sinh . p)) |^ $1 = (cosh . ($1 * p)) + (sinh . ($1 * p));
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: for p being Real holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; :: thesis: S₁[n + 1]
for p being Real holds ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p))

proof

let p be Real; :: thesis: ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p))
A3: ((cosh . (n * p)) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (cosh . p)) + ((sinh . (n * p)) * (sinh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (sinh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (sinh . p)) by Def1
.= ((((exp_R . (n * p)) / 2) + ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) / 2) + ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) / 2) - ((exp_R . (- (n * p))) / 2)) * (((exp_R . p) - (exp_R . (- p))) / 2)) by Def1
.= (2 * (((exp_R . (n * p)) * (exp_R . p)) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2)))
.= (2 * ((exp_R . ((p * n) + (p * 1))) / (2 * 2))) + (2 * (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2))) by Th12
.= (2 * ((exp_R . (p * (n + 1))) / (2 * 2))) + (2 * ((exp_R . ((- (n * p)) + (- p))) / (2 * 2))) by Th12
.= ((exp_R . (p * (n + 1))) + (exp_R . (- (p * (n + 1))))) / 2
.= cosh . (p * (n + 1)) by Def3 ;
A4: ((cosh . (n * p)) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) = ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (sinh . p)) + ((sinh . (n * p)) * (cosh . p)) by Def3
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((sinh . (n * p)) * (cosh . p)) by Def1
.= ((((exp_R . (n * p)) + (exp_R . (- (n * p)))) / 2) * (((exp_R . p) - (exp_R . (- p))) / 2)) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (cosh . p)) by Def1
.= ((((((exp_R . (n * p)) / 2) * ((exp_R . p) / 2)) - (((exp_R . (n * p)) / 2) * ((exp_R . (- p)) / 2))) + (((exp_R . (- (n * p))) / 2) * ((exp_R . p) / 2))) - (((exp_R . (- (n * p))) / 2) * ((exp_R . (- p)) / 2))) + ((((exp_R . (n * p)) - (exp_R . (- (n * p)))) / 2) * (((exp_R . p) + (exp_R . (- p))) / 2)) by Def3
.= (2 * (((exp_R . (n * p)) * (exp_R . p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / (2 * 2))))
.= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- (((exp_R . (- (n * p))) * (exp_R . (- p))) / 4))) by Th12
.= (2 * ((exp_R . ((n * p) + p)) / 4)) + (2 * (- ((exp_R . ((- (n * p)) + (- p))) / 4))) by Th12
.= ((exp_R . (p * (n + 1))) - (exp_R . (- (p * (n + 1))))) / 2
.= sinh . (p * (n + 1)) by Def1 ;
((cosh . p) + (sinh . p)) |^ (n + 1) = (((cosh . p) + (sinh . p)) |^ n) * ((cosh . p) + (sinh . p)) by NEWTON:6
.= ((cosh . (n * p)) + (sinh . (n * p))) * ((cosh . p) + (sinh . p)) by A2
.= (sinh . ((n + 1) * p)) + (cosh . ((n + 1) * p)) by A3, A4 ;
hence ((cosh . p) + (sinh . p)) |^ (n + 1) = (cosh . ((n + 1) * p)) + (sinh . ((n + 1) * p)) ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A5: S₁[ 0 ] by Th15, Th16, NEWTON:4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A1);
hence ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p)) ; :: thesis: verum