let x be Real; ( 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 2
.=
- (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:55, TAYLOR_1:11
.=
- (log (number_e,(((sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2))) ^2)))
by POWER:46
.=
- (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 2
.=
- (log (number_e,((((x + 1) / 2) + ((2 * (sqrt ((x + 1) / 2))) * (sqrt ((x - 1) / 2)))) + ((x - 1) / 2))))
by A2, SQUARE_1:def 2
.=
- (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:29
.=
- (log (number_e,(x + ((sqrt (2 ^2)) * (sqrt (((x ^2) - 1) / 4))))))
by SQUARE_1:22
.=
- (log (number_e,(x + (sqrt (4 * (((x ^2) - 1) / 4))))))
by A3, SQUARE_1:29
.=
- (log (number_e,(x + (sqrt ((x ^2) - 1)))))
;
hence
cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2)))
; verum