let x be Real; ( x > 0 & x <= 1 implies sech2" x = cosh2" (1 / x) )
assume that
A1:
x > 0
and
A2:
x <= 1
; sech2" x = cosh2" (1 / x)
A3:
1 - (x ^2) >= 0
by A1, A2, Th22;
A4:
x ^2 > 0
by A1;
cosh2" (1 / x) =
- (log (number_e,((1 / x) + (sqrt ((1 / (x ^2)) - (1 ^2))))))
by XCMPLX_1:76
.=
- (log (number_e,((1 / x) + (sqrt ((1 - (1 * (x ^2))) / (x ^2))))))
by A4, XCMPLX_1:126
.=
- (log (number_e,((1 / x) + ((sqrt (1 - (x ^2))) / (sqrt (x ^2))))))
by A1, A3, SQUARE_1:30
.=
- (log (number_e,((1 / x) + ((sqrt (1 - (x ^2))) / x))))
by A1, SQUARE_1:22
.=
- (log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)))
;
hence
sech2" x = cosh2" (1 / x)
; verum