:: COMPTRIG semantic presentation
begin
scheme
:: COMPTRIG:sch 1
Regrwithout0
{
P
1
[ ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) ] } :
P
1
[1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ]
provided
ex
k
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) st
P
1
[
k
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ]
and
for
k
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) st
k
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
<>
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
P
1
[
k
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ] holds
ex
n
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) st
(
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
<
k
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) &
P
1
[
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ] )
proof
end;
theorem
:: COMPTRIG:1
for
z
being ( (
complex
) (
complex
)
number
) holds
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
-
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:2
for
z
being ( (
complex
) (
complex
)
number
) holds
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
-
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:3
for
z
being ( (
complex
) (
complex
)
number
) holds
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
^2
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
=
(
(
Re
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
^2
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
Im
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
^2
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:4
for
x
being ( (
real
) (
complex
real
ext-real
)
number
)
for
n
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
-root
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( (
real
) (
complex
real
ext-real
)
set
)
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) : ( ( ) (
complex
real
ext-real
)
set
)
=
x
: ( (
real
) (
complex
real
ext-real
)
number
) ;
registration
cluster
PI
: ( (
real
) (
complex
real
ext-real
)
set
)
->
real
non
negative
;
end;
begin
theorem
:: COMPTRIG:5
(
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) ;
theorem
:: COMPTRIG:6
for
a
,
b
,
c
,
x
being ( (
real
) (
complex
real
ext-real
)
number
) holds
( not
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
a
: ( (
real
) (
complex
real
ext-real
)
number
) ,
c
: ( (
real
) (
complex
real
ext-real
)
number
)
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) or
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
a
: ( (
real
) (
complex
real
ext-real
)
number
) ,
b
: ( (
real
) (
complex
real
ext-real
)
number
)
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) or
x
: ( (
real
) (
complex
real
ext-real
)
number
)
=
b
: ( (
real
) (
complex
real
ext-real
)
number
) or
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
b
: ( (
real
) (
complex
real
ext-real
)
number
) ,
c
: ( (
real
) (
complex
real
ext-real
)
number
)
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:7
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:8
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
[.
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:9
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:10
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
[.
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:11
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
(
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:12
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
[.
(
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:13
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:14
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
[.
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:15
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
].
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:16
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
x
: ( (
real
) (
complex
real
ext-real
)
number
)
in
[.
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) holds
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:17
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
x
: ( (
real
) (
complex
real
ext-real
)
number
) &
x
: ( (
real
) (
complex
real
ext-real
)
number
)
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
sin
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) & not
x
: ( (
real
) (
complex
real
ext-real
)
number
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
x
: ( (
real
) (
complex
real
ext-real
)
number
)
=
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:18
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) st
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
x
: ( (
real
) (
complex
real
ext-real
)
number
) &
x
: ( (
real
) (
complex
real
ext-real
)
number
)
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
cos
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) & not
x
: ( (
real
) (
complex
real
ext-real
)
number
)
=
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) holds
x
: ( (
real
) (
complex
real
ext-real
)
number
)
=
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:19
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
].
(
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
increasing
;
theorem
:: COMPTRIG:20
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
].
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
decreasing
;
theorem
:: COMPTRIG:21
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
].
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
decreasing
;
theorem
:: COMPTRIG:22
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
].
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
increasing
;
theorem
:: COMPTRIG:23
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
(
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
increasing
;
theorem
:: COMPTRIG:24
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
decreasing
;
theorem
:: COMPTRIG:25
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
decreasing
;
theorem
:: COMPTRIG:26
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) : ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) is
increasing
;
theorem
:: COMPTRIG:27
for
x
being ( (
real
) (
complex
real
ext-real
)
number
) holds
(
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
in
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) &
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
.
x
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
in
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:28
rng
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: COMPTRIG:29
rng
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: COMPTRIG:30
rng
(
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
(
-
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
positive
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) )
)
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: COMPTRIG:31
rng
(
sin
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) )
)
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: COMPTRIG:32
rng
(
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) )
)
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: COMPTRIG:33
rng
(
cos
: ( (
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
V30
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) )
|
[.
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) )
)
: ( (
Function-like
) (
Relation-like
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-defined
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
)
-valued
Function-like
continuous
V46
()
V47
()
V48
() )
Element
of
K19
(
K20
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ,
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
V46
()
V47
()
V48
() )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) (
V70
()
V71
()
V72
() )
set
)
=
[.
(
-
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
non
positive
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
.]
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ;
begin
definition
let
z
be ( (
complex
) (
complex
)
number
) ;
func
Arg
z
->
( ( ) (
complex
real
ext-real
)
Real
)
means
:: COMPTRIG:def 1
(
z
: ( ( ) ( )
set
)
=
(
|.
z
: ( ( ) ( )
set
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
cos
it
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
|.
z
: ( ( ) ( )
set
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
sin
it
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) &
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
it
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) &
it
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) )
if
z
: ( ( ) ( )
set
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
otherwise
it
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
end;
theorem
:: COMPTRIG:34
for
z
being ( (
complex
) (
complex
)
number
) holds
(
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
) &
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
)
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ) ;
theorem
:: COMPTRIG:35
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Arg
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Real
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:36
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Arg
x
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Real
)
=
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:37
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Arg
(
x
: ( ( ) (
complex
real
ext-real
)
Real
)
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
real
ext-real
)
Real
)
=
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:38
for
x
being ( ( ) (
complex
real
ext-real
)
Real
) st
x
: ( ( ) (
complex
real
ext-real
)
Real
)
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
Arg
(
x
: ( ( ) (
complex
real
ext-real
)
Real
)
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
real
ext-real
)
Real
)
=
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:39
Arg
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
)
Real
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:40
Arg
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
)
Real
)
=
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:41
for
z
being ( (
complex
) (
complex
)
number
) holds
(
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
)
in
].
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) iff (
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: COMPTRIG:42
for
z
being ( (
complex
) (
complex
)
number
) holds
(
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
)
in
].
(
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) iff (
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: COMPTRIG:43
for
z
being ( (
complex
) (
complex
)
number
) holds
(
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
)
in
].
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) iff (
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: COMPTRIG:44
for
z
being ( (
complex
) (
complex
)
number
) holds
(
Arg
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Real
)
in
].
(
(
3 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( non
empty
complex
real
ext-real
positive
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) ,
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
.[
: ( ( ) (
V70
()
V71
()
V72
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) iff (
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) ;
theorem
:: COMPTRIG:45
for
z
being ( (
complex
) (
complex
)
number
) st
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sin
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:46
for
z
being ( (
complex
) (
complex
)
number
) st
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sin
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:47
for
z
being ( (
complex
) (
complex
)
number
) st
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sin
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:48
for
z
being ( (
complex
) (
complex
)
number
) st
Im
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sin
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:49
for
z
being ( (
complex
) (
complex
)
number
) st
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
cos
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:50
for
z
being ( (
complex
) (
complex
)
number
) st
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
cos
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:51
for
z
being ( (
complex
) (
complex
)
number
) st
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
cos
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
>=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:52
for
z
being ( (
complex
) (
complex
)
number
) st
Re
z
: ( (
complex
) (
complex
)
number
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) &
z
: ( (
complex
) (
complex
)
number
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
cos
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
) : ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
<=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:53
for
x
being ( (
real
) (
complex
real
ext-real
)
number
)
for
n
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) holds
(
(
cos
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
+
(
(
sin
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) : ( ( ) (
complex
)
set
)
=
(
cos
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
*
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
+
(
(
sin
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
*
x
: ( (
real
) (
complex
real
ext-real
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
)
: ( ( ) (
complex
real
ext-real
)
set
)
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: COMPTRIG:54
for
z
being ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
for
n
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) st (
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) or
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) : ( ( ) (
complex
)
set
)
=
(
(
|.
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
cos
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
*
(
Arg
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
(
|.
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
sin
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
*
(
Arg
z
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: COMPTRIG:55
for
x
being ( ( ) (
complex
real
ext-real
)
Real
)
for
n
,
k
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) st
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
cos
(
(
x
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
sin
(
(
x
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) : ( ( ) (
complex
)
set
)
=
(
cos
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
sin
x
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;
theorem
:: COMPTRIG:56
for
z
being ( (
complex
) (
complex
)
number
)
for
n
,
k
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) st
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
<>
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
z
: ( (
complex
) (
complex
)
number
)
=
(
(
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
-root
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
cos
(
(
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
(
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
-root
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
sin
(
(
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
)
)
: ( ( ) (
complex
)
set
)
|^
n
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) : ( ( ) (
complex
)
set
) ;
definition
let
x
be ( (
complex
) (
complex
)
number
) ;
let
n
be ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ;
mode
CRoot
of
n
,
x
->
( (
complex
) (
complex
)
number
)
means
:: COMPTRIG:def 2
it
: ( ( ) ( )
set
)
|^
n
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) : ( ( ) ( )
set
)
=
x
: ( ( ) ( )
set
) ;
end;
theorem
:: COMPTRIG:57
for
x
being ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
for
n
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
for
k
being ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
) holds
(
(
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
-root
|.
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
cos
(
(
(
Arg
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
(
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
-root
|.
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
sin
(
(
(
Arg
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Real
)
+
(
(
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
k
: ( (
natural
) (
ordinal
natural
complex
real
ext-real
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
/
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) is ( ( ) (
complex
)
CRoot
of
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ,
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) ) ;
theorem
:: COMPTRIG:58
for
x
being ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
for
v
being ( ( ) (
complex
)
CRoot
of 1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) ) holds
v
: ( ( ) (
complex
)
CRoot
of 1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
b
1
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) )
=
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) ;
theorem
:: COMPTRIG:59
for
n
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
for
v
being ( ( ) (
complex
)
CRoot
of
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ,
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ) holds
v
: ( ( ) (
complex
)
CRoot
of
b
1
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ,
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) )
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:60
for
n
being ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
)
for
x
being ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
for
v
being ( ( ) (
complex
)
CRoot
of
n
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ,
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) ) st
v
: ( ( ) (
complex
)
CRoot
of
b
1
: ( ( non
empty
natural
) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
)
Nat
) ,
b
2
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) ) )
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
x
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:61
for
a
being ( (
real
) (
complex
real
ext-real
)
number
) st
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
a
: ( (
real
) (
complex
real
ext-real
)
number
) &
a
: ( (
real
) (
complex
real
ext-real
)
number
)
<
2 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) )
*
PI
: ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) (
complex
real
ext-real
non
negative
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) &
cos
a
: ( (
real
) (
complex
real
ext-real
)
number
) : ( ( ) (
complex
real
ext-real
)
set
)
=
1 : ( ( ) ( non
empty
ordinal
natural
complex
real
ext-real
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
a
: ( (
real
) (
complex
real
ext-real
)
number
)
=
0
: ( ( ) (
Function-like
functional
empty
ordinal
natural
complex
real
ext-real
non
positive
non
negative
V56
()
V69
()
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
NAT
: ( ( ) (
V70
()
V71
()
V72
()
V73
()
V74
()
V75
()
V76
() )
Element
of
K19
(
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: COMPTRIG:62
for
z
being ( (
complex
) (
complex
)
number
) holds
z
: ( (
complex
) (
complex
)
number
)
=
(
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
cos
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
+
(
(
|.
z
: ( (
complex
) (
complex
)
number
)
.|
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
(
sin
(
Arg
z
: ( (
complex
) (
complex
)
number
)
)
: ( ( ) (
complex
real
ext-real
)
Real
)
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
)
: ( ( ) (
complex
real
ext-real
)
Element
of
REAL
: ( ( ) ( non
empty
V58
()
V70
()
V71
()
V72
()
V76
() )
set
) )
*
<i>
: ( ( ) (
complex
)
Element
of
COMPLEX
: ( ( ) ( non
empty
V58
()
V70
()
V76
() )
set
) )
)
: ( ( ) (
complex
)
set
) : ( ( ) (
complex
)
set
) ;