:: SIN_COS7 semantic presentation begin Lm1: number_e <> 1 by TAYLOR_1:11; Lm2: for x, y being real number st x ^2 < 1 & y < 1 holds (x ^2) * y < 1 proof let x, y be real number ; ::_thesis: ( x ^2 < 1 & y < 1 implies (x ^2) * y < 1 ) assume that A1: x ^2 < 1 and A2: y < 1 ; ::_thesis: (x ^2) * y < 1 percases ( 0 = x ^2 or 0 < x ^2 ) by XREAL_1:63; suppose 0 = x ^2 ; ::_thesis: (x ^2) * y < 1 hence (x ^2) * y < 1 ; ::_thesis: verum end; suppose 0 < x ^2 ; ::_thesis: (x ^2) * y < 1 then y * (x ^2) < 1 * (x ^2) by A2, XREAL_1:68; hence (x ^2) * y < 1 by A1, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th1: :: SIN_COS7:1 for x being real number st x > 0 holds 1 / x = x to_power (- 1) proof let x be real number ; ::_thesis: ( x > 0 implies 1 / x = x to_power (- 1) ) assume x > 0 ; ::_thesis: 1 / x = x to_power (- 1) then x to_power (- 1) = (1 / x) to_power 1 by POWER:32 .= 1 / x by POWER:25 ; hence 1 / x = x to_power (- 1) ; ::_thesis: verum end; theorem :: SIN_COS7:2 for x being real number st x > 1 holds ((sqrt ((x ^2) - 1)) / x) ^2 < 1 proof let x be real number ; ::_thesis: ( x > 1 implies ((sqrt ((x ^2) - 1)) / x) ^2 < 1 ) A1: (- 1) + (x ^2) < 0 + (x ^2) by XREAL_1:6; assume x > 1 ; ::_thesis: ((sqrt ((x ^2) - 1)) / x) ^2 < 1 then x ^2 > (1 ^2) + 0 by SQUARE_1:16; then A2: (x ^2) - 1 > 0 by XREAL_1:20; ((sqrt ((x ^2) - 1)) / x) ^2 = ((sqrt ((x ^2) - 1)) ^2) / (x ^2) by XCMPLX_1:76 .= ((x ^2) - 1) / (x ^2) by A2, SQUARE_1:def_2 ; hence ((sqrt ((x ^2) - 1)) / x) ^2 < 1 by A2, A1, XREAL_1:189; ::_thesis: verum end; theorem :: SIN_COS7:3 for x being real number holds (x / (sqrt ((x ^2) + 1))) ^2 < 1 proof let x be real number ; ::_thesis: (x / (sqrt ((x ^2) + 1))) ^2 < 1 A1: x ^2 < (x ^2) + 1 by XREAL_1:29; A2: x ^2 >= 0 by XREAL_1:63; then (sqrt ((x ^2) + 1)) ^2 = sqrt (((x ^2) + 1) ^2) by SQUARE_1:29 .= (x ^2) + 1 by A2, SQUARE_1:22 ; then A3: (x / (sqrt ((x ^2) + 1))) ^2 = (x ^2) / ((x ^2) + 1) by XCMPLX_1:76; percases ( x ^2 > 0 or x ^2 = 0 ) by XREAL_1:63; suppose x ^2 > 0 ; ::_thesis: (x / (sqrt ((x ^2) + 1))) ^2 < 1 hence (x / (sqrt ((x ^2) + 1))) ^2 < 1 by A1, A3, XREAL_1:189; ::_thesis: verum end; suppose x ^2 = 0 ; ::_thesis: (x / (sqrt ((x ^2) + 1))) ^2 < 1 hence (x / (sqrt ((x ^2) + 1))) ^2 < 1 by A3; ::_thesis: verum end; end; end; theorem Th4: :: SIN_COS7:4 for x being real number holds sqrt ((x ^2) + 1) > 0 proof let x be real number ; ::_thesis: sqrt ((x ^2) + 1) > 0 x ^2 >= 0 by XREAL_1:63; hence sqrt ((x ^2) + 1) > 0 by SQUARE_1:25; ::_thesis: verum end; theorem Th5: :: SIN_COS7:5 for x being real number holds (sqrt ((x ^2) + 1)) + x > 0 proof let x be real number ; ::_thesis: (sqrt ((x ^2) + 1)) + x > 0 percases ( x > 0 or x <= 0 ) ; suppose x > 0 ; ::_thesis: (sqrt ((x ^2) + 1)) + x > 0 hence (sqrt ((x ^2) + 1)) + x > 0 by Th4, XREAL_1:29; ::_thesis: verum end; supposeA1: x <= 0 ; ::_thesis: (sqrt ((x ^2) + 1)) + x > 0 x ^2 < (x ^2) + 1 by XREAL_1:29; then sqrt (x ^2) < sqrt ((x ^2) + 1) by SQUARE_1:27, XREAL_1:63; then - x < sqrt ((x ^2) + 1) by A1, SQUARE_1:23; hence (sqrt ((x ^2) + 1)) + x > 0 by XREAL_1:62; ::_thesis: verum end; end; end; Lm3: for x being real number st 1 <= x holds (x ^2) - 1 >= 0 proof let x be real number ; ::_thesis: ( 1 <= x implies (x ^2) - 1 >= 0 ) assume 1 <= x ; ::_thesis: (x ^2) - 1 >= 0 then x ^2 >= 1 ^2 by SQUARE_1:15; then 1 + (- 1) <= (x ^2) + (- 1) by XREAL_1:6; hence (x ^2) - 1 >= 0 ; ::_thesis: verum end; theorem :: SIN_COS7:6 for y, x being real number st y >= 0 & x >= 1 holds (x + 1) / y >= 0 ; theorem Th7: :: SIN_COS7:7 for y, x being real number st y >= 0 & x >= 1 holds (x - 1) / y >= 0 proof let y, x be real number ; ::_thesis: ( y >= 0 & x >= 1 implies (x - 1) / y >= 0 ) assume that A1: y >= 0 and A2: x >= 1 ; ::_thesis: (x - 1) / y >= 0 x + (- 1) >= 1 + (- 1) by A2, XREAL_1:6; hence (x - 1) / y >= 0 by A1; ::_thesis: verum end; theorem Th8: :: SIN_COS7:8 for x being real number st x >= 1 holds sqrt ((x + 1) / 2) >= 1 proof let x be real number ; ::_thesis: ( x >= 1 implies sqrt ((x + 1) / 2) >= 1 ) assume x >= 1 ; ::_thesis: sqrt ((x + 1) / 2) >= 1 then x + 1 >= 1 + 1 by XREAL_1:6; then (x + 1) / 2 >= 1 by XREAL_1:181; hence sqrt ((x + 1) / 2) >= 1 by SQUARE_1:18, SQUARE_1:26; ::_thesis: verum end; theorem Th9: :: SIN_COS7:9 for y, x being real number st y >= 0 & x >= 1 holds ((x ^2) - 1) / y >= 0 proof let y, x be real number ; ::_thesis: ( y >= 0 & x >= 1 implies ((x ^2) - 1) / y >= 0 ) assume that A1: y >= 0 and A2: x >= 1 ; ::_thesis: ((x ^2) - 1) / y >= 0 (x ^2) - 1 >= 0 by A2, Lm3; hence ((x ^2) - 1) / y >= 0 by A1; ::_thesis: verum end; theorem Th10: :: SIN_COS7:10 for x being real number st x >= 1 holds (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 proof let x be real number ; ::_thesis: ( x >= 1 implies (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 ) assume A1: x >= 1 ; ::_thesis: (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 then (x - 1) / 2 >= 0 by Th7; then A2: sqrt ((x - 1) / 2) >= 0 by SQUARE_1:17, SQUARE_1:26; sqrt ((x + 1) / 2) >= 1 by A1, Th8; hence (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 by A2; ::_thesis: verum end; theorem Th11: :: SIN_COS7:11 for x being real number st x ^2 < 1 holds ( x + 1 > 0 & 1 - x > 0 ) proof let x be real number ; ::_thesis: ( x ^2 < 1 implies ( x + 1 > 0 & 1 - x > 0 ) ) assume x ^2 < 1 ; ::_thesis: ( x + 1 > 0 & 1 - x > 0 ) then ( - 1 < x & x < 1 ) by SQUARE_1:52; hence ( x + 1 > 0 & 1 - x > 0 ) by XREAL_1:148, XREAL_1:149; ::_thesis: verum end; Lm4: for x being real number st x ^2 < 1 holds (x + 1) / (1 - x) > 0 proof let x be real number ; ::_thesis: ( x ^2 < 1 implies (x + 1) / (1 - x) > 0 ) assume x ^2 < 1 ; ::_thesis: (x + 1) / (1 - x) > 0 then ( x + 1 > 0 & 1 - x > 0 ) by Th11; hence (x + 1) / (1 - x) > 0 by XREAL_1:139; ::_thesis: verum end; theorem Th12: :: SIN_COS7:12 for x being real number st x <> 1 holds (1 - x) ^2 > 0 proof let x be real number ; ::_thesis: ( x <> 1 implies (1 - x) ^2 > 0 ) assume x <> 1 ; ::_thesis: (1 - x) ^2 > 0 then 0 <> 1 - x ; hence (1 - x) ^2 > 0 by SQUARE_1:12; ::_thesis: verum end; theorem Th13: :: SIN_COS7:13 for x being real number st x ^2 < 1 holds ((x ^2) + 1) / (1 - (x ^2)) >= 0 proof let x be real number ; ::_thesis: ( x ^2 < 1 implies ((x ^2) + 1) / (1 - (x ^2)) >= 0 ) assume x ^2 < 1 ; ::_thesis: ((x ^2) + 1) / (1 - (x ^2)) >= 0 then A1: 0 < 1 - (x ^2) by XREAL_1:50; x ^2 >= 0 by XREAL_1:63; hence ((x ^2) + 1) / (1 - (x ^2)) >= 0 by A1; ::_thesis: verum end; theorem :: SIN_COS7:14 for x being real number st x ^2 < 1 holds ((2 * x) / (1 + (x ^2))) ^2 < 1 proof let x be real number ; ::_thesis: ( x ^2 < 1 implies ((2 * x) / (1 + (x ^2))) ^2 < 1 ) assume x ^2 < 1 ; ::_thesis: ((2 * x) / (1 + (x ^2))) ^2 < 1 then (x ^2) + (- 1) < 1 + (- 1) by XREAL_1:8; then ((x ^2) - 1) * ((x ^2) - 1) > 0 * ((x ^2) - 1) by XREAL_1:69; then A1: ( x ^2 >= 0 & ((((x ^2) ^2) - (2 * (x ^2))) + 1) + (4 * (x ^2)) > 0 + (4 * (x ^2)) ) by XREAL_1:8, XREAL_1:63; ((2 * x) / (1 + (x ^2))) ^2 = ((2 * x) ^2) / ((1 + (x ^2)) ^2) by XCMPLX_1:76 .= (4 * (x ^2)) / ((((x ^2) ^2) + (2 * (x ^2))) + 1) ; hence ((2 * x) / (1 + (x ^2))) ^2 < 1 by A1, XREAL_1:189; ::_thesis: verum end; theorem Th15: :: SIN_COS7:15 for x being real number st 0 < x & x < 1 holds (1 + x) / (1 - x) > 0 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies (1 + x) / (1 - x) > 0 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: (1 + x) / (1 - x) > 0 x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; hence (1 + x) / (1 - x) > 0 by Lm4; ::_thesis: verum end; theorem :: SIN_COS7:16 for x being real number st 0 < x & x < 1 holds x ^2 < 1 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies x ^2 < 1 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: x ^2 < 1 x ^2 < x by A1, A2, SQUARE_1:13; hence x ^2 < 1 by A2, XXREAL_0:2; ::_thesis: verum end; Lm5: for x being real number st 0 < x & x < 1 holds 0 < 1 - (x ^2) proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies 0 < 1 - (x ^2) ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: 0 < 1 - (x ^2) x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; then (x ^2) - (x ^2) < 1 - (x ^2) by XREAL_1:9; hence 0 < 1 - (x ^2) ; ::_thesis: verum end; theorem :: SIN_COS7:17 for x being real number st 0 < x & x < 1 holds 1 / (sqrt (1 - (x ^2))) > 1 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies 1 / (sqrt (1 - (x ^2))) > 1 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: 1 / (sqrt (1 - (x ^2))) > 1 A3: 0 < 1 - (x ^2) by A1, A2, Lm5; then A4: 0 < sqrt (1 - (x ^2)) by SQUARE_1:25; x * x > 0 * x by A1, XREAL_1:68; then (x ^2) * (- 1) < 0 * (- 1) by XREAL_1:69; then (- (x ^2)) + 1 < 0 + 1 by XREAL_1:8; then sqrt (1 - (x ^2)) < 1 by A3, SQUARE_1:18, SQUARE_1:27; hence 1 / (sqrt (1 - (x ^2))) > 1 by A4, XREAL_1:187; ::_thesis: verum end; theorem Th18: :: SIN_COS7:18 for x being real number st 0 < x & x < 1 holds (2 * x) / (1 - (x ^2)) > 0 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies (2 * x) / (1 - (x ^2)) > 0 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: (2 * x) / (1 - (x ^2)) > 0 x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; then A3: (x ^2) + (- (x ^2)) < 1 + (- (x ^2)) by XREAL_1:8; 0 * 2 < x * 2 by A1, XREAL_1:68; hence (2 * x) / (1 - (x ^2)) > 0 by A3, XREAL_1:139; ::_thesis: verum end; theorem Th19: :: SIN_COS7:19 for x being real number st 0 < x & x < 1 holds 0 < (1 - (x ^2)) ^2 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies 0 < (1 - (x ^2)) ^2 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: 0 < (1 - (x ^2)) ^2 x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; then (x ^2) + (- (x ^2)) < 1 + (- (x ^2)) by XREAL_1:8; hence 0 < (1 - (x ^2)) ^2 by SQUARE_1:12; ::_thesis: verum end; theorem :: SIN_COS7:20 for x being real number st 0 < x & x < 1 holds (1 + (x ^2)) / (1 - (x ^2)) > 1 proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies (1 + (x ^2)) / (1 - (x ^2)) > 1 ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: (1 + (x ^2)) / (1 - (x ^2)) > 1 x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; then A3: (x ^2) + (- (x ^2)) < 1 + (- (x ^2)) by XREAL_1:8; 0 * x < x * x by A1, XREAL_1:68; then (- (x ^2)) + 1 < (x ^2) + 1 by XREAL_1:8; hence (1 + (x ^2)) / (1 - (x ^2)) > 1 by A3, XREAL_1:187; ::_thesis: verum end; theorem :: SIN_COS7:21 for x being real number st 1 < x ^2 holds (1 / x) ^2 < 1 proof let x be real number ; ::_thesis: ( 1 < x ^2 implies (1 / x) ^2 < 1 ) assume A1: 1 < x ^2 ; ::_thesis: (1 / x) ^2 < 1 then 1 / (x ^2) < (x ^2) / (x ^2) by XREAL_1:74; then (1 ^2) / (x ^2) < 1 by A1, XCMPLX_1:60; hence (1 / x) ^2 < 1 by XCMPLX_1:76; ::_thesis: verum end; theorem Th22: :: SIN_COS7:22 for x being real number st 0 < x & x <= 1 holds 1 - (x ^2) >= 0 proof let x be real number ; ::_thesis: ( 0 < x & x <= 1 implies 1 - (x ^2) >= 0 ) assume that A1: 0 < x and A2: x <= 1 ; ::_thesis: 1 - (x ^2) >= 0 A3: x - 1 <= 1 - 1 by A2, XREAL_1:9; percases ( x - 1 < 0 or x - 1 = 0 ) by A3; suppose x - 1 < 0 ; ::_thesis: 1 - (x ^2) >= 0 then (x - 1) + 1 < 0 + 1 by XREAL_1:8; hence 1 - (x ^2) >= 0 by A1, Lm5; ::_thesis: verum end; suppose x - 1 = 0 ; ::_thesis: 1 - (x ^2) >= 0 hence 1 - (x ^2) >= 0 ; ::_thesis: verum end; end; end; theorem Th23: :: SIN_COS7:23 for x being real number st 1 <= x holds 0 < x + (sqrt ((x ^2) - 1)) proof let x be real number ; ::_thesis: ( 1 <= x implies 0 < x + (sqrt ((x ^2) - 1)) ) assume A1: 1 <= x ; ::_thesis: 0 < x + (sqrt ((x ^2) - 1)) then (x ^2) - 1 >= 0 by Lm3; then 0 <= sqrt ((x ^2) - 1) by SQUARE_1:def_2; hence 0 < x + (sqrt ((x ^2) - 1)) by A1; ::_thesis: verum end; theorem Th24: :: SIN_COS7:24 for x, y being real number st 1 <= x & 1 <= y holds 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y implies 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) ) assume that A1: 1 <= x and A2: 1 <= y ; ::_thesis: 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) 0 <= (y ^2) - 1 by A2, Lm3; then A3: 0 <= sqrt ((y ^2) - 1) by SQUARE_1:def_2; 0 <= (x ^2) - 1 by A1, Lm3; then 0 <= sqrt ((x ^2) - 1) by SQUARE_1:def_2; hence 0 <= (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) by A1, A2, A3; ::_thesis: verum end; theorem Th25: :: SIN_COS7:25 for y being real number st 1 <= y holds 0 < y - (sqrt ((y ^2) - 1)) proof let y be real number ; ::_thesis: ( 1 <= y implies 0 < y - (sqrt ((y ^2) - 1)) ) assume A1: 1 <= y ; ::_thesis: 0 < y - (sqrt ((y ^2) - 1)) then 1 * y <= y * y by XREAL_1:64; then 1 <= y ^2 by A1, XXREAL_0:2; then A2: 1 - 1 <= (y ^2) - 1 by XREAL_1:13; (- 1) + (y ^2) < 0 + (y ^2) by XREAL_1:8; then sqrt ((y ^2) - 1) < sqrt (y ^2) by A2, SQUARE_1:27; then sqrt ((y ^2) - 1) < y by A1, SQUARE_1:22; then (sqrt ((y ^2) - 1)) - (sqrt ((y ^2) - 1)) < y - (sqrt ((y ^2) - 1)) by XREAL_1:14; hence 0 < y - (sqrt ((y ^2) - 1)) ; ::_thesis: verum end; theorem Th26: :: SIN_COS7:26 for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) ) assume that A1: 1 <= x and A2: 1 <= y and A3: abs y <= abs x ; ::_thesis: 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) A4: 0 <= (y ^2) - 1 by A2, Lm3; A5: ( (abs x) ^2 = x ^2 & (abs y) ^2 = y ^2 ) by COMPLEX1:75; 1 <= abs y by A2, ABSVALUE:def_1; then y ^2 <= x ^2 by A3, A5, SQUARE_1:15; then (- 1) * (x ^2) <= (- 1) * (y ^2) by XREAL_1:65; then (- (x ^2)) + ((x ^2) * (y ^2)) <= (- (y ^2)) + ((x ^2) * (y ^2)) by XREAL_1:6; then ( 0 <= x ^2 & sqrt ((x ^2) * ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1)) ) by A1, A4, SQUARE_1:26; then (sqrt (x ^2)) * (sqrt ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1)) by A4, SQUARE_1:29; then A6: x * (sqrt ((y ^2) - 1)) <= sqrt ((y ^2) * ((x ^2) - 1)) by A1, SQUARE_1:22; ( 0 <= y ^2 & 0 <= (x ^2) - 1 ) by A1, Lm3, XREAL_1:63; then x * (sqrt ((y ^2) - 1)) <= (sqrt (y ^2)) * (sqrt ((x ^2) - 1)) by A6, SQUARE_1:29; then x * (sqrt ((y ^2) - 1)) <= y * (sqrt ((x ^2) - 1)) by A2, SQUARE_1:22; then (x * (sqrt ((y ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) by XREAL_1:13; hence 0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) ; ::_thesis: verum end; theorem Th27: :: SIN_COS7:27 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds x * y <> - 1 proof let x, y be real number ; ::_thesis: ( x ^2 < 1 & y ^2 < 1 implies x * y <> - 1 ) assume A1: ( x ^2 < 1 & y ^2 < 1 ) ; ::_thesis: x * y <> - 1 assume x * y = - 1 ; ::_thesis: contradiction then (x * y) * (x * y) = 1 ; then (x * x) * (y * y) = 1 ; hence contradiction by A1, Lm2; ::_thesis: verum end; theorem Th28: :: SIN_COS7:28 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds x * y <> 1 proof let x, y be real number ; ::_thesis: ( x ^2 < 1 & y ^2 < 1 implies x * y <> 1 ) assume A1: ( x ^2 < 1 & y ^2 < 1 ) ; ::_thesis: x * y <> 1 assume x * y = 1 ; ::_thesis: contradiction then (x * y) * (x * y) = 1 ; then (x * x) * (y * y) = 1 ; hence contradiction by A1, Lm2; ::_thesis: verum end; theorem Th29: :: SIN_COS7:29 for x being real number st x <> 0 holds exp_R x <> 1 proof let x be real number ; ::_thesis: ( x <> 0 implies exp_R x <> 1 ) assume A1: x <> 0 ; ::_thesis: exp_R x <> 1 assume A2: exp_R x = 1 ; ::_thesis: contradiction x = log (number_e,(exp_R x)) by TAYLOR_1:12 .= 0 by A2, Lm1, POWER:51, TAYLOR_1:11 ; hence contradiction by A1; ::_thesis: verum end; theorem Th30: :: SIN_COS7:30 for x being real number st 0 <> x holds ((exp_R x) ^2) - 1 <> 0 proof let x be real number ; ::_thesis: ( 0 <> x implies ((exp_R x) ^2) - 1 <> 0 ) assume A1: 0 <> x ; ::_thesis: ((exp_R x) ^2) - 1 <> 0 assume ((exp_R x) ^2) - 1 = 0 ; ::_thesis: contradiction then ( exp_R x = 1 or exp_R x = - 1 ) by XCMPLX_1:182; hence contradiction by A1, Th29, SIN_COS:55; ::_thesis: verum end; Lm6: for x being real number holds (x ^2) + 1 > 0 proof let x be real number ; ::_thesis: (x ^2) + 1 > 0 x ^2 >= 0 by XREAL_1:63; hence (x ^2) + 1 > 0 ; ::_thesis: verum end; theorem Th31: :: SIN_COS7:31 for t being real number holds ((t ^2) - 1) / ((t ^2) + 1) < 1 proof let t be real number ; ::_thesis: ((t ^2) - 1) / ((t ^2) + 1) < 1 A1: 0 < (t ^2) + 1 by Lm6; (- 1) + (t ^2) < 1 + (t ^2) by XREAL_1:8; then ((- 1) + (t ^2)) / (1 + (t ^2)) < (1 + (t ^2)) / (1 + (t ^2)) by A1, XREAL_1:74; hence ((t ^2) - 1) / ((t ^2) + 1) < 1 by A1, XCMPLX_1:60; ::_thesis: verum end; theorem Th32: :: SIN_COS7:32 for t being real number st - 1 < t & t < 1 holds 0 < (t + 1) / (1 - t) proof let t be real number ; ::_thesis: ( - 1 < t & t < 1 implies 0 < (t + 1) / (1 - t) ) assume ( - 1 < t & t < 1 ) ; ::_thesis: 0 < (t + 1) / (1 - t) then ( (- 1) + 1 < t + 1 & t - t < 1 - t ) by XREAL_1:8; then 0 / (1 - t) < (t + 1) / (1 - t) by XREAL_1:74; hence 0 < (t + 1) / (1 - t) ; ::_thesis: verum end; Lm7: for t being real number st ( 1 < t or t < - 1 ) holds 0 < (t + 1) / (t - 1) proof let t be real number ; ::_thesis: ( ( 1 < t or t < - 1 ) implies 0 < (t + 1) / (t - 1) ) assume A1: ( 1 < t or t < - 1 ) ; ::_thesis: 0 < (t + 1) / (t - 1) percases ( 1 < t or t < - 1 ) by A1; supposeA2: 1 < t ; ::_thesis: 0 < (t + 1) / (t - 1) then 1 - 1 < t - 1 by XREAL_1:14; then 0 / (t - 1) < (t + 1) / (t - 1) by A2, XREAL_1:74; hence 0 < (t + 1) / (t - 1) ; ::_thesis: verum end; supposeA3: t < - 1 ; ::_thesis: 0 < (t + 1) / (t - 1) then t + 1 < (- 1) + 1 by XREAL_1:8; then 0 / (t - 1) < (t + 1) / (t - 1) by A3, XREAL_1:75; hence 0 < (t + 1) / (t - 1) ; ::_thesis: verum end; end; end; Lm8: for x being real number holds sqrt ((x ^2) + 1) > x proof let x be real number ; ::_thesis: sqrt ((x ^2) + 1) > x percases ( x >= 0 or x < 0 ) ; supposeA1: x >= 0 ; ::_thesis: sqrt ((x ^2) + 1) > x (x ^2) + 1 > (x ^2) + 0 by XREAL_1:8; then sqrt ((x ^2) + 1) > sqrt (x ^2) by SQUARE_1:27, XREAL_1:63; hence sqrt ((x ^2) + 1) > x by A1, SQUARE_1:22; ::_thesis: verum end; suppose x < 0 ; ::_thesis: sqrt ((x ^2) + 1) > x hence sqrt ((x ^2) + 1) > x by Th4; ::_thesis: verum end; end; end; Lm9: for x, y being real number holds ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0 proof let x, y be real number ; ::_thesis: ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) > 0 A1: (y ^2) + 1 > 0 by Lm6; assume ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) <= 0 ; ::_thesis: contradiction then A2: (sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)) <= x * y by XREAL_1:50; ( sqrt ((x ^2) + 1) > 0 & sqrt ((y ^2) + 1) > 0 ) by Th4; then ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) ^2 <= (x * y) ^2 by A2, SQUARE_1:15; then A3: ((sqrt ((x ^2) + 1)) ^2) * ((sqrt ((y ^2) + 1)) ^2) <= (x * y) ^2 ; (x ^2) + 1 > 0 by Lm6; then ((x ^2) + 1) * ((sqrt ((y ^2) + 1)) ^2) <= (x * y) ^2 by A3, SQUARE_1:def_2; then ((x ^2) + 1) * ((y ^2) + 1) <= (x * y) ^2 by A1, SQUARE_1:def_2; then A4: (((((x * y) ^2) + (x ^2)) + (y ^2)) + 1) - ((x * y) ^2) <= ((x * y) ^2) - ((x * y) ^2) by XREAL_1:13; ( 0 <= x ^2 & 0 <= y ^2 ) by XREAL_1:63; then 0 + 1 <= ((x ^2) + (y ^2)) + 1 by XREAL_1:6; hence contradiction by A4; ::_thesis: verum end; Lm10: for y being real number st 1 <= y holds y + (sqrt ((y ^2) - 1)) > 0 proof let y be real number ; ::_thesis: ( 1 <= y implies y + (sqrt ((y ^2) - 1)) > 0 ) assume A1: 1 <= y ; ::_thesis: y + (sqrt ((y ^2) - 1)) > 0 then 0 <= (y ^2) - 1 by Lm3; then 0 <= sqrt ((y ^2) - 1) by SQUARE_1:def_2; hence y + (sqrt ((y ^2) - 1)) > 0 by A1; ::_thesis: verum end; Lm11: for t being real number st 0 < t holds - 1 < ((t ^2) - 1) / ((t ^2) + 1) proof let t be real number ; ::_thesis: ( 0 < t implies - 1 < ((t ^2) - 1) / ((t ^2) + 1) ) A1: 0 < (t ^2) + 1 by Lm6; assume 0 < t ; ::_thesis: - 1 < ((t ^2) - 1) / ((t ^2) + 1) then 0 < t ^2 by SQUARE_1:12; then 0 * 2 < 2 * (t ^2) by XREAL_1:68; then 0 - ((t ^2) + 1) < (2 * (t ^2)) - ((t ^2) + 1) by XREAL_1:14; then (- ((t ^2) + 1)) / ((t ^2) + 1) < ((t ^2) - 1) / ((t ^2) + 1) by A1, XREAL_1:74; then - (((t ^2) + 1) / ((t ^2) + 1)) < ((t ^2) - 1) / ((t ^2) + 1) ; hence - 1 < ((t ^2) - 1) / ((t ^2) + 1) by A1, XCMPLX_1:60; ::_thesis: verum end; Lm12: for t being real number st 0 < t & t <> 1 & not 1 < ((t ^2) + 1) / ((t ^2) - 1) holds ((t ^2) + 1) / ((t ^2) - 1) < - 1 proof let t be real number ; ::_thesis: ( 0 < t & t <> 1 & not 1 < ((t ^2) + 1) / ((t ^2) - 1) implies ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) assume that A1: 0 < t and A2: t <> 1 ; ::_thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) ( 1 < t or t < 1 ) by A2, XXREAL_0:1; then A3: ( 1 - 1 < t - 1 or t - 1 < 1 - 1 ) by XREAL_1:14; percases ( 0 < t - 1 or t - 1 < 0 ) by A3; suppose 0 < t - 1 ; ::_thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) then A4: 0 + 1 < (t - 1) + 1 by XREAL_1:8; then t < t ^2 by SQUARE_1:14; then 1 < t ^2 by A4, XXREAL_0:2; then A5: 1 - 1 < (t ^2) - 1 by XREAL_1:14; (- 1) + (t ^2) < 1 + (t ^2) by XREAL_1:8; hence ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) by A5, XREAL_1:187; ::_thesis: verum end; suppose t - 1 < 0 ; ::_thesis: ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) then A6: (t - 1) + 1 < 0 + 1 by XREAL_1:8; then t ^2 < t by A1, SQUARE_1:13; then t ^2 < 1 by A6, XXREAL_0:2; then A7: (t ^2) - (t ^2) < 1 - (t ^2) by XREAL_1:14; 0 < t ^2 by A1, SQUARE_1:12; then (- (t ^2)) + 1 < (t ^2) + 1 by XREAL_1:8; then 1 < ((t ^2) + 1) / (1 - (t ^2)) by A7, XREAL_1:187; then (- 1) * (((t ^2) + 1) / (1 - (t ^2))) < 1 * (- 1) by XREAL_1:69; then (- ((t ^2) + 1)) / (1 - (t ^2)) < 1 * (- 1) ; then ((t ^2) + 1) / (- (1 - (t ^2))) < 1 * (- 1) by XCMPLX_1:192; hence ( 1 < ((t ^2) + 1) / ((t ^2) - 1) or ((t ^2) + 1) / ((t ^2) - 1) < - 1 ) ; ::_thesis: verum end; end; end; Lm13: for t being real number st 0 < t holds 0 < (2 * t) / (1 + (t ^2)) proof let t be real number ; ::_thesis: ( 0 < t implies 0 < (2 * t) / (1 + (t ^2)) ) assume 0 < t ; ::_thesis: 0 < (2 * t) / (1 + (t ^2)) then A1: 0 * 2 < 2 * t by XREAL_1:68; (t ^2) + 1 > 0 by Lm6; then 0 / ((t ^2) + 1) < (2 * t) / ((t ^2) + 1) by A1, XREAL_1:74; hence 0 < (2 * t) / (1 + (t ^2)) ; ::_thesis: verum end; Lm14: for t being real number st 0 < t holds (2 * t) / (1 + (t ^2)) <= 1 proof let t be real number ; ::_thesis: ( 0 < t implies (2 * t) / (1 + (t ^2)) <= 1 ) 0 <= (t - 1) ^2 by XREAL_1:63; then A1: 0 + (2 * t) <= (((t ^2) - (2 * t)) + 1) + (2 * t) by XREAL_1:6; assume 0 < t ; ::_thesis: (2 * t) / (1 + (t ^2)) <= 1 hence (2 * t) / (1 + (t ^2)) <= 1 by A1, XREAL_1:183; ::_thesis: verum end; Lm15: for t being real number st 0 < t holds (1 - (sqrt (1 + (t ^2)))) / t < 0 proof let t be real number ; ::_thesis: ( 0 < t implies (1 - (sqrt (1 + (t ^2)))) / t < 0 ) assume A1: 0 < t ; ::_thesis: (1 - (sqrt (1 + (t ^2)))) / t < 0 then 0 + 1 < (t ^2) + 1 by SQUARE_1:12, XREAL_1:8; then 1 < sqrt ((t ^2) + 1) by SQUARE_1:18, SQUARE_1:27; then - (sqrt ((t ^2) + 1)) < - 1 by XREAL_1:24; then (- (sqrt ((t ^2) + 1))) + 1 < (- 1) + 1 by XREAL_1:8; then (1 - (sqrt ((t ^2) + 1))) / t < 0 / t by A1, XREAL_1:74; hence (1 - (sqrt (1 + (t ^2)))) / t < 0 ; ::_thesis: verum end; Lm16: for t being real number st 0 < t & t <= 1 holds 0 <= 1 - (t ^2) proof let t be real number ; ::_thesis: ( 0 < t & t <= 1 implies 0 <= 1 - (t ^2) ) assume ( 0 < t & t <= 1 ) ; ::_thesis: 0 <= 1 - (t ^2) then t ^2 <= 1 ^2 by SQUARE_1:15; then (t ^2) - (t ^2) <= 1 - (t ^2) by XREAL_1:13; hence 0 <= 1 - (t ^2) ; ::_thesis: verum end; Lm17: for t being real number st 0 < t & t <= 1 holds 0 <= 4 - (4 * (t ^2)) proof let t be real number ; ::_thesis: ( 0 < t & t <= 1 implies 0 <= 4 - (4 * (t ^2)) ) assume ( 0 < t & t <= 1 ) ; ::_thesis: 0 <= 4 - (4 * (t ^2)) then 0 <= 1 - (t ^2) by Lm16; then 0 * 4 <= 4 * (1 - (t ^2)) ; hence 0 <= 4 - (4 * (t ^2)) ; ::_thesis: verum end; Lm18: for t being real number st 0 < t & t <= 1 holds 0 < 1 + (sqrt (1 - (t ^2))) proof let t be real number ; ::_thesis: ( 0 < t & t <= 1 implies 0 < 1 + (sqrt (1 - (t ^2))) ) assume ( 0 < t & t <= 1 ) ; ::_thesis: 0 < 1 + (sqrt (1 - (t ^2))) then 0 <= 1 - (t ^2) by Lm16; then 0 <= sqrt (1 - (t ^2)) by SQUARE_1:17, SQUARE_1:26; hence 0 < 1 + (sqrt (1 - (t ^2))) ; ::_thesis: verum end; Lm19: for t being real number st 0 < t & t <= 1 holds 0 < (1 + (sqrt (1 - (t ^2)))) / t proof let t be real number ; ::_thesis: ( 0 < t & t <= 1 implies 0 < (1 + (sqrt (1 - (t ^2)))) / t ) assume that A1: 0 < t and A2: t <= 1 ; ::_thesis: 0 < (1 + (sqrt (1 - (t ^2)))) / t 0 < 1 + (sqrt (1 - (t ^2))) by A1, A2, Lm18; then 0 / t < (1 + (sqrt (1 - (t ^2)))) / t by A1, XREAL_1:74; hence 0 < (1 + (sqrt (1 - (t ^2)))) / t ; ::_thesis: verum end; Lm20: for t being real number st 0 < t & t <> 1 holds (2 * t) / ((t ^2) - 1) <> 0 proof let t be real number ; ::_thesis: ( 0 < t & t <> 1 implies (2 * t) / ((t ^2) - 1) <> 0 ) assume that A1: 0 < t and A2: t <> 1 ; ::_thesis: (2 * t) / ((t ^2) - 1) <> 0 percases ( 1 < t or t < 1 ) by A2, XXREAL_0:1; supposeA3: 1 < t ; ::_thesis: (2 * t) / ((t ^2) - 1) <> 0 then t < t ^2 by SQUARE_1:14; then 1 < t ^2 by A3, XXREAL_0:2; then A4: 1 - 1 < (t ^2) - 1 by XREAL_1:14; 2 * 1 < 2 * t by A3, XREAL_1:68; then 0 / ((t ^2) - 1) < (2 * t) / ((t ^2) - 1) by A4, XREAL_1:74; hence (2 * t) / ((t ^2) - 1) <> 0 ; ::_thesis: verum end; supposeA5: t < 1 ; ::_thesis: (2 * t) / ((t ^2) - 1) <> 0 then t ^2 < t by A1, SQUARE_1:13; then t ^2 < 1 by A5, XXREAL_0:2; then A6: (t ^2) - 1 < 1 - 1 by XREAL_1:14; 0 * 2 < 2 * t by A1, XREAL_1:68; then (2 * t) / ((t ^2) - 1) < 0 / ((t ^2) - 1) by A6, XREAL_1:75; hence (2 * t) / ((t ^2) - 1) <> 0 ; ::_thesis: verum end; end; end; Lm21: for t being real number st t < 0 holds (1 + (sqrt (1 + (t ^2)))) / t < 0 proof let t be real number ; ::_thesis: ( t < 0 implies (1 + (sqrt (1 + (t ^2)))) / t < 0 ) assume A1: t < 0 ; ::_thesis: (1 + (sqrt (1 + (t ^2)))) / t < 0 0 + 1 < (sqrt (1 + (t ^2))) + 1 by Th4, XREAL_1:8; then (1 + (sqrt (1 + (t ^2)))) / t < 0 / t by A1, XREAL_1:75; hence (1 + (sqrt (1 + (t ^2)))) / t < 0 ; ::_thesis: verum end; begin definition let x be real number ; func sinh" x -> real number equals :: SIN_COS7:def 1 log (number_e,(x + (sqrt ((x ^2) + 1)))); coherence log (number_e,(x + (sqrt ((x ^2) + 1)))) is real number ; end; :: deftheorem defines sinh" SIN_COS7:def_1_:_ for x being real number holds sinh" x = log (number_e,(x + (sqrt ((x ^2) + 1)))); definition let x be real number ; func cosh1" x -> real number equals :: SIN_COS7:def 2 log (number_e,(x + (sqrt ((x ^2) - 1)))); coherence log (number_e,(x + (sqrt ((x ^2) - 1)))) is real number ; end; :: deftheorem defines cosh1" SIN_COS7:def_2_:_ for x being real number holds cosh1" x = log (number_e,(x + (sqrt ((x ^2) - 1)))); definition let x be real number ; func cosh2" x -> real number equals :: SIN_COS7:def 3 - (log (number_e,(x + (sqrt ((x ^2) - 1))))); coherence - (log (number_e,(x + (sqrt ((x ^2) - 1))))) is real number ; end; :: deftheorem defines cosh2" SIN_COS7:def_3_:_ for x being real number holds cosh2" x = - (log (number_e,(x + (sqrt ((x ^2) - 1))))); definition let x be real number ; func tanh" x -> real number equals :: SIN_COS7:def 4 (1 / 2) * (log (number_e,((1 + x) / (1 - x)))); coherence (1 / 2) * (log (number_e,((1 + x) / (1 - x)))) is real number ; end; :: deftheorem defines tanh" SIN_COS7:def_4_:_ for x being real number holds tanh" x = (1 / 2) * (log (number_e,((1 + x) / (1 - x)))); definition let x be real number ; func coth" x -> real number equals :: SIN_COS7:def 5 (1 / 2) * (log (number_e,((x + 1) / (x - 1)))); coherence (1 / 2) * (log (number_e,((x + 1) / (x - 1)))) is real number ; end; :: deftheorem defines coth" SIN_COS7:def_5_:_ for x being real number holds coth" x = (1 / 2) * (log (number_e,((x + 1) / (x - 1)))); definition let x be real number ; func sech1" x -> real number equals :: SIN_COS7:def 6 log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)); coherence log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)) is real number ; end; :: deftheorem defines sech1" SIN_COS7:def_6_:_ for x being real number holds sech1" x = log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)); definition let x be real number ; func sech2" x -> real number equals :: SIN_COS7:def 7 - (log (number_e,((1 + (sqrt (1 - (x ^2)))) / x))); coherence - (log (number_e,((1 + (sqrt (1 - (x ^2)))) / x))) is real number ; end; :: deftheorem defines sech2" SIN_COS7:def_7_:_ for x being real number holds sech2" x = - (log (number_e,((1 + (sqrt (1 - (x ^2)))) / x))); definition let x be real number ; func csch" x -> real number equals :Def8: :: SIN_COS7:def 8 log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) if 0 < x log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) if x < 0 ; correctness coherence ( ( 0 < x implies log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) is real number ) & ( x < 0 implies log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) is real number ) ); consistency for b1 being real number st 0 < x & x < 0 holds ( b1 = log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) iff b1 = log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) ); ; end; :: deftheorem Def8 defines csch" SIN_COS7:def_8_:_ for x being real number holds ( ( 0 < x implies csch" x = log (number_e,((1 + (sqrt (1 + (x ^2)))) / x)) ) & ( x < 0 implies csch" x = log (number_e,((1 - (sqrt (1 + (x ^2)))) / x)) ) ); theorem :: SIN_COS7:33 for x being real number st 0 <= x holds sinh" x = cosh1" (sqrt ((x ^2) + 1)) proof let x be real number ; ::_thesis: ( 0 <= x implies sinh" x = cosh1" (sqrt ((x ^2) + 1)) ) assume A1: 0 <= x ; ::_thesis: sinh" x = cosh1" (sqrt ((x ^2) + 1)) x ^2 >= 0 by XREAL_1:63; then cosh1" (sqrt ((x ^2) + 1)) = log (number_e,((sqrt ((x ^2) + 1)) + (sqrt (((x ^2) + 1) - 1)))) by SQUARE_1:def_2 .= log (number_e,((sqrt ((x ^2) + 1)) + x)) by A1, SQUARE_1:22 ; hence sinh" x = cosh1" (sqrt ((x ^2) + 1)) ; ::_thesis: verum end; theorem :: SIN_COS7:34 for x being real number st x < 0 holds sinh" x = cosh2" (sqrt ((x ^2) + 1)) proof let x be real number ; ::_thesis: ( x < 0 implies sinh" x = cosh2" (sqrt ((x ^2) + 1)) ) assume A1: x < 0 ; ::_thesis: sinh" x = cosh2" (sqrt ((x ^2) + 1)) A2: (sqrt ((x ^2) + 1)) + x > 0 by Th5; A3: 1 / ((sqrt ((x ^2) + 1)) + x) = ((sqrt ((x ^2) + 1)) + x) to_power (- 1) by Th1, Th5; A4: x ^2 >= 0 by XREAL_1:63; then cosh2" (sqrt ((x ^2) + 1)) = - (log (number_e,((sqrt ((x ^2) + 1)) + (sqrt (((x ^2) + 1) - 1))))) by SQUARE_1:def_2 .= - (log (number_e,((sqrt ((x ^2) + 1)) + (- x)))) by A1, SQUARE_1:23 .= - (log (number_e,((((sqrt ((x ^2) + 1)) - x) * ((sqrt ((x ^2) + 1)) + x)) / ((sqrt ((x ^2) + 1)) + x)))) by A2, XCMPLX_1:89 .= - (log (number_e,((((sqrt ((x ^2) + 1)) ^2) - (x ^2)) / ((sqrt ((x ^2) + 1)) + x)))) .= - (log (number_e,((((x ^2) + 1) - (x ^2)) / ((sqrt ((x ^2) + 1)) + x)))) by A4, SQUARE_1:def_2 .= - ((- 1) * (log (number_e,((sqrt ((x ^2) + 1)) + x)))) by A2, A3, Lm1, POWER:55, TAYLOR_1:11 .= log (number_e,((sqrt ((x ^2) + 1)) + x)) ; hence sinh" x = cosh2" (sqrt ((x ^2) + 1)) ; ::_thesis: verum end; theorem :: SIN_COS7:35 for x being real number holds sinh" x = tanh" (x / (sqrt ((x ^2) + 1))) proof let x be real number ; ::_thesis: sinh" x = tanh" (x / (sqrt ((x ^2) + 1))) set t = (sqrt ((x ^2) + 1)) + x; A1: (sqrt ((x ^2) + 1)) + x > 0 by Th5; A2: (x ^2) + 1 > 0 by Lm6; A3: sqrt ((x ^2) + 1) > 0 by Th4; then tanh" (x / (sqrt ((x ^2) + 1))) = (1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (1 - (x / (sqrt ((x ^2) + 1))))))) by XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (((1 * (sqrt ((x ^2) + 1))) - x) / (sqrt ((x ^2) + 1)))))) by A3, XCMPLX_1:127 .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) / ((sqrt ((x ^2) + 1)) - x)))) by A3, XCMPLX_1:55 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) - x) * ((sqrt ((x ^2) + 1)) + x))))) by A1, XCMPLX_1:91 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) * (sqrt ((x ^2) + 1))) - (x ^2))))) .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / ((sqrt (((x ^2) + 1) ^2)) - (x ^2))))) by A2, SQUARE_1:29 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((x ^2) + 1) - (x ^2))))) by A2, SQUARE_1:22 .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) ^2))) .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) to_power 2))) by POWER:46 .= (1 / 2) * (2 * (log (number_e,((sqrt ((x ^2) + 1)) + x)))) by A1, Lm1, POWER:55, TAYLOR_1:11 .= log (number_e,((sqrt ((x ^2) + 1)) + x)) ; hence sinh" x = tanh" (x / (sqrt ((x ^2) + 1))) ; ::_thesis: verum end; theorem :: SIN_COS7:36 for x being real number st x >= 1 holds cosh1" x = sinh" (sqrt ((x ^2) - 1)) proof let x be real number ; ::_thesis: ( x >= 1 implies cosh1" x = sinh" (sqrt ((x ^2) - 1)) ) assume A1: x >= 1 ; ::_thesis: cosh1" x = sinh" (sqrt ((x ^2) - 1)) then (x ^2) - 1 >= 0 by Lm3; then sinh" (sqrt ((x ^2) - 1)) = log (number_e,((sqrt ((x ^2) - 1)) + (sqrt (((x ^2) - 1) + 1)))) by SQUARE_1:def_2 .= log (number_e,((sqrt ((x ^2) - 1)) + x)) by A1, SQUARE_1:22 ; hence cosh1" x = sinh" (sqrt ((x ^2) - 1)) ; ::_thesis: verum end; theorem :: SIN_COS7:37 for x being real number st x > 1 holds cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) proof let x be real number ; ::_thesis: ( x > 1 implies cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) ) assume A1: x > 1 ; ::_thesis: cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) then A2: (sqrt ((x ^2) - 1)) + x > 0 by Th23; x ^2 > (1 ^2) + 0 by A1, SQUARE_1:16; then A3: (x ^2) - 1 > 0 by XREAL_1:20; tanh" ((sqrt ((x ^2) - 1)) / x) = (1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + (x * 1)) / x) / (1 - ((sqrt ((x ^2) - 1)) / x))))) by A1, XCMPLX_1:113 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) / x) / (((1 * x) - (sqrt ((x ^2) - 1))) / x)))) by A1, XCMPLX_1:127 .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) / (x - (sqrt ((x ^2) - 1)))))) by A1, XCMPLX_1:55 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x - (sqrt ((x ^2) - 1))) * ((sqrt ((x ^2) - 1)) + x))))) by A2, XCMPLX_1:91 .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x ^2) - ((sqrt ((x ^2) - 1)) ^2))))) .= (1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x ^2) - ((x ^2) - 1))))) by A3, SQUARE_1:def_2 .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) ^2))) .= (1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) to_power 2))) by POWER:46 .= (1 / 2) * (2 * (log (number_e,((sqrt ((x ^2) - 1)) + x)))) by A2, Lm1, POWER:55, TAYLOR_1:11 .= log (number_e,((sqrt ((x ^2) - 1)) + x)) ; hence cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) ; ::_thesis: verum end; theorem :: SIN_COS7:38 for x being real number st x >= 1 holds cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2))) proof let x be real number ; ::_thesis: ( x >= 1 implies cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2))) ) assume A1: x >= 1 ; ::_thesis: cosh1" x = 2 * (cosh1" (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 * (cosh1" (sqrt ((x + 1) / 2))) = 2 * (log (number_e,((sqrt ((x + 1) / 2)) + (sqrt (((x + 1) / 2) - 1))))) by A1, SQUARE_1:def_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 cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2))) ; ::_thesis: verum end; theorem :: SIN_COS7:39 for x being real number st x >= 1 holds cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2))) proof let x be real number ; ::_thesis: ( x >= 1 implies cosh2" x = 2 * (cosh2" (sqrt ((x + 1) / 2))) ) assume A1: x >= 1 ; ::_thesis: 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))) ; ::_thesis: verum end; theorem :: SIN_COS7:40 for x being real number st x >= 1 holds cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) proof let x be real number ; ::_thesis: ( x >= 1 implies cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) ) assume A1: x >= 1 ; ::_thesis: cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) then A2: (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 by Th10; A3: ((x ^2) - 1) / 4 >= 0 by A1, Th9; A4: (x - 1) / 2 >= 0 by A1, Th7; then 2 * (sinh" (sqrt ((x - 1) / 2))) = 2 * (log (number_e,((sqrt ((x - 1) / 2)) + (sqrt (((x - 1) / 2) + 1))))) by SQUARE_1:def_2 .= log (number_e,(((sqrt ((x - 1) / 2)) + (sqrt ((x + 1) / 2))) to_power 2)) by A2, 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 A4, SQUARE_1:def_2 .= log (number_e,((((x - 1) / 2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((x + 1) / 2))) by A1, 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, A4, 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 cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) ; ::_thesis: verum end; theorem :: SIN_COS7:41 for x being real number st x ^2 < 1 holds tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) proof let x be real number ; ::_thesis: ( x ^2 < 1 implies tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) ) assume A1: x ^2 < 1 ; ::_thesis: tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) then A2: x + 1 > 0 by Th11; A3: sqrt (x + 1) > 0 by A1, Th11, SQUARE_1:25; A4: (x + 1) / (1 - x) > 0 by A1, Lm4; A5: 1 - (x ^2) > 0 by A1, XREAL_1:50; A6: 1 - x > 0 by A1, Th11; then A7: sqrt ((x + 1) / (1 - x)) = ((x + 1) / (1 - x)) to_power (1 / 2) by A2, ASYMPT_1:83; sinh" (x / (sqrt (1 - (x ^2)))) = log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) / ((sqrt (1 - (x ^2))) ^2)) + 1)))) by XCMPLX_1:76 .= log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) / (1 - (x ^2))) + 1)))) by A5, SQUARE_1:def_2 .= log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) + ((1 - (x ^2)) * 1)) / (1 - (x ^2)))))) by A5, XCMPLX_1:113 .= log (number_e,((x / (sqrt (1 - (x ^2)))) + ((sqrt 1) / (sqrt (1 - (x ^2)))))) by A5, SQUARE_1:30 .= log (number_e,((x + 1) / (sqrt ((1 - x) * (1 + x))))) by SQUARE_1:18 .= log (number_e,((sqrt ((x + 1) ^2)) / (sqrt ((1 - x) * (1 + x))))) by A2, SQUARE_1:22 .= log (number_e,(((sqrt (x + 1)) * (sqrt (x + 1))) / (sqrt ((1 - x) * (1 + x))))) by A2, SQUARE_1:29 .= log (number_e,(((sqrt (x + 1)) * (sqrt (x + 1))) / ((sqrt (1 - x)) * (sqrt (1 + x))))) by A2, A6, SQUARE_1:29 .= log (number_e,((sqrt (x + 1)) / (sqrt (1 - x)))) by A3, XCMPLX_1:91 .= log (number_e,(sqrt ((x + 1) / (1 - x)))) by A2, A6, SQUARE_1:30 .= (1 / 2) * (log (number_e,((1 + x) / (1 - x)))) by A4, A7, Lm1, POWER:55, TAYLOR_1:11 ; hence tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; theorem :: SIN_COS7:42 for x being real number st 0 < x & x < 1 holds tanh" x = cosh1" (1 / (sqrt (1 - (x ^2)))) proof let x be real number ; ::_thesis: ( 0 < x & x < 1 implies tanh" x = cosh1" (1 / (sqrt (1 - (x ^2)))) ) assume that A1: 0 < x and A2: x < 1 ; ::_thesis: tanh" x = cosh1" (1 / (sqrt (1 - (x ^2)))) A3: 1 - (x ^2) > 0 by A1, A2, Lm5; A4: (1 + x) / (1 - x) > 0 by A1, A2, Th15; A5: 1 - x > 0 by A2, XREAL_1:50; A6: sqrt (1 + x) > 0 by A1, SQUARE_1:25; (1 + x) / (1 - x) > 0 by A1, A2, Th15; then A7: sqrt ((1 + x) / (1 - x)) = ((1 + x) / (1 - x)) to_power (1 / 2) by ASYMPT_1:83; A8: x ^2 >= 0 by XREAL_1:63; cosh1" (1 / (sqrt (1 - (x ^2)))) = log (number_e,((1 / (sqrt (1 - (x ^2)))) + (sqrt ((1 / ((sqrt (1 - (x ^2))) ^2)) - (1 ^2))))) by XCMPLX_1:76 .= log (number_e,((1 / (sqrt (1 - (x ^2)))) + (sqrt ((1 / (1 - (x ^2))) - 1)))) by A3, SQUARE_1:def_2 .= log (number_e,((1 / (sqrt (1 - (x ^2)))) + (sqrt ((1 - (1 * (1 - (x ^2)))) / (1 - (x ^2)))))) by A3, XCMPLX_1:126 .= log (number_e,((1 / (sqrt (1 - (x ^2)))) + ((sqrt (x ^2)) / (sqrt (1 - (x ^2)))))) by A3, A8, SQUARE_1:30 .= log (number_e,((1 / (sqrt (1 - (x ^2)))) + (x / (sqrt (1 - (x ^2)))))) by A1, SQUARE_1:22 .= log (number_e,((1 + x) / (sqrt ((1 - x) * (1 + x))))) .= log (number_e,((1 + x) / ((sqrt (1 - x)) * (sqrt (1 + x))))) by A1, A5, SQUARE_1:29 .= log (number_e,((sqrt ((1 + x) ^2)) / ((sqrt (1 - x)) * (sqrt (1 + x))))) by A1, SQUARE_1:22 .= log (number_e,(((sqrt (1 + x)) * (sqrt (1 + x))) / ((sqrt (1 - x)) * (sqrt (1 + x))))) by A1, SQUARE_1:29 .= log (number_e,((sqrt (1 + x)) / (sqrt (1 - x)))) by A6, XCMPLX_1:91 .= log (number_e,(sqrt ((1 + x) / (1 - x)))) by A1, A5, SQUARE_1:30 .= (1 / 2) * (log (number_e,((1 + x) / (1 - x)))) by A7, A4, Lm1, POWER:55, TAYLOR_1:11 ; hence tanh" x = cosh1" (1 / (sqrt (1 - (x ^2)))) ; ::_thesis: verum end; theorem :: SIN_COS7:43 for x being real number st x ^2 < 1 holds tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) proof let x be real number ; ::_thesis: ( x ^2 < 1 implies tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) ) assume A1: x ^2 < 1 ; ::_thesis: tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) then A2: (1 - (x ^2)) ^2 > 0 by Th12; A3: x + 1 > 0 by A1, Th11; (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) = (1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((2 * x) ^2) / ((1 - (x ^2)) ^2)) + 1))))) by XCMPLX_1:76 .= (1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt (((4 * (x ^2)) + (((1 - (x ^2)) ^2) * 1)) / ((1 - (x ^2)) ^2)))))) by A2, XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((x ^2) + 1) ^2) / ((1 - (x ^2)) ^2)))))) .= (1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((x ^2) + 1) / (1 - (x ^2))) ^2))))) by XCMPLX_1:76 .= (1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (((x ^2) + 1) / (1 - (x ^2)))))) by A1, Th13, SQUARE_1:22 .= (1 / 2) * (log (number_e,(((2 * x) + ((x ^2) + 1)) / (1 - (x ^2))))) .= (1 / 2) * (log (number_e,(((x + 1) * (x + 1)) / ((1 - x) * (1 + x))))) .= (1 / 2) * (log (number_e,((x + 1) / (1 - x)))) by A3, XCMPLX_1:91 ; hence tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) ; ::_thesis: verum end; theorem :: SIN_COS7:44 for x being real number st x > 0 & x < 1 holds tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2)))) proof let x be real number ; ::_thesis: ( x > 0 & x < 1 implies tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2)))) ) assume that A1: x > 0 and A2: x < 1 ; ::_thesis: tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2)))) A3: 0 < (1 - (x ^2)) ^2 by A1, A2, Th19; A4: (2 * x) / (1 - (x ^2)) > 0 by A1, A2, Th18; (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2)))) = (1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + (sqrt ((((1 + (x ^2)) ^2) / ((1 - (x ^2)) ^2)) - 1))))) by XCMPLX_1:76 .= (1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + (sqrt ((((1 + (x ^2)) ^2) - (1 * ((1 - (x ^2)) ^2))) / ((1 - (x ^2)) ^2)))))) by A3, XCMPLX_1:126 .= (1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + (sqrt (((2 * x) ^2) / ((1 - (x ^2)) ^2)))))) .= (1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + (sqrt (((2 * x) / (1 - (x ^2))) ^2))))) by XCMPLX_1:76 .= (1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + ((2 * x) / (1 - (x ^2)))))) by A4, SQUARE_1:22 .= (1 / 2) * (log (number_e,(((1 + (x ^2)) + (2 * x)) / (1 - (x ^2))))) .= (1 / 2) * (log (number_e,(((x + 1) * (x + 1)) / ((1 - x) * (1 + x))))) .= (1 / 2) * (log (number_e,((x + 1) / (1 - x)))) by A1, XCMPLX_1:91 ; hence tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2)))) ; ::_thesis: verum end; theorem :: SIN_COS7:45 for x being real number st x ^2 < 1 holds tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) proof let x be real number ; ::_thesis: ( x ^2 < 1 implies tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) ) assume x ^2 < 1 ; ::_thesis: tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) then A1: (x + 1) / (1 - x) > 0 by Lm4; A2: 1 + (x ^2) > 0 by Lm6; then (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) = (1 / 2) * ((1 / 2) * (log (number_e,((((2 * x) + ((1 + (x ^2)) * 1)) / (1 + (x ^2))) / (1 - ((2 * x) / (1 + (x ^2)))))))) by XCMPLX_1:113 .= (1 / 2) * ((1 / 2) * (log (number_e,(((((2 * x) + 1) + (x ^2)) / (1 + (x ^2))) / (((1 * (1 + (x ^2))) - (2 * x)) / (1 + (x ^2))))))) by A2, XCMPLX_1:127 .= (1 / 2) * ((1 / 2) * (log (number_e,(((x + 1) ^2) / ((1 - x) ^2))))) by A2, XCMPLX_1:55 .= (1 / 2) * ((1 / 2) * (log (number_e,(((x + 1) / (1 - x)) ^2)))) by XCMPLX_1:76 .= (1 / 2) * ((1 / 2) * (log (number_e,(((x + 1) / (1 - x)) to_power 2)))) by POWER:46 .= (1 / 2) * ((1 / 2) * (2 * (log (number_e,((x + 1) / (1 - x)))))) by A1, Lm1, POWER:55, TAYLOR_1:11 .= (1 / 2) * (log (number_e,((1 + x) / (1 - x)))) ; hence tanh" x = (1 / 2) * (tanh" ((2 * x) / (1 + (x ^2)))) ; ::_thesis: verum end; theorem :: SIN_COS7:46 for x being real number st x ^2 > 1 holds coth" x = tanh" (1 / x) proof let x be real number ; ::_thesis: ( x ^2 > 1 implies coth" x = tanh" (1 / x) ) assume x ^2 > 1 ; ::_thesis: coth" x = tanh" (1 / x) then A1: x <> 0 ; then tanh" (1 / x) = (1 / 2) * (log (number_e,(((1 + (x * 1)) / x) / (1 - (1 / x))))) by XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((1 + (x * 1)) / x) / (((1 * x) - 1) / x)))) by A1, XCMPLX_1:127 .= (1 / 2) * (log (number_e,((1 + x) / (x - 1)))) by A1, XCMPLX_1:55 ; hence coth" x = tanh" (1 / x) ; ::_thesis: verum end; theorem :: SIN_COS7:47 for x being real number st x > 0 & x <= 1 holds sech1" x = cosh1" (1 / x) proof let x be real number ; ::_thesis: ( x > 0 & x <= 1 implies sech1" x = cosh1" (1 / x) ) assume that A1: x > 0 and A2: x <= 1 ; ::_thesis: sech1" x = cosh1" (1 / x) A3: 1 - (x ^2) >= 0 by A1, A2, Th22; A4: x ^2 > 0 by A1, SQUARE_1:12; cosh1" (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 sech1" x = cosh1" (1 / x) ; ::_thesis: verum end; theorem :: SIN_COS7:48 for x being real number st x > 0 & x <= 1 holds sech2" x = cosh2" (1 / x) proof let x be real number ; ::_thesis: ( x > 0 & x <= 1 implies sech2" x = cosh2" (1 / x) ) assume that A1: x > 0 and A2: x <= 1 ; ::_thesis: sech2" x = cosh2" (1 / x) A3: 1 - (x ^2) >= 0 by A1, A2, Th22; A4: x ^2 > 0 by A1, SQUARE_1:12; 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) ; ::_thesis: verum end; theorem :: SIN_COS7:49 for x being real number st x > 0 holds csch" x = sinh" (1 / x) proof let x be real number ; ::_thesis: ( x > 0 implies csch" x = sinh" (1 / x) ) assume A1: x > 0 ; ::_thesis: csch" x = sinh" (1 / x) then A2: x ^2 > 0 by SQUARE_1:12; sinh" (1 / x) = log (number_e,((1 / x) + (sqrt ((1 / (x ^2)) + (1 ^2))))) by XCMPLX_1:76 .= log (number_e,((1 / x) + (sqrt ((1 + ((x ^2) * 1)) / (x ^2))))) by A2, XCMPLX_1:113 .= log (number_e,((1 / x) + ((sqrt (1 + (x ^2))) / (sqrt (x ^2))))) by A1, 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 csch" x = sinh" (1 / x) by A1, Def8; ::_thesis: verum end; theorem :: SIN_COS7:50 for x, y being real number st (x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) >= 0 holds (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) proof let x, y be real number ; ::_thesis: ( (x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) >= 0 implies (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) ) assume A1: (x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) >= 0 ; ::_thesis: (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) ( (sqrt ((x ^2) + 1)) + x > 0 & (sqrt ((y ^2) + 1)) + y > 0 ) by Th5; then A2: (sinh" x) + (sinh" y) = log (number_e,((x + (sqrt ((x ^2) + 1))) * (y + (sqrt ((y ^2) + 1))))) by Lm1, POWER:53, TAYLOR_1:11 .= log (number_e,(((x * (sqrt ((y ^2) + 1))) + ((sqrt ((x ^2) + 1)) * y)) + ((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))))) .= log (number_e,(((x * (sqrt ((y ^2) + 1))) + ((sqrt ((x ^2) + 1)) * y)) + (sqrt (((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) ^2)))) by A1, SQUARE_1:22 ; A3: (y ^2) + 1 >= 0 by Lm6; set p = sqrt ((((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) ^2) + 1); set t = sqrt (((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) ^2); A4: (x ^2) + 1 >= 0 by Lm6; A5: sqrt ((((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) ^2) + 1) = sqrt (((((x ^2) * ((sqrt (1 + (y ^2))) ^2)) + ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y * (sqrt (1 + (x ^2)))) ^2)) + 1) .= sqrt (((((x ^2) * (1 + (y ^2))) + ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y * (sqrt (1 + (x ^2)))) ^2)) + 1) by A3, SQUARE_1:def_2 .= sqrt (((((x ^2) + ((x * y) ^2)) + ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y ^2) * ((sqrt (1 + (x ^2))) ^2))) + 1) .= sqrt (((((x ^2) + ((x * y) ^2)) + ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y ^2) * (1 + (x ^2)))) + 1) by A4, SQUARE_1:def_2 .= sqrt (((((x ^2) + (2 * ((x * y) ^2))) + (y ^2)) + 1) + (((2 * x) * y) * ((sqrt (1 + (y ^2))) * (sqrt (1 + (x ^2)))))) .= sqrt (((((x ^2) + (2 * ((x * y) ^2))) + (y ^2)) + 1) + (((2 * x) * y) * (sqrt ((1 + (y ^2)) * (1 + (x ^2)))))) by A4, A3, SQUARE_1:29 ; sqrt (((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) ^2) = sqrt (((x * y) + (sqrt (((x ^2) + 1) * ((y ^2) + 1)))) ^2) by A4, A3, SQUARE_1:29 .= sqrt ((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) + 1) * ((y ^2) + 1))))) + ((sqrt (((x ^2) + 1) * ((y ^2) + 1))) ^2)) .= sqrt ((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) + 1) * ((y ^2) + 1))))) + (((((x * y) ^2) + (x ^2)) + (y ^2)) + 1)) by A4, A3, SQUARE_1:def_2 .= sqrt (((((2 * ((x * y) ^2)) + (x ^2)) + (y ^2)) + 1) + ((2 * (x * y)) * (sqrt (((x ^2) + 1) * ((y ^2) + 1))))) ; hence (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) by A2, A5; ::_thesis: verum end; theorem :: SIN_COS7:51 for x, y being real number holds (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) proof let x, y be real number ; ::_thesis: (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) set t = ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y); set q = sqrt ((((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) ^2) + 1); A1: (x ^2) + 1 >= 0 by Lm6; y + 0 < sqrt ((y ^2) + 1) by Lm8; then A2: (sqrt ((y ^2) + 1)) - y > 0 by XREAL_1:20; A3: (y ^2) + 1 >= 0 by Lm6; ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) >= 0 by Lm9; then A4: ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) = sqrt ((((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y)) ^2) by SQUARE_1:22 .= sqrt (((((sqrt ((x ^2) + 1)) ^2) * ((sqrt ((y ^2) + 1)) ^2)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2)) .= sqrt (((((x ^2) + 1) * ((sqrt ((y ^2) + 1)) ^2)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2)) by A1, SQUARE_1:def_2 .= sqrt (((((x ^2) + 1) * ((y ^2) + 1)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2)) by A3, SQUARE_1:def_2 .= sqrt (((((2 * ((x * y) ^2)) + (x ^2)) + (y ^2)) + 1) - ((2 * (x * y)) * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))))) ; A5: sqrt ((((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) ^2) + 1) = sqrt (((((x ^2) * ((sqrt (1 + (y ^2))) ^2)) - ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y * (sqrt (1 + (x ^2)))) ^2)) + 1) .= sqrt (((((x ^2) * (1 + (y ^2))) - ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y * (sqrt (1 + (x ^2)))) ^2)) + 1) by A3, SQUARE_1:def_2 .= sqrt (((((x ^2) + ((x ^2) * (y ^2))) - ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y ^2) * ((sqrt (1 + (x ^2))) ^2))) + 1) .= sqrt (((((x ^2) + ((x ^2) * (y ^2))) - ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y ^2) * (1 + (x ^2)))) + 1) by A1, SQUARE_1:def_2 .= sqrt (((((x ^2) + (y ^2)) + (2 * ((x * y) ^2))) + 1) - ((((2 * x) * y) * (sqrt (1 + (y ^2)))) * (sqrt (1 + (x ^2))))) ; ( (sqrt ((x ^2) + 1)) + x > 0 & (sqrt ((y ^2) + 1)) + y > 0 ) by Th5; then (sinh" x) - (sinh" y) = log (number_e,((x + (sqrt ((x ^2) + 1))) / (y + (sqrt ((y ^2) + 1))))) by Lm1, POWER:54, TAYLOR_1:11 .= log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / ((y + (sqrt ((y ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)))) by A2, XCMPLX_1:91 .= log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / (((sqrt ((y ^2) + 1)) ^2) - (y ^2)))) .= log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / (((y ^2) + 1) - (y ^2)))) by A3, SQUARE_1:def_2 .= log (number_e,((((x * (sqrt ((y ^2) + 1))) - (y * (sqrt ((x ^2) + 1)))) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) - (x * y))) ; hence (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) by A4, A5; ::_thesis: verum end; theorem :: SIN_COS7:52 for x, y being real number st 1 <= x & 1 <= y holds (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y implies (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) ) assume that A1: 1 <= x and A2: 1 <= y ; ::_thesis: (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) A3: (y ^2) - 1 >= 0 by A2, Lm3; set t = (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))); A4: (x ^2) - 1 >= 0 by A1, Lm3; (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) = sqrt (((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) ^2) by A1, A2, Th24, SQUARE_1:22 .= sqrt ((((x ^2) * ((sqrt ((y ^2) - 1)) ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2)) .= sqrt ((((x ^2) * ((y ^2) - 1)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2)) by A3, SQUARE_1:def_2 .= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((sqrt ((x ^2) - 1)) ^2))) .= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((x ^2) - 1))) by A4, SQUARE_1:def_2 .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) ; then A5: log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))) = log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * ((sqrt ((y ^2) - 1)) * (sqrt ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))) .= log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))) by A4, A3, SQUARE_1:29 ; A6: cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) = log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1)))) .= log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1)))) by A4, A3, SQUARE_1:def_2 .= log (number_e,((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) + (x * y)))) ; ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23; then (cosh1" x) + (cosh1" y) = log (number_e,((x + (sqrt ((x ^2) - 1))) * (y + (sqrt ((y ^2) - 1))))) by Lm1, POWER:53, TAYLOR_1:11 .= log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))) + (x * y))) .= log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))) by A4, A3, SQUARE_1:29 ; hence (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A5, A6; ::_thesis: verum end; theorem :: SIN_COS7:53 for x, y being real number st 1 <= x & 1 <= y holds (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y implies (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) ) assume that A1: 1 <= x and A2: 1 <= y ; ::_thesis: (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) A3: (y ^2) - 1 >= 0 by A2, Lm3; A4: ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23; set t = (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))); A5: (x ^2) - 1 >= 0 by A1, Lm3; (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) = sqrt (((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) ^2) by A1, A2, Th24, SQUARE_1:22 .= sqrt ((((x ^2) * ((sqrt ((y ^2) - 1)) ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2)) .= sqrt ((((x ^2) * ((y ^2) - 1)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2)) by A3, SQUARE_1:def_2 .= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((sqrt ((x ^2) - 1)) ^2))) .= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((x ^2) - 1))) by A5, SQUARE_1:def_2 .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) ; then A6: - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) = - (log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * ((sqrt ((y ^2) - 1)) * (sqrt ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) .= - (log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) by A5, A3, SQUARE_1:29 ; A7: cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) = - (log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1))))) .= - (log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1))))) by A5, A3, SQUARE_1:def_2 .= - (log (number_e,((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) + (x * y))))) ; (cosh2" x) + (cosh2" y) = (- 1) * ((log (number_e,(x + (sqrt ((x ^2) - 1))))) + (log (number_e,(y + (sqrt ((y ^2) - 1)))))) .= (- 1) * (log (number_e,((x + (sqrt ((x ^2) - 1))) * (y + (sqrt ((y ^2) - 1)))))) by A4, Lm1, POWER:53, TAYLOR_1:11 .= - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))) + (x * y)))) .= - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) by A5, A3, SQUARE_1:29 ; hence (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A6, A7; ::_thesis: verum end; theorem :: SIN_COS7:54 for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) ) assume that A1: 1 <= x and A2: 1 <= y and A3: abs y <= abs x ; ::_thesis: (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) A4: 0 <= (x ^2) - 1 by A1, Lm3; set t = (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))); A5: y - (sqrt ((y ^2) - 1)) > 0 by A2, Th25; A6: 0 <= (y ^2) - 1 by A2, Lm3; ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23; then A7: (cosh1" x) - (cosh1" y) = log (number_e,((x + (sqrt ((x ^2) - 1))) / (y + (sqrt ((y ^2) - 1))))) by Lm1, POWER:54, TAYLOR_1:11 .= log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y + (sqrt ((y ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))))) by A5, XCMPLX_1:91 .= log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((sqrt ((y ^2) - 1)) ^2)))) .= log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((y ^2) - 1)))) by A6, SQUARE_1:def_2 .= log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1))))) .= log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) by A4, A6, SQUARE_1:29 .= log (number_e,((((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (x * (sqrt ((y ^2) - 1))))) ; A8: cosh1" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) = log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1)))) .= log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1)))) by A4, A6, SQUARE_1:def_2 .= log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1)))))))) ; (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) = sqrt (((y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))) ^2) by A1, A2, A3, Th26, SQUARE_1:22 .= sqrt ((((y ^2) * ((sqrt ((x ^2) - 1)) ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2)) .= sqrt ((((y ^2) * ((x ^2) - 1)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2)) by A4, SQUARE_1:def_2 .= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((sqrt ((y ^2) - 1)) ^2))) .= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((y ^2) - 1))) by A6, SQUARE_1:def_2 .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1))))) .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) by A4, A6, SQUARE_1:29 ; hence (cosh1" x) - (cosh1" y) = cosh1" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A7, A8; ::_thesis: verum end; theorem :: SIN_COS7:55 for x, y being real number st 1 <= x & 1 <= y & abs y <= abs x holds (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) proof let x, y be real number ; ::_thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) ) assume that A1: 1 <= x and A2: 1 <= y and A3: abs y <= abs x ; ::_thesis: (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) A4: ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23; A5: 0 <= (y ^2) - 1 by A2, Lm3; set t = (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))); A6: y - (sqrt ((y ^2) - 1)) > 0 by A2, Th25; A7: 0 <= (x ^2) - 1 by A1, Lm3; A8: cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) = - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1))))) .= - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1))))) by A7, A5, SQUARE_1:def_2 .= - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))))))) ; A9: (cosh2" x) - (cosh2" y) = - ((log (number_e,(x + (sqrt ((x ^2) - 1))))) - (log (number_e,(y + (sqrt ((y ^2) - 1)))))) .= - (log (number_e,((x + (sqrt ((x ^2) - 1))) / (y + (sqrt ((y ^2) - 1)))))) by A4, Lm1, POWER:54, TAYLOR_1:11 .= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y + (sqrt ((y ^2) - 1))) * (y - (sqrt ((y ^2) - 1))))))) by A6, XCMPLX_1:91 .= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((sqrt ((y ^2) - 1)) ^2))))) .= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((y ^2) - 1))))) by A5, SQUARE_1:def_2 .= - (log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))))) .= - (log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))))) by A7, A5, SQUARE_1:29 .= - (log (number_e,((((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (x * (sqrt ((y ^2) - 1)))))) ; (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) = sqrt (((y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))) ^2) by A1, A2, A3, Th26, SQUARE_1:22 .= sqrt ((((y ^2) * ((sqrt ((x ^2) - 1)) ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2)) .= sqrt ((((y ^2) * ((x ^2) - 1)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2)) by A7, SQUARE_1:def_2 .= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((sqrt ((y ^2) - 1)) ^2))) .= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((y ^2) - 1))) by A5, SQUARE_1:def_2 .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1))))) .= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) by A7, A5, SQUARE_1:29 ; hence (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A9, A8; ::_thesis: verum end; theorem :: SIN_COS7:56 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds (tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y))) proof let x, y be real number ; ::_thesis: ( x ^2 < 1 & y ^2 < 1 implies (tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y))) ) assume A1: ( x ^2 < 1 & y ^2 < 1 ) ; ::_thesis: (tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y))) then A2: ( 0 < (1 + x) / (1 - x) & 0 < (1 + y) / (1 - y) ) by Lm4; A3: (tanh" x) + (tanh" y) = (1 / 2) * ((log (number_e,((1 + x) / (1 - x)))) + (log (number_e,((1 + y) / (1 - y))))) .= (1 / 2) * (log (number_e,(((1 + x) / (1 - x)) * ((1 + y) / (1 - y))))) by A2, Lm1, POWER:53, TAYLOR_1:11 .= (1 / 2) * (log (number_e,(((1 + x) * (1 + y)) / ((1 - x) * (1 - y))))) by XCMPLX_1:76 .= (1 / 2) * (log (number_e,((((1 + x) + y) + (x * y)) / (((1 + (x * y)) - x) - y)))) ; A4: (x * y) + 1 <> 0 by A1, Th27; then tanh" ((x + y) / (1 + (x * y))) = (1 / 2) * (log (number_e,((((x + y) + ((1 + (x * y)) * 1)) / (1 + (x * y))) / (1 - ((x + y) / (1 + (x * y))))))) by XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((((x + y) + 1) + (x * y)) / (1 + (x * y))) / (((1 * (1 + (x * y))) - (x + y)) / (1 + (x * y)))))) by A4, XCMPLX_1:127 .= (1 / 2) * (log (number_e,((((1 + x) + y) + (x * y)) / (((1 + (x * y)) - x) - y)))) by A4, XCMPLX_1:55 ; hence (tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y))) by A3; ::_thesis: verum end; theorem :: SIN_COS7:57 for x, y being real number st x ^2 < 1 & y ^2 < 1 holds (tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y))) proof let x, y be real number ; ::_thesis: ( x ^2 < 1 & y ^2 < 1 implies (tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y))) ) assume A1: ( x ^2 < 1 & y ^2 < 1 ) ; ::_thesis: (tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y))) then A2: ( 0 < (1 + x) / (1 - x) & 0 < (1 + y) / (1 - y) ) by Lm4; A3: (tanh" x) - (tanh" y) = (1 / 2) * ((log (number_e,((1 + x) / (1 - x)))) - (log (number_e,((1 + y) / (1 - y))))) .= (1 / 2) * (log (number_e,(((1 + x) / (1 - x)) / ((1 + y) / (1 - y))))) by A2, Lm1, POWER:54, TAYLOR_1:11 .= (1 / 2) * (log (number_e,(((1 + x) * (1 - y)) / ((1 - x) * (1 + y))))) by XCMPLX_1:84 .= (1 / 2) * (log (number_e,((((1 - y) + x) - (x * y)) / (((1 + y) - x) - (x * y))))) ; A4: 1 - (x * y) <> 0 by A1, Th28; then tanh" ((x - y) / (1 - (x * y))) = (1 / 2) * (log (number_e,((((x - y) + ((1 - (x * y)) * 1)) / (1 - (x * y))) / (1 - ((x - y) / (1 - (x * y))))))) by XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((((x - y) + 1) - (x * y)) / (1 - (x * y))) / (((1 * (1 - (x * y))) - (x - y)) / (1 - (x * y)))))) by A4, XCMPLX_1:127 .= (1 / 2) * (log (number_e,((((1 - y) + x) - (x * y)) / (((1 + y) - x) - (x * y))))) by A4, XCMPLX_1:55 ; hence (tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y))) by A3; ::_thesis: verum end; theorem :: SIN_COS7:58 for x being real number st 0 < x holds log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) proof let x be real number ; ::_thesis: ( 0 < x implies log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) ) assume A1: 0 < x ; ::_thesis: log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) then 2 * (tanh" ((x - 1) / (x + 1))) = log (number_e,((((x - 1) + ((x + 1) * 1)) / (x + 1)) / (1 - ((x - 1) / (x + 1))))) by XCMPLX_1:113 .= log (number_e,(((2 * x) / (x + 1)) / (((1 * (x + 1)) - (x - 1)) / (x + 1)))) by A1, XCMPLX_1:127 .= log (number_e,((2 * x) / 2)) by A1, XCMPLX_1:55 .= log (number_e,x) ; hence log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) ; ::_thesis: verum end; theorem :: SIN_COS7:59 for x being real number st 0 < x holds log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) proof let x be real number ; ::_thesis: ( 0 < x implies log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) ) assume A1: 0 < x ; ::_thesis: log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) A2: (x ^2) + 1 > 0 by Lm6; then tanh" (((x ^2) - 1) / ((x ^2) + 1)) = (1 / 2) * (log (number_e,(((((x ^2) - 1) + (((x ^2) + 1) * 1)) / ((x ^2) + 1)) / (1 - (((x ^2) - 1) / ((x ^2) + 1)))))) by XCMPLX_1:113 .= (1 / 2) * (log (number_e,(((2 * (x ^2)) / ((x ^2) + 1)) / (((1 * ((x ^2) + 1)) - ((x ^2) - 1)) / ((x ^2) + 1))))) by A2, XCMPLX_1:127 .= (1 / 2) * (log (number_e,((2 * (x ^2)) / 2))) by A2, XCMPLX_1:55 .= (1 / 2) * (log (number_e,(x to_power 2))) by POWER:46 .= (1 / 2) * (2 * (log (number_e,x))) by A1, Lm1, POWER:55, TAYLOR_1:11 .= log (number_e,x) ; hence log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) ; ::_thesis: verum end; theorem :: SIN_COS7:60 for x being real number st 1 < x holds log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) proof let x be real number ; ::_thesis: ( 1 < x implies log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) ) assume A1: 1 < x ; ::_thesis: log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) then x < x ^2 by SQUARE_1:14; then 1 < x ^2 by A1, XXREAL_0:2; then A2: 1 - 1 < (x ^2) - 1 by XREAL_1:14; 1 * 2 < 2 * x by A1, XREAL_1:68; then 1 < 2 * x by XXREAL_0:2; then A3: 1 ^2 < (2 * x) ^2 by SQUARE_1:16; cosh1" (((x ^2) + 1) / (2 * x)) = log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt (((((x ^2) + 1) ^2) / ((2 * x) ^2)) - 1)))) by XCMPLX_1:76 .= log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt ((((((x ^2) ^2) + (2 * (x ^2))) + 1) - (1 * ((2 * x) ^2))) / ((2 * x) ^2))))) by A3, XCMPLX_1:126 .= log (number_e,((((x ^2) + 1) / (2 * x)) + ((sqrt (((x ^2) - 1) ^2)) / (sqrt ((2 * x) ^2))))) by A1, A2, SQUARE_1:30 .= log (number_e,((((x ^2) + 1) / (2 * x)) + (((x ^2) - 1) / (sqrt ((2 * x) ^2))))) by A2, SQUARE_1:22 .= log (number_e,((((x ^2) + 1) / (2 * x)) + (((x ^2) - 1) / (2 * x)))) by A1, SQUARE_1:22 .= log (number_e,((((x ^2) + 1) + ((x ^2) - 1)) / (2 * x))) .= log (number_e,((2 * (x ^2)) / (2 * x))) .= log (number_e,((x * x) / x)) by XCMPLX_1:91 .= log (number_e,(x / (x / x))) by XCMPLX_1:77 .= log (number_e,(x / 1)) by A1, XCMPLX_1:60 .= log (number_e,x) ; hence log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) ; ::_thesis: verum end; theorem :: SIN_COS7:61 for x being real number st 0 < x & x < 1 & 1 <= ((x ^2) + 1) / (2 * x) holds log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x)) proof let x be real number ; ::_thesis: ( 0 < x & x < 1 & 1 <= ((x ^2) + 1) / (2 * x) implies log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x)) ) assume that A1: 0 < x and A2: x < 1 and A3: 1 <= ((x ^2) + 1) / (2 * x) ; ::_thesis: log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x)) A4: 1 / x = x to_power (- 1) by A1, Th1; x ^2 < x by A1, A2, SQUARE_1:13; then x ^2 < 1 by A2, XXREAL_0:2; then A5: (x ^2) - (x ^2) < 1 - (x ^2) by XREAL_1:14; 0 * 2 < x * 2 by A1, A3; then A6: 0 < (2 * x) ^2 by SQUARE_1:12; cosh2" (((x ^2) + 1) / (2 * x)) = - (log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt (((((x ^2) + 1) ^2) / ((2 * x) ^2)) - 1))))) by XCMPLX_1:76 .= - (log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt ((((((x ^2) ^2) + (2 * (x ^2))) + 1) - (1 * ((2 * x) ^2))) / ((2 * x) ^2)))))) by A6, XCMPLX_1:126 .= - (log (number_e,((((x ^2) + 1) / (2 * x)) + ((sqrt ((1 - (x ^2)) ^2)) / (sqrt ((2 * x) ^2)))))) by A1, A5, SQUARE_1:30 .= - (log (number_e,((((x ^2) + 1) / (2 * x)) + ((1 - (x ^2)) / (sqrt ((2 * x) ^2)))))) by A5, SQUARE_1:22 .= - (log (number_e,((((x ^2) + 1) / (2 * x)) + ((1 - (x ^2)) / (2 * x))))) by A1, SQUARE_1:22 .= - (log (number_e,((((x ^2) + 1) + (1 - (x ^2))) / (2 * x)))) .= - (log (number_e,((2 * 1) / (2 * x)))) .= - (log (number_e,(1 / x))) by XCMPLX_1:91 .= - ((- 1) * (log (number_e,x))) by A1, A4, Lm1, POWER:55, TAYLOR_1:11 .= log (number_e,x) ; hence log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x)) ; ::_thesis: verum end; theorem :: SIN_COS7:62 for x being real number st 0 < x holds log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x)) proof let x be real number ; ::_thesis: ( 0 < x implies log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x)) ) A1: x ^2 >= 0 by XREAL_1:63; assume A2: 0 < x ; ::_thesis: log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x)) then 0 * 2 < x * 2 by XREAL_1:68; then A3: 0 < (2 * x) ^2 by SQUARE_1:12; sinh" (((x ^2) - 1) / (2 * x)) = log (number_e,((((x ^2) - 1) / (2 * x)) + (sqrt (((((x ^2) - 1) ^2) / ((2 * x) ^2)) + 1)))) by XCMPLX_1:76 .= log (number_e,((((x ^2) - 1) / (2 * x)) + (sqrt ((((((x ^2) ^2) - (2 * (x ^2))) + 1) + (((2 * x) ^2) * 1)) / ((2 * x) ^2))))) by A3, XCMPLX_1:113 .= log (number_e,((((x ^2) - 1) / (2 * x)) + ((sqrt (((x ^2) + 1) ^2)) / (sqrt ((2 * x) ^2))))) by A2, SQUARE_1:30 .= log (number_e,((((x ^2) - 1) / (2 * x)) + (((x ^2) + 1) / (sqrt ((2 * x) ^2))))) by A1, SQUARE_1:22 .= log (number_e,((((x ^2) - 1) / (2 * x)) + (((x ^2) + 1) / (2 * x)))) by A2, SQUARE_1:22 .= log (number_e,((((x ^2) - 1) + ((x ^2) + 1)) / (2 * x))) .= log (number_e,((2 * (x ^2)) / (2 * x))) .= log (number_e,((x * x) / x)) by XCMPLX_1:91 .= log (number_e,(x / (x / x))) by XCMPLX_1:77 .= log (number_e,(x / 1)) by A2, XCMPLX_1:60 .= log (number_e,x) ; hence log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x)) ; ::_thesis: verum end; theorem :: SIN_COS7:63 for y, x being real number st y = (1 / 2) * ((exp_R x) - (exp_R (- x))) holds x = log (number_e,(y + (sqrt ((y ^2) + 1)))) proof let y, x be real number ; ::_thesis: ( y = (1 / 2) * ((exp_R x) - (exp_R (- x))) implies x = log (number_e,(y + (sqrt ((y ^2) + 1)))) ) A1: exp_R x > 0 by SIN_COS:55; set t = exp_R x; A2: delta (1,(- (2 * y)),(- 1)) = (((- 2) * y) ^2) - ((4 * 1) * (- 1)) by QUIN_1:def_1 .= (4 * (y ^2)) + 4 ; A3: 0 <= y ^2 by XREAL_1:63; assume y = (1 / 2) * ((exp_R x) - (exp_R (- x))) ; ::_thesis: x = log (number_e,(y + (sqrt ((y ^2) + 1)))) then (2 * y) * (exp_R x) = ((exp_R x) - (1 / (exp_R x))) * (exp_R x) by TAYLOR_1:4; then (2 * y) * (exp_R x) = ((exp_R x) ^2) - (((exp_R x) * 1) / (exp_R x)) ; then ((2 * y) * (exp_R x)) - ((2 * y) * (exp_R x)) = (((exp_R x) ^2) - 1) - ((2 * y) * (exp_R x)) by A1, XCMPLX_1:60; then ((1 * ((exp_R x) ^2)) + ((- (2 * y)) * (exp_R x))) + (- 1) = 0 ; then ( exp_R x = ((- (- (2 * y))) + (sqrt (delta (1,(- (2 * y)),(- 1))))) / (2 * 1) or exp_R x = ((- (- (2 * y))) - (sqrt (delta (1,(- (2 * y)),(- 1))))) / (2 * 1) ) by A2, A3, QUIN_1:15; then ( exp_R x = ((2 * y) + ((sqrt 4) * (sqrt ((y ^2) + 1)))) / 2 or exp_R x = ((2 * y) - (sqrt (4 * ((y ^2) + 1)))) / 2 ) by A2, A3, SQUARE_1:29; then ( exp_R x = ((2 * y) + (2 * (sqrt ((y ^2) + 1)))) / 2 or exp_R x = ((2 * y) - (2 * (sqrt ((y ^2) + 1)))) / 2 ) by A3, SQUARE_1:20, SQUARE_1:29; then A4: ( exp_R x = y + (sqrt ((y ^2) + 1)) or exp_R x = y - (sqrt ((y ^2) + 1)) ) ; y < (sqrt ((y ^2) + 1)) + 0 by Lm8; hence x = log (number_e,(y + (sqrt ((y ^2) + 1)))) by A1, A4, TAYLOR_1:12, XREAL_1:19; ::_thesis: verum end; theorem :: SIN_COS7:64 for y, x being real number st y = (1 / 2) * ((exp_R x) + (exp_R (- x))) & 1 <= y & not x = log (number_e,(y + (sqrt ((y ^2) - 1)))) holds x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) proof let y, x be real number ; ::_thesis: ( y = (1 / 2) * ((exp_R x) + (exp_R (- x))) & 1 <= y & not x = log (number_e,(y + (sqrt ((y ^2) - 1)))) implies x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) ) assume that A1: y = (1 / 2) * ((exp_R x) + (exp_R (- x))) and A2: 1 <= y ; ::_thesis: ( x = log (number_e,(y + (sqrt ((y ^2) - 1)))) or x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) ) A3: y + (sqrt ((y ^2) - 1)) > 0 by A2, Lm10; set t = exp_R x; (2 * y) * (exp_R x) = ((exp_R x) + (1 / (exp_R x))) * (exp_R x) by A1, TAYLOR_1:4; then ( 0 < exp_R x & (2 * y) * (exp_R x) = ((exp_R x) ^2) + (((exp_R x) * 1) / (exp_R x)) ) by SIN_COS:55; then ((2 * y) * (exp_R x)) - ((2 * y) * (exp_R x)) = (((exp_R x) ^2) + 1) - ((2 * y) * (exp_R x)) by XCMPLX_1:60; then A4: 0 = ((1 * ((exp_R x) ^2)) + ((- (2 * y)) * (exp_R x))) + 1 ; A5: delta (1,(- (2 * y)),1) = (((- 2) * y) ^2) - ((4 * 1) * 1) by QUIN_1:def_1 .= (4 * (y ^2)) - 4 ; A6: 0 <= (y ^2) - 1 by A2, Lm3; then 0 * 4 <= ((y ^2) - 1) * 4 ; then ( exp_R x = ((- (- (2 * y))) + (sqrt (delta (1,(- (2 * y)),1)))) / (2 * 1) or exp_R x = ((- (- (2 * y))) - (sqrt (delta (1,(- (2 * y)),1)))) / (2 * 1) ) by A4, A5, QUIN_1:15; then ( exp_R x = ((2 * y) + ((sqrt 4) * (sqrt ((y ^2) - 1)))) / 2 or exp_R x = ((2 * y) - (sqrt (4 * ((y ^2) - 1)))) / 2 ) by A6, A5, SQUARE_1:29; then ( exp_R x = ((2 * y) + (2 * (sqrt ((y ^2) - 1)))) / 2 or exp_R x = ((2 * y) - (2 * (sqrt ((y ^2) - 1)))) / 2 ) by A6, SQUARE_1:20, SQUARE_1:29; then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(y - (sqrt ((y ^2) - 1)))) = x ) by TAYLOR_1:12; then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y - (sqrt ((y ^2) - 1))) * (y + (sqrt ((y ^2) - 1)))) / (y + (sqrt ((y ^2) - 1))))) = x ) by A3, XCMPLX_1:89; then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y ^2) - ((sqrt ((y ^2) - 1)) ^2)) / (y + (sqrt ((y ^2) - 1))))) = x ) ; then A7: ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y ^2) - ((y ^2) - 1)) / (y + (sqrt ((y ^2) - 1))))) = x ) by A6, SQUARE_1:def_2; 1 / (y + (sqrt ((y ^2) - 1))) = (y + (sqrt ((y ^2) - 1))) to_power (- 1) by A3, Th1; then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or (- 1) * (log (number_e,(y + (sqrt ((y ^2) - 1))))) = x ) by A3, A7, Lm1, POWER:55, TAYLOR_1:11; hence ( x = log (number_e,(y + (sqrt ((y ^2) - 1)))) or x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) ) ; ::_thesis: verum end; theorem :: SIN_COS7:65 for y, x being real number st y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) holds x = (1 / 2) * (log (number_e,((1 + y) / (1 - y)))) proof let y, x be real number ; ::_thesis: ( y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) implies x = (1 / 2) * (log (number_e,((1 + y) / (1 - y)))) ) A1: 0 < exp_R x by SIN_COS:55; set t = exp_R x; assume y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) ; ::_thesis: x = (1 / 2) * (log (number_e,((1 + y) / (1 - y)))) then y = ((exp_R x) - (1 / (exp_R x))) / ((exp_R x) + (exp_R (- x))) by TAYLOR_1:4; then y = ((exp_R x) - (1 / (exp_R x))) / ((exp_R x) + (1 / (exp_R x))) by TAYLOR_1:4; then y = ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) / ((exp_R x) + (1 / (exp_R x))) by A1, XCMPLX_1:127; then y = ((((exp_R x) ^2) - 1) / (exp_R x)) / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x)) by A1, XCMPLX_1:113; then A2: y = (((exp_R x) ^2) - 1) / (1 + ((exp_R x) ^2)) by A1, XCMPLX_1:55; then (1 * y) + (((exp_R x) ^2) * y) = ((((exp_R x) ^2) - 1) / (1 + ((exp_R x) ^2))) * (1 + ((exp_R x) ^2)) ; then (y + (((exp_R x) ^2) * y)) - (((exp_R x) ^2) - 1) = (((exp_R x) ^2) - 1) - (((exp_R x) ^2) - 1) by A1, XCMPLX_1:87; then (((exp_R x) ^2) * (y - 1)) / (y - 1) = (- (y + 1)) / (y - 1) ; then A3: (((exp_R x) ^2) * (y - 1)) / (y - 1) = (y + 1) / (- (y - 1)) by XCMPLX_1:192; y - 1 <> 0 by A2, Th31; then sqrt ((exp_R x) ^2) = sqrt ((y + 1) / (1 - y)) by A3, XCMPLX_1:89; then A4: exp_R x = sqrt ((y + 1) / (1 - y)) by A1, SQUARE_1:22; - 1 < y by A2, Lm11, SIN_COS:55; then A5: 0 < (y + 1) / (1 - y) by A2, Th31, Th32; then sqrt ((y + 1) / (1 - y)) = ((y + 1) / (1 - y)) to_power (1 / 2) by ASYMPT_1:83; then log (number_e,(((y + 1) / (1 - y)) to_power (1 / 2))) = x by A4, TAYLOR_1:12; hence x = (1 / 2) * (log (number_e,((1 + y) / (1 - y)))) by A5, Lm1, POWER:55, TAYLOR_1:11; ::_thesis: verum end; theorem :: SIN_COS7:66 for y, x being real number st y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & x <> 0 holds x = (1 / 2) * (log (number_e,((y + 1) / (y - 1)))) proof let y, x be real number ; ::_thesis: ( y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & x <> 0 implies x = (1 / 2) * (log (number_e,((y + 1) / (y - 1)))) ) A1: 0 < exp_R x by SIN_COS:55; set t = exp_R x; assume that A2: y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) and A3: x <> 0 ; ::_thesis: x = (1 / 2) * (log (number_e,((y + 1) / (y - 1)))) y = ((exp_R x) + (1 / (exp_R x))) / ((exp_R x) - (exp_R (- x))) by A2, TAYLOR_1:4; then y = ((exp_R x) + (1 / (exp_R x))) / ((exp_R x) - (1 / (exp_R x))) by TAYLOR_1:4; then y = ((exp_R x) + (1 / (exp_R x))) / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by A1, XCMPLX_1:127; then y = ((1 + ((exp_R x) * (exp_R x))) / (exp_R x)) / ((((exp_R x) ^2) - 1) / (exp_R x)) by A1, XCMPLX_1:113; then A4: y = (1 + ((exp_R x) ^2)) / (((exp_R x) ^2) - 1) by A1, XCMPLX_1:55; then y * (((exp_R x) ^2) - 1) = 1 + ((exp_R x) ^2) by A3, Th30, XCMPLX_1:87; then A5: (((exp_R x) ^2) * (y - 1)) / (y - 1) = (y + 1) / (y - 1) ; exp_R x <> 1 by A3, Th29; then A6: ( 1 < y or y < - 1 ) by A4, Lm12, SIN_COS:55; then ( 1 - 1 < y - 1 or y - 1 < (- 1) - 1 ) by XREAL_1:14; then sqrt ((exp_R x) ^2) = sqrt ((y + 1) / (y - 1)) by A5, XCMPLX_1:89; then A7: exp_R x = sqrt ((y + 1) / (y - 1)) by A1, SQUARE_1:22; A8: 0 < (y + 1) / (y - 1) by A6, Lm7; then sqrt ((y + 1) / (y - 1)) = ((y + 1) / (y - 1)) to_power (1 / 2) by ASYMPT_1:83; then log (number_e,(((y + 1) / (y - 1)) to_power (1 / 2))) = x by A7, TAYLOR_1:12; hence x = (1 / 2) * (log (number_e,((y + 1) / (y - 1)))) by A8, Lm1, POWER:55, TAYLOR_1:11; ::_thesis: verum end; theorem :: SIN_COS7:67 for y, x being real number holds ( not y = 1 / (((exp_R x) + (exp_R (- x))) / 2) or x = log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) or x = - (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) ) proof let y, x be real number ; ::_thesis: ( not y = 1 / (((exp_R x) + (exp_R (- x))) / 2) or x = log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) or x = - (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) ) set t = exp_R x; A1: delta (y,(- 2),y) = ((- 2) ^2) - ((4 * y) * y) by QUIN_1:def_1 .= 4 - (4 * (y ^2)) ; assume y = 1 / (((exp_R x) + (exp_R (- x))) / 2) ; ::_thesis: ( x = log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) or x = - (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) ) then y = (1 * 2) / (2 * (((exp_R x) + (exp_R (- x))) / 2)) by XCMPLX_1:91; then ( 0 < exp_R x & y = 2 / ((exp_R x) + (1 / (exp_R x))) ) by SIN_COS:55, TAYLOR_1:4; then y = 2 / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x)) by XCMPLX_1:113; then y = 2 * ((exp_R x) / (1 + ((exp_R x) ^2))) by XCMPLX_1:79; then A2: y = (2 * (exp_R x)) / (1 + ((exp_R x) ^2)) ; then A3: 0 < y by Lm13, SIN_COS:55; 1 + ((exp_R x) ^2) > 0 by Lm6; then A4: y * (1 + ((exp_R x) ^2)) = 2 * (exp_R x) by A2, XCMPLX_1:87; A5: y <= 1 by A2, Lm14, SIN_COS:55; then A6: 0 <= 1 - (y ^2) by A3, Lm16; Polynom (y,(- 2),y,(exp_R x)) = ((y * ((exp_R x) ^2)) + ((- 2) * (exp_R x))) + y by POLYEQ_1:def_2; then ( exp_R x = ((- (- 2)) + (sqrt (delta (y,(- 2),y)))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta (y,(- 2),y)))) / (2 * y) ) by A3, A5, A4, A1, Lm17, QUIN_1:15; then ( exp_R x = (2 + (sqrt (4 * (1 - (y ^2))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 - (y ^2))))) / (2 * y) ) by A1; then ( exp_R x = (2 + (2 * (sqrt (1 - (y ^2))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 - (y ^2))))) / (2 * y) ) by A6, SQUARE_1:20, SQUARE_1:29; then ( exp_R x = (2 * (1 + (sqrt (1 - (y ^2))))) / (2 * y) or exp_R x = (2 * (1 - (sqrt (1 - (y ^2))))) / (2 * y) ) ; then A7: ( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = (1 - (sqrt (1 - (y ^2)))) / y ) by XCMPLX_1:91; 0 < 1 + (sqrt (1 - (y ^2))) by A3, A5, Lm18; then ( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = ((1 - (sqrt (1 - (y ^2)))) * (1 + (sqrt (1 - (y ^2))))) / (y * (1 + (sqrt (1 - (y ^2))))) ) by A7, XCMPLX_1:91; then ( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = (1 - ((sqrt (1 - (y ^2))) ^2)) / (y * (1 + (sqrt (1 - (y ^2))))) ) ; then ( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = (1 - (1 - (y ^2))) / (y * (1 + (sqrt (1 - (y ^2))))) ) by A6, SQUARE_1:def_2; then A8: ( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = y / (1 + (sqrt (1 - (y ^2)))) ) by A3, XCMPLX_1:91; ( log (number_e,(exp_R x)) = x & 1 / ((1 + (sqrt (1 - (y ^2)))) / y) = ((1 + (sqrt (1 - (y ^2)))) / y) to_power (- 1) ) by A3, A5, Lm19, Th1, TAYLOR_1:12; then A9: ( log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) = x or log (number_e,(((1 + (sqrt (1 - (y ^2)))) / y) to_power (- 1))) = x ) by A8, XCMPLX_1:57; 0 < (1 + (sqrt (1 - (y ^2)))) / y by A3, A5, Lm19; then ( log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) = x or (- 1) * (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) = x ) by A9, Lm1, POWER:55, TAYLOR_1:11; hence ( x = log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) or x = - (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) ) ; ::_thesis: verum end; theorem :: SIN_COS7:68 for y, x being real number st y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 & not x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) holds x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) proof let y, x be real number ; ::_thesis: ( y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 & not x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) implies x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) A1: 0 < exp_R x by SIN_COS:55; set t = exp_R x; assume that A2: y = 1 / (((exp_R x) - (exp_R (- x))) / 2) and A3: x <> 0 ; ::_thesis: ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) A4: delta (y,(- 2),(- y)) = ((- 2) ^2) - ((4 * y) * (- y)) by QUIN_1:def_1 .= 4 + (4 * (y ^2)) ; y = (1 * 2) / (2 * (((exp_R x) - (exp_R (- x))) / 2)) by A2, XCMPLX_1:91; then y = 2 / ((exp_R x) - (1 / (exp_R x))) by TAYLOR_1:4; then y = 2 / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by A1, XCMPLX_1:127; then A5: y = 2 * ((exp_R x) / (((exp_R x) ^2) - 1)) by XCMPLX_1:79; then A6: y = (2 * (exp_R x)) / (((exp_R x) ^2) - 1) ; then y * (((exp_R x) ^2) - 1) = 2 * (exp_R x) by A3, Th30, XCMPLX_1:87; then A7: ((y * ((exp_R x) ^2)) + ((- 2) * (exp_R x))) + (- y) = 0 ; A8: exp_R x <> 1 by A3, Th29; then A9: (2 * (exp_R x)) / (((exp_R x) ^2) - 1) <> 0 by Lm20, SIN_COS:55; percases ( 0 < y or y < 0 ) by A9, A5; supposeA10: 0 < y ; ::_thesis: ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) A11: 0 < 1 + (y ^2) by Lm6; then 0 * 4 < 4 * (1 + (y ^2)) by XREAL_1:68; then ( exp_R x = (2 + (sqrt (delta (y,(- 2),(- y))))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta (y,(- 2),(- y))))) / (2 * y) ) by A1, A8, A6, A7, A4, Lm20, QUIN_1:15; then ( exp_R x = (2 + ((sqrt 4) * (sqrt (1 + (y ^2))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 + (y ^2))))) / (2 * y) ) by A4, A11, SQUARE_1:29; then ( exp_R x = (2 * (1 + (sqrt (1 + (y ^2))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 + (y ^2))))) / (2 * y) ) by A11, SQUARE_1:20, SQUARE_1:29; then A12: ( exp_R x = (1 + (sqrt (1 + (y ^2)))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2))))) / (2 * y) ) by XCMPLX_1:91; (1 - (sqrt (1 + (y ^2)))) / y < 0 by A10, Lm15; hence ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) by A1, A12, TAYLOR_1:12, XCMPLX_1:91; ::_thesis: verum end; supposeA13: y < 0 ; ::_thesis: ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) A14: 0 < 1 + (y ^2) by Lm6; then 0 * 4 < 4 * (1 + (y ^2)) by XREAL_1:68; then ( exp_R x = (2 + (sqrt (delta (y,(- 2),(- y))))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta (y,(- 2),(- y))))) / (2 * y) ) by A1, A8, A6, A7, A4, Lm20, QUIN_1:15; then ( exp_R x = (2 + ((sqrt 4) * (sqrt (1 + (y ^2))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 + (y ^2))))) / (2 * y) ) by A4, A14, SQUARE_1:29; then ( exp_R x = (2 * (1 + (sqrt (1 + (y ^2))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 + (y ^2))))) / (2 * y) ) by A14, SQUARE_1:20, SQUARE_1:29; then A15: ( exp_R x = (1 + (sqrt (1 + (y ^2)))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2))))) / (2 * y) ) by XCMPLX_1:91; (1 + (sqrt (1 + (y ^2)))) / y < 0 by A13, Lm21; then exp_R x = (1 - (sqrt (1 + (y ^2)))) / y by A15, SIN_COS:55, XCMPLX_1:91; hence ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) by TAYLOR_1:12; ::_thesis: verum end; end; end; theorem Th69: :: SIN_COS7:69 for x being real number holds cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2)) proof let x be real number ; ::_thesis: cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2)) 2 * ((sinh . x) ^2) = 2 * ((1 / 2) * ((cosh . (2 * x)) - 1)) by SIN_COS2:18; hence cosh . (2 * x) = 1 + (2 * ((sinh . x) ^2)) ; ::_thesis: verum end; theorem Th70: :: SIN_COS7:70 for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2) proof let x be real number ; ::_thesis: (cosh . x) ^2 = 1 + ((sinh . x) ^2) cosh . (2 * x) = cosh . (x + x) .= ((cosh . x) ^2) + ((sinh . x) ^2) by SIN_COS2:20 ; then (1 + (2 * ((sinh . x) ^2))) - ((sinh . x) ^2) = (((cosh . x) ^2) + ((sinh . x) ^2)) - ((sinh . x) ^2) by Th69; hence (cosh . x) ^2 = 1 + ((sinh . x) ^2) ; ::_thesis: verum end; theorem Th71: :: SIN_COS7:71 for x being real number holds (sinh . x) ^2 = ((cosh . x) ^2) - 1 proof let x be real number ; ::_thesis: (sinh . x) ^2 = ((cosh . x) ^2) - 1 (((cosh . x) ^2) - ((sinh . x) ^2)) - 1 = 1 - 1 by SIN_COS2:14; hence (sinh . x) ^2 = ((cosh . x) ^2) - 1 ; ::_thesis: verum end; theorem :: SIN_COS7:72 for x being real number holds sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5)) proof let x be real number ; ::_thesis: sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5)) set t = sinh . x; sinh (5 * x) = sinh . ((4 * x) + x) by SIN_COS2:def_2 .= ((sinh . (2 * (2 * x))) * (cosh . x)) + ((cosh . (4 * x)) * (sinh . x)) by SIN_COS2:21 .= (((2 * (sinh . (2 * x))) * (cosh . (2 * x))) * (cosh . x)) + ((cosh . (4 * x)) * (sinh . x)) by SIN_COS2:23 .= (((2 * ((2 * (sinh . x)) * (cosh . x))) * (cosh . (2 * x))) * (cosh . x)) + ((cosh . (4 * x)) * (sinh . x)) by SIN_COS2:23 .= (((4 * (sinh . x)) * ((cosh . x) ^2)) * (cosh . (2 * x))) + ((cosh . (4 * x)) * (sinh . x)) .= (((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + ((cosh . (2 * (2 * x))) * (sinh . x)) by Th69 .= (((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + ((1 + (2 * ((sinh . (2 * x)) ^2))) * (sinh . x)) by Th69 .= (((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + ((1 + (2 * (((2 * (sinh . x)) * (cosh . x)) ^2))) * (sinh . x)) by SIN_COS2:23 .= ((((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + (sinh . x)) + (((8 * ((sinh . x) ^2)) * (sinh . x)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + (sinh . x)) + (((8 * (((sinh . x) |^ 1) * (sinh . x))) * (sinh . x)) * ((cosh . x) ^2)) by NEWTON:5 .= ((((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + (sinh . x)) + (((8 * ((sinh . x) |^ (1 + 1))) * (sinh . x)) * ((cosh . x) ^2)) by NEWTON:6 .= ((((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + (sinh . x)) + ((8 * (((sinh . x) |^ 2) * (sinh . x))) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) * ((cosh . x) ^2)) * (1 + (2 * ((sinh . x) ^2)))) + (sinh . x)) + ((8 * ((sinh . x) |^ (2 + 1))) * ((cosh . x) ^2)) by NEWTON:6 .= (((((4 * (sinh . x)) * ((cosh . x) ^2)) * 1) + ((((4 * (sinh . x)) * ((cosh . x) ^2)) * 2) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= (((((4 * (sinh . x)) * (1 + ((sinh . x) ^2))) * 1) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by Th70 .= ((((4 * (sinh . x)) + (((4 * (sinh . x)) * (sinh . x)) * (sinh . x))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + (((4 * ((sinh . x) |^ 1)) * (sinh . x)) * (sinh . x))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:5 .= ((((4 * (sinh . x)) + ((4 * (((sinh . x) |^ 1) * (sinh . x))) * (sinh . x))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + ((4 * ((sinh . x) |^ (1 + 1))) * (sinh . x))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= ((((4 * (sinh . x)) + (4 * (((sinh . x) |^ 2) * (sinh . x)))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ (2 + 1)))) + (((8 * (sinh . x)) * ((cosh . x) ^2)) * ((sinh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + ((((8 * (sinh . x)) * (sinh . x)) * (sinh . x)) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + ((((8 * ((sinh . x) |^ 1)) * (sinh . x)) * (sinh . x)) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:5 .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (((8 * (((sinh . x) |^ 1) * (sinh . x))) * (sinh . x)) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (((8 * ((sinh . x) |^ (1 + 1))) * (sinh . x)) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + ((8 * (((sinh . x) |^ 2) * (sinh . x))) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + ((8 * ((sinh . x) |^ (2 + 1))) * ((cosh . x) ^2))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= ((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + ((8 * ((sinh . x) |^ 3)) * (1 + ((sinh . x) ^2)))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by Th70 .= (((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + ((8 * (((sinh . x) |^ 3) * (sinh . x))) * (sinh . x))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= (((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + ((8 * ((sinh . x) |^ (3 + 1))) * (sinh . x))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= (((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * (((sinh . x) |^ 4) * (sinh . x)))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) .= (((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ (4 + 1)))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * ((cosh . x) ^2)) by NEWTON:6 .= (((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 5))) + (sinh . x)) + ((8 * ((sinh . x) |^ 3)) * (1 + ((sinh . x) ^2))) by Th70 .= ((((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 5))) + (sinh . x)) + (8 * ((sinh . x) |^ 3))) + ((8 * (((sinh . x) |^ 3) * (sinh . x))) * (sinh . x)) .= ((((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 5))) + (sinh . x)) + (8 * ((sinh . x) |^ 3))) + ((8 * ((sinh . x) |^ (3 + 1))) * (sinh . x)) by NEWTON:6 .= ((((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 5))) + (sinh . x)) + (8 * ((sinh . x) |^ 3))) + (8 * (((sinh . x) |^ 4) * (sinh . x))) .= ((((((4 * (sinh . x)) + (4 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ 5))) + (sinh . x)) + (8 * ((sinh . x) |^ 3))) + (8 * ((sinh . x) |^ (4 + 1))) by NEWTON:6 .= ((5 * (sinh . x)) + (20 * ((sinh . x) |^ 3))) + ((8 * ((sinh . x) |^ 5)) + (8 * ((sinh . x) |^ 5))) .= ((5 * (sinh x)) + (20 * ((sinh . x) |^ 3))) + (16 * ((sinh . x) |^ 5)) by SIN_COS2:def_2 .= ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh . x) |^ 5)) by SIN_COS2:def_2 .= ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5)) by SIN_COS2:def_2 ; hence sinh (5 * x) = ((5 * (sinh x)) + (20 * ((sinh x) |^ 3))) + (16 * ((sinh x) |^ 5)) ; ::_thesis: verum end; theorem :: SIN_COS7:73 for x being real number holds cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5)) proof let x be real number ; ::_thesis: cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5)) set t = cosh . x; set u = sinh . x; cosh (5 * x) = cosh . ((4 * x) + x) by SIN_COS2:def_4 .= ((cosh . (2 * (2 * x))) * (cosh . x)) + ((sinh . (4 * x)) * (sinh . x)) by SIN_COS2:20 .= ((1 + (2 * ((sinh . (2 * x)) ^2))) * (cosh . x)) + ((sinh . (4 * x)) * (sinh . x)) by Th69 .= ((1 + (2 * (((2 * (sinh . x)) * (cosh . x)) ^2))) * (cosh . x)) + ((sinh . (2 * (2 * x))) * (sinh . x)) by SIN_COS2:23 .= ((cosh . x) + ((8 * ((sinh . x) ^2)) * (((cosh . x) ^2) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x)) .= ((cosh . x) + ((8 * ((sinh . x) ^2)) * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by NEWTON:5 .= ((cosh . x) + ((8 * ((sinh . x) ^2)) * (((cosh . x) |^ (1 + 1)) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by NEWTON:6 .= ((cosh . x) + ((8 * ((sinh . x) ^2)) * ((cosh . x) |^ (2 + 1)))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by NEWTON:6 .= ((cosh . x) + ((8 * (((cosh . x) ^2) - 1)) * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by Th71 .= (((cosh . x) + (8 * ((((cosh . x) |^ 3) * (cosh . x)) * (cosh . x)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x)) .= (((cosh . x) + (8 * (((cosh . x) |^ (3 + 1)) * (cosh . x)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by NEWTON:6 .= (((cosh . x) + (8 * ((cosh . x) |^ (4 + 1)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x)) by NEWTON:6 .= (((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((2 * (sinh . (2 * x))) * (cosh . (2 * x))) * (sinh . x)) by SIN_COS2:23 .= (((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((2 * ((2 * (sinh . x)) * (cosh . x))) * (cosh . (2 * x))) * (sinh . x)) by SIN_COS2:23 .= (((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((4 * ((sinh . x) ^2)) * (cosh . x)) * (cosh . (2 * x))) .= (((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((4 * (((cosh . x) ^2) - 1)) * (cosh . x)) * (cosh . (2 * x))) by Th71 .= ((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * (((cosh . x) * (cosh . x)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x))) .= ((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by NEWTON:5 .= ((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by NEWTON:6 .= ((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((cosh . x) |^ (2 + 1))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by NEWTON:6 .= ((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((cosh . x) |^ 3)) * ((2 * ((cosh . x) ^2)) - 1))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by SIN_COS2:23 .= (((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * ((((cosh . x) |^ 3) * (cosh . x)) * (cosh . x)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x))) .= (((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * (((cosh . x) |^ (3 + 1)) * (cosh . x)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by NEWTON:6 .= (((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * ((cosh . x) |^ (4 + 1)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x))) by NEWTON:6 .= (((cosh . x) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * ((2 * ((cosh . x) ^2)) - 1)) by SIN_COS2:23 .= (((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * (((cosh . x) * (cosh . x)) * (cosh . x))) .= (((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) by NEWTON:5 .= (((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) by NEWTON:6 .= (((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * ((cosh . x) |^ (2 + 1))) by NEWTON:6 .= ((5 * (cosh . x)) - (20 * ((cosh . x) |^ 3))) + (16 * ((cosh . x) |^ 5)) .= ((5 * (cosh x)) - (20 * ((cosh . x) |^ 3))) + (16 * ((cosh . x) |^ 5)) by SIN_COS2:def_4 .= ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh . x) |^ 5)) by SIN_COS2:def_4 .= ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5)) by SIN_COS2:def_4 ; hence cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5)) ; ::_thesis: verum end;