:: SIN_COS7 semantic presentation

begin

theorem :: SIN_COS7:1
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = x : ( ( real ) ( V11() real ext-real ) number ) to_power (- 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non positive V33() V34() ) M2( INT : ( ( ) ( V45() V46() V47() V48() V49() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SIN_COS7:2
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
((sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:3
for x being ( ( real ) ( V11() real ext-real ) number ) holds (x : ( ( real ) ( V11() real ext-real ) number ) / (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:4
for x being ( ( real ) ( V11() real ext-real ) number ) holds sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:5
for x being ( ( real ) ( V11() real ext-real ) number ) holds (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:6
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:7
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(x : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:8
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:9
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:10
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:11
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
( x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

theorem :: SIN_COS7:12
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:13
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:14
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
((2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:15
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:16
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:17
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:18
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:19
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:20
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) > 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:21
for x being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) holds
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:22
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) <= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:23
for x being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) + (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:24
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= (x : ( ( real ) ( V11() real ext-real ) number ) * (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (y : ( ( real ) ( V11() real ext-real ) number ) * (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:25
for y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < y : ( ( real ) ( V11() real ext-real ) number ) - (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:26
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) & abs y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <= abs x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= (y : ( ( real ) ( V11() real ext-real ) number ) * (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (x : ( ( real ) ( V11() real ext-real ) number ) * (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:27
for x, y being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <> - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real non positive V33() V34() ) M2( INT : ( ( ) ( V45() V46() V47() V48() V49() V51() ) set ) )) ;

theorem :: SIN_COS7:28
for x, y being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <> 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:29
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
exp_R x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <> 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:30
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <> x : ( ( real ) ( V11() real ext-real ) number ) holds
((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <> 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:31
for t being ( ( real ) ( V11() real ext-real ) number ) holds ((t : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((t : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: SIN_COS7:32
for t being ( ( real ) ( V11() real ext-real ) number ) st - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real non positive V33() V34() ) M2( INT : ( ( ) ( V45() V46() V47() V48() V49() V51() ) set ) )) < t : ( ( real ) ( V11() real ext-real ) number ) & t : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < (t : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - t : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

begin

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func sinh" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 1
 log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt ((x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func cosh1" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 2
 log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt ((x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func cosh2" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 3
 - (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt ((x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func tanh" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 4
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func coth" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 5
(1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func sech1" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 6
 log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func sech2" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 7
 - (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;
end;

definition
let x be ( ( real ) ( V11() real ext-real ) number ) ;
func csch" x -> ( ( real ) ( V11() real ext-real ) number ) equals :: SIN_COS7:def 8
 log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) if 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ))
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) if x : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) < 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) ))
;
end;

theorem :: SIN_COS7:33
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) holds
sinh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = cosh1" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:34
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) < 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sinh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = cosh2" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:35
for x being ( ( real ) ( V11() real ext-real ) number ) holds sinh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = tanh" (x : ( ( real ) ( V11() real ext-real ) number ) / (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:36
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosh1" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = sinh" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:37
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosh1" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = tanh" ((sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:38
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosh1" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cosh1" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:39
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosh2" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cosh2" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:40
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
cosh1" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (sinh" (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:41
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tanh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = sinh" (x : ( ( real ) ( V11() real ext-real ) number ) / (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:42
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tanh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = cosh1" (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:43
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tanh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (sinh" ((2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:44
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tanh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (cosh1" ((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:45
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
tanh" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (tanh" ((2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:46
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) > 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
coth" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = tanh" (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:47
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) <= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sech1" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = cosh1" (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:48
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & x : ( ( real ) ( V11() real ext-real ) number ) <= 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
sech2" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = cosh2" (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:49
for x being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
csch" x : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = sinh" (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:50
for x, y being ( ( real ) ( V11() real ext-real ) number ) st (x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + ((sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) >= 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(sinh" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) + (sinh" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = sinh" ((x : ( ( real ) ( V11() real ext-real ) number ) * (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (y : ( ( real ) ( V11() real ext-real ) number ) * (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:51
for x, y being ( ( real ) ( V11() real ext-real ) number ) holds (sinh" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) - (sinh" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = sinh" ((x : ( ( real ) ( V11() real ext-real ) number ) * (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (y : ( ( real ) ( V11() real ext-real ) number ) * (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:52
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) holds
(cosh1" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) + (cosh1" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = cosh1" ((x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:53
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) holds
(cosh2" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) + (cosh2" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = cosh2" ((x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (sqrt (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:54
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) & abs y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <= abs x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
(cosh1" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) - (cosh1" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = cosh1" ((x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (sqrt (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:55
for x, y being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= x : ( ( real ) ( V11() real ext-real ) number ) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) & abs y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) <= abs x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
(cosh2" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) - (cosh2" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = cosh2" ((x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (sqrt (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) * ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:56
for x, y being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(tanh" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) + (tanh" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = tanh" ((x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:57
for x, y being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & y : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(tanh" x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) - (tanh" y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = tanh" ((x : ( ( real ) ( V11() real ext-real ) number ) - y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:58
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) holds
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) = 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (tanh" ((x : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (x : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:59
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) holds
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) = tanh" (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:60
for x being ( ( real ) ( V11() real ext-real ) number ) st 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) holds
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) = cosh1" (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:61
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) & x : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) = cosh2" (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:62
for x being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) < x : ( ( real ) ( V11() real ext-real ) number ) holds
log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) set ) = sinh" (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: SIN_COS7:63
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) - (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) = log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(y : ( ( real ) ( V11() real ext-real ) number ) + (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:64
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) <= y : ( ( real ) ( V11() real ext-real ) number ) & not x : ( ( real ) ( V11() real ext-real ) number ) = log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(y : ( ( real ) ( V11() real ext-real ) number ) + (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) = - (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,(y : ( ( real ) ( V11() real ext-real ) number ) + (sqrt ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:65
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) = ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) - (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:66
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) = ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / ((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) - (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & x : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) = (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real non negative V34() ) M2( RAT : ( ( ) ( V45() V46() V47() V48() V51() ) set ) )) * (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((y : ( ( real ) ( V11() real ext-real ) number ) + 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / (y : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:67
for y, x being ( ( real ) ( V11() real ext-real ) number ) holds
( not y : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / (((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) or x : ( ( real ) ( V11() real ext-real ) number ) = log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) or x : ( ( real ) ( V11() real ext-real ) number ) = - (log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) ;

theorem :: SIN_COS7:68
for y, x being ( ( real ) ( V11() real ext-real ) number ) st y : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) / (((exp_R x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) - (exp_R (- x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / 2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) & x : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( V1() natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) & not x : ( ( real ) ( V11() real ext-real ) number ) = log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) holds
x : ( ( real ) ( V11() real ext-real ) number ) = log (number_e : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ,((1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) - (sqrt (1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) / y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:69
for x being ( ( real ) ( V11() real ext-real ) number ) holds cosh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + (2 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((sinh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:70
for x being ( ( real ) ( V11() real ext-real ) number ) holds (cosh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) + ((sinh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:71
for x being ( ( real ) ( V11() real ext-real ) number ) holds (sinh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((cosh : ( ( V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) ) ( V16() V19( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V20( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V21() V30( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) V35() V36() V37() ) M2(K6(K7(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ,REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) )) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - 1 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:72
for x being ( ( real ) ( V11() real ext-real ) number ) holds sinh (5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (sinh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (20 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((sinh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (16 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((sinh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;

theorem :: SIN_COS7:73
for x being ( ( real ) ( V11() real ext-real ) number ) holds cosh (5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) = ((5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * (cosh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) - (20 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((cosh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 3 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) + (16 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) * ((cosh x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) |^ 5 : ( ( ) ( V1() natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() ) M3( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) , NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() ) M2(K6(REAL : ( ( ) ( V45() V46() V47() V51() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V45() V46() V47() V51() ) set ) )) ;