let x be real number ; ( x >= 1 implies cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2))) )
assume A1:
x >= 1
; cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2)))
then A2:
(x - 1) / 2 >= 0
by Th7;
A3:
((x ^2 ) - 1) / 4 >= 0
by A1, Th9;
A4:
(sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0
by A1, Th10;
2 * (cosh2" (sqrt ((x + 1) / 2))) =
2 * (- (log number_e ,((sqrt ((x + 1) / 2)) + (sqrt (((x + 1) / 2) - 1)))))
by A1, SQUARE_1:def 4
.=
- (2 * (log number_e ,((sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)))))
.=
- (log number_e ,(((sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2))) to_power 2))
by A4, Lm1, POWER:63, TAYLOR_1:11
.=
- (log number_e ,(((sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2))) ^2 ))
by POWER:53
.=
- (log number_e ,((((sqrt ((x + 1) / 2)) ^2 ) + ((2 * (sqrt ((x + 1) / 2))) * (sqrt ((x - 1) / 2)))) + ((sqrt ((x - 1) / 2)) ^2 )))
.=
- (log number_e ,((((x + 1) / 2) + ((2 * (sqrt ((x + 1) / 2))) * (sqrt ((x - 1) / 2)))) + ((sqrt ((x - 1) / 2)) ^2 )))
by A1, SQUARE_1:def 4
.=
- (log number_e ,((((x + 1) / 2) + ((2 * (sqrt ((x + 1) / 2))) * (sqrt ((x - 1) / 2)))) + ((x - 1) / 2)))
by A2, SQUARE_1:def 4
.=
- (log number_e ,(x + (2 * ((sqrt ((x + 1) / 2)) * (sqrt ((x - 1) / 2))))))
.=
- (log number_e ,(x + (2 * (sqrt (((x + 1) / 2) * ((x - 1) / 2))))))
by A1, A2, SQUARE_1:97
.=
- (log number_e ,(x + ((sqrt (2 ^2 )) * (sqrt (((x ^2 ) - 1) / 4)))))
by SQUARE_1:89
.=
- (log number_e ,(x + (sqrt (4 * (((x ^2 ) - 1) / 4)))))
by A3, SQUARE_1:97
.=
- (log number_e ,(x + (sqrt ((x ^2 ) - 1))))
;
hence
cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2)))
; verum