:: FDIFF_7 semantic presentation

REAL is V11() V49() V50() V51() V55() V70() set
NAT is V49() V50() V51() V52() V53() V54() V55() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V11() V49() V55() V70() set
0 is set
1 is V11() V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
{0,1} is set
K20(REAL,REAL) is V39() V40() V41() set
K19(K20(REAL,REAL)) is set
K20(NAT,REAL) is V39() V40() V41() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V39() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V39() set
K19(K20(COMPLEX,COMPLEX)) is set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
RAT is V11() V49() V50() V51() V52() V55() V70() set
INT is V11() V49() V50() V51() V52() V53() V55() V70() set
NAT is V49() V50() V51() V52() V53() V54() V55() set
K19(NAT) is set
K19(NAT) is set
arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- 1 is V22() V23() ext-real V68() Element of REAL
].(- 1),1.[ is open V49() V50() V51() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= - 1 & not 1 <= b₁ ) } is set
arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
0 is V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
exp_R is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
[#] REAL is V49() V50() V51() Element of K19(REAL)
dom exp_R is V49() V50() V51() Element of K19(REAL)
rng exp_R is V49() V50() V51() Element of K19(REAL)
right_open_halfline 0 is V49() V50() V51() Element of K19(REAL)
+infty is set
K88(0,+infty) is set
ln is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
exp_R " is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ln is V49() V50() V51() Element of K19(REAL)
rng ln is V49() V50() V51() Element of K19(REAL)
2 is V11() V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
#Z 2 is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
cos is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
cos ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
sin is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
sin ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
{0} is V49() V50() V51() V52() V53() V54() set
Z is V22() V23() ext-real Element of REAL
Z #Z 2 is V22() V23() ext-real Element of REAL
Z ^2 is V22() V23() ext-real Element of REAL
K57(Z,Z) is set
Z |^ 2 is V22() V23() ext-real Element of REAL
1 / 2 is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z #R (1 / 2) is V22() V23() ext-real Element of REAL
sqrt Z is V22() V23() ext-real Element of REAL
(1 / 2) * 2 is V22() V23() ext-real Element of REAL
Z #R ((1 / 2) * 2) is V22() V23() ext-real Element of REAL
(Z #R (1 / 2)) #R 2 is V22() V23() ext-real Element of REAL
(Z #R (1 / 2)) #Q 2 is V22() V23() ext-real Element of REAL
(Z #R (1 / 2)) to_power 2 is V22() V23() ext-real Element of REAL
(Z #R (1 / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((Z #R (1 / 2)),(Z #R (1 / 2))) is set
- (1 / 2) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
sqrt Z is V22() V23() ext-real Element of REAL
1 / (sqrt Z) is V22() V23() ext-real Element of REAL
Z #R (1 / 2) is V22() V23() ext-real Element of REAL
1 / (Z #R (1 / 2)) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z / 2 is V22() V23() ext-real Element of REAL
cos . (Z / 2) is V22() V23() ext-real Element of REAL
(cos . (Z / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (Z / 2)),(cos . (Z / 2))) is set
2 * ((cos . (Z / 2)) ^2) is V22() V23() ext-real Element of REAL
cos . Z is V22() V23() ext-real Element of REAL
1 + (cos . Z) is V22() V23() ext-real Element of REAL
cos (Z / 2) is V22() V23() ext-real Element of REAL
(cos (Z / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((cos (Z / 2)),(cos (Z / 2))) is set
2 * (Z / 2) is V22() V23() ext-real Element of REAL
cos (2 * (Z / 2)) is V22() V23() ext-real Element of REAL
1 + (cos (2 * (Z / 2))) is V22() V23() ext-real Element of REAL
(1 + (cos (2 * (Z / 2)))) / 2 is V22() V23() ext-real Element of REAL
cos Z is V22() V23() ext-real Element of REAL
1 + (cos Z) is V22() V23() ext-real Element of REAL
(1 + (cos Z)) / 2 is V22() V23() ext-real Element of REAL
2 * ((1 + (cos Z)) / 2) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z / 2 is V22() V23() ext-real Element of REAL
sin . (Z / 2) is V22() V23() ext-real Element of REAL
(sin . (Z / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (Z / 2)),(sin . (Z / 2))) is set
2 * ((sin . (Z / 2)) ^2) is V22() V23() ext-real Element of REAL
cos . Z is V22() V23() ext-real Element of REAL
1 - (cos . Z) is V22() V23() ext-real Element of REAL
sin (Z / 2) is V22() V23() ext-real Element of REAL
(sin (Z / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((sin (Z / 2)),(sin (Z / 2))) is set
2 * (Z / 2) is V22() V23() ext-real Element of REAL
cos (2 * (Z / 2)) is V22() V23() ext-real Element of REAL
1 - (cos (2 * (Z / 2))) is V22() V23() ext-real Element of REAL
(1 - (cos (2 * (Z / 2)))) / 2 is V22() V23() ext-real Element of REAL
cos Z is V22() V23() ext-real Element of REAL
1 - (cos Z) is V22() V23() ext-real Element of REAL
(1 - (cos Z)) / 2 is V22() V23() ext-real Element of REAL
2 * ((1 - (cos Z)) / 2) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z (#) arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (Z (#) arcsin) is V49() V50() V51() Element of K19(REAL)
f is open V49() V50() V51() Element of K19(REAL)
(Z (#) arcsin) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
((Z (#) arcsin) `| f) . x is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
diff (arcsin,x) is V22() V23() ext-real Element of REAL
Z * (diff (arcsin,x)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
Z * (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((Z (#) arcsin) `| f) . x is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z (#) arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (Z (#) arccos) is V49() V50() V51() Element of K19(REAL)
f is open V49() V50() V51() Element of K19(REAL)
(Z (#) arccos) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
((Z (#) arccos) `| f) . x is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- (Z / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
diff (arccos,x) is V22() V23() ext-real Element of REAL
Z * (diff (arccos,x)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
Z * (- (1 / (sqrt (1 - (x ^2))))) is V22() V23() ext-real Element of REAL
Z * (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
- (Z * (1 / (sqrt (1 - (x ^2))))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((Z (#) arccos) `| f) . x is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- (Z / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f . Z is V22() V23() ext-real Element of REAL
arcsin * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
diff ((arcsin * f),Z) is V22() V23() ext-real Element of REAL
diff (f,Z) is V22() V23() ext-real Element of REAL
(f . Z) ^2 is V22() V23() ext-real Element of REAL
K57((f . Z),(f . Z)) is set
1 - ((f . Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f . Z) ^2)) is V22() V23() ext-real Element of REAL
(diff (f,Z)) / (sqrt (1 - ((f . Z) ^2))) is V22() V23() ext-real Element of REAL
diff (arcsin,(f . Z)) is V22() V23() ext-real Element of REAL
(diff (arcsin,(f . Z))) * (diff (f,Z)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((f . Z) ^2))) is V22() V23() ext-real Element of REAL
(diff (f,Z)) * (1 / (sqrt (1 - ((f . Z) ^2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f . Z is V22() V23() ext-real Element of REAL
arccos * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
diff ((arccos * f),Z) is V22() V23() ext-real Element of REAL
diff (f,Z) is V22() V23() ext-real Element of REAL
(f . Z) ^2 is V22() V23() ext-real Element of REAL
K57((f . Z),(f . Z)) is set
1 - ((f . Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f . Z) ^2)) is V22() V23() ext-real Element of REAL
(diff (f,Z)) / (sqrt (1 - ((f . Z) ^2))) is V22() V23() ext-real Element of REAL
- ((diff (f,Z)) / (sqrt (1 - ((f . Z) ^2)))) is V22() V23() ext-real Element of REAL
diff (arccos,(f . Z)) is V22() V23() ext-real Element of REAL
(diff (arccos,(f . Z))) * (diff (f,Z)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((f . Z) ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - ((f . Z) ^2)))) is V22() V23() ext-real Element of REAL
(- (1 / (sqrt (1 - ((f . Z) ^2))))) * (diff (f,Z)) is V22() V23() ext-real Element of REAL
(diff (f,Z)) * (1 / (sqrt (1 - ((f . Z) ^2)))) is V22() V23() ext-real Element of REAL
- ((diff (f,Z)) * (1 / (sqrt (1 - ((f . Z) ^2))))) is V22() V23() ext-real Element of REAL
ln * arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (ln * arcsin) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(ln * arcsin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((ln * arcsin) `| Z) . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
(sqrt (1 - (f ^2))) * (arcsin . f) is V22() V23() ext-real Element of REAL
1 / ((sqrt (1 - (f ^2))) * (arcsin . f)) is V22() V23() ext-real Element of REAL
diff ((ln * arcsin),f) is V22() V23() ext-real Element of REAL
diff (arcsin,f) is V22() V23() ext-real Element of REAL
(diff (arcsin,f)) / (arcsin . f) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(1 / (sqrt (1 - (f ^2)))) / (arcsin . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((ln * arcsin) `| Z) . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
(sqrt (1 - (f ^2))) * (arcsin . f) is V22() V23() ext-real Element of REAL
1 / ((sqrt (1 - (f ^2))) * (arcsin . f)) is V22() V23() ext-real Element of REAL
ln * arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (ln * arccos) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(ln * arccos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((ln * arccos) `| Z) . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
(sqrt (1 - (f ^2))) * (arccos . f) is V22() V23() ext-real Element of REAL
1 / ((sqrt (1 - (f ^2))) * (arccos . f)) is V22() V23() ext-real Element of REAL
- (1 / ((sqrt (1 - (f ^2))) * (arccos . f))) is V22() V23() ext-real Element of REAL
diff ((ln * arccos),f) is V22() V23() ext-real Element of REAL
diff (arccos,f) is V22() V23() ext-real Element of REAL
(diff (arccos,f)) / (arccos . f) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
(- (1 / (sqrt (1 - (f ^2))))) / (arccos . f) is V22() V23() ext-real Element of REAL
(1 / (sqrt (1 - (f ^2)))) / (arccos . f) is V22() V23() ext-real Element of REAL
- ((1 / (sqrt (1 - (f ^2)))) / (arccos . f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((ln * arccos) `| Z) . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
(sqrt (1 - (f ^2))) * (arccos . f) is V22() V23() ext-real Element of REAL
1 / ((sqrt (1 - (f ^2))) * (arccos . f)) is V22() V23() ext-real Element of REAL
- (1 / ((sqrt (1 - (f ^2))) * (arccos . f))) is V22() V23() ext-real Element of REAL
Z is V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
#Z Z is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
(#Z Z) * arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z Z) * arcsin) is V49() V50() V51() Element of K19(REAL)
Z - 1 is V22() V23() ext-real V68() Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
((#Z Z) * arcsin) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((#Z Z) * arcsin) `| f) . x is V22() V23() ext-real Element of REAL
arcsin . x is V22() V23() ext-real Element of REAL
(arcsin . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * ((arcsin . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
(Z * ((arcsin . x) #Z (Z - 1))) / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
diff (((#Z Z) * arcsin),x) is V22() V23() ext-real Element of REAL
diff (arcsin,x) is V22() V23() ext-real Element of REAL
(Z * ((arcsin . x) #Z (Z - 1))) * (diff (arcsin,x)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
(Z * ((arcsin . x) #Z (Z - 1))) * (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((#Z Z) * arcsin) `| f) . x is V22() V23() ext-real Element of REAL
arcsin . x is V22() V23() ext-real Element of REAL
(arcsin . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * ((arcsin . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
(Z * ((arcsin . x) #Z (Z - 1))) / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
Z is V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
#Z Z is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
(#Z Z) * arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z Z) * arccos) is V49() V50() V51() Element of K19(REAL)
Z - 1 is V22() V23() ext-real V68() Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
((#Z Z) * arccos) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((#Z Z) * arccos) `| f) . x is V22() V23() ext-real Element of REAL
arccos . x is V22() V23() ext-real Element of REAL
(arccos . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * ((arccos . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
(Z * ((arccos . x) #Z (Z - 1))) / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- ((Z * ((arccos . x) #Z (Z - 1))) / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
diff (((#Z Z) * arccos),x) is V22() V23() ext-real Element of REAL
diff (arccos,x) is V22() V23() ext-real Element of REAL
(Z * ((arccos . x) #Z (Z - 1))) * (diff (arccos,x)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
(Z * ((arccos . x) #Z (Z - 1))) * (- (1 / (sqrt (1 - (x ^2))))) is V22() V23() ext-real Element of REAL
(Z * ((arccos . x) #Z (Z - 1))) * (1 / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
- ((Z * ((arccos . x) #Z (Z - 1))) * (1 / (sqrt (1 - (x ^2))))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((#Z Z) * arccos) `| f) . x is V22() V23() ext-real Element of REAL
arccos . x is V22() V23() ext-real Element of REAL
(arccos . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * ((arccos . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 - (x ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (x ^2)) is V22() V23() ext-real Element of REAL
(Z * ((arccos . x) #Z (Z - 1))) / (sqrt (1 - (x ^2))) is V22() V23() ext-real Element of REAL
- ((Z * ((arccos . x) #Z (Z - 1))) / (sqrt (1 - (x ^2)))) is V22() V23() ext-real Element of REAL
(#Z 2) * arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(1 / 2) (#) ((#Z 2) * arcsin) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) ((#Z 2) * arcsin)) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
((1 / 2) (#) ((#Z 2) * arcsin)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z 2) * arcsin) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
(((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . f is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
(arcsin . f) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
diff (((#Z 2) * arcsin),f) is V22() V23() ext-real Element of REAL
(1 / 2) * (diff (((#Z 2) * arcsin),f)) is V22() V23() ext-real Element of REAL
((#Z 2) * arcsin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#Z 2) * arcsin) `| Z) . f is V22() V23() ext-real Element of REAL
(1 / 2) * ((((#Z 2) * arcsin) `| Z) . f) is V22() V23() ext-real Element of REAL
2 - 1 is V22() V23() ext-real V68() Element of REAL
(arcsin . f) #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * ((arcsin . f) #Z (2 - 1)) is V22() V23() ext-real Element of REAL
(2 * ((arcsin . f) #Z (2 - 1))) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(1 / 2) * ((2 * ((arcsin . f) #Z (2 - 1))) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
(1 / 2) * (2 * ((arcsin . f) #Z (2 - 1))) is V22() V23() ext-real Element of REAL
((1 / 2) * (2 * ((arcsin . f) #Z (2 - 1)))) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . f is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
(arcsin . f) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(#Z 2) * arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(1 / 2) (#) ((#Z 2) * arccos) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) ((#Z 2) * arccos)) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
((1 / 2) (#) ((#Z 2) * arccos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z 2) * arccos) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
(((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . f is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
(arccos . f) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- ((arccos . f) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
diff (((#Z 2) * arccos),f) is V22() V23() ext-real Element of REAL
(1 / 2) * (diff (((#Z 2) * arccos),f)) is V22() V23() ext-real Element of REAL
((#Z 2) * arccos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#Z 2) * arccos) `| Z) . f is V22() V23() ext-real Element of REAL
(1 / 2) * ((((#Z 2) * arccos) `| Z) . f) is V22() V23() ext-real Element of REAL
2 - 1 is V22() V23() ext-real V68() Element of REAL
(arccos . f) #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * ((arccos . f) #Z (2 - 1)) is V22() V23() ext-real Element of REAL
(2 * ((arccos . f) #Z (2 - 1))) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- ((2 * ((arccos . f) #Z (2 - 1))) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
(1 / 2) * (- ((2 * ((arccos . f) #Z (2 - 1))) / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
(1 / 2) * ((2 * ((arccos . f) #Z (2 - 1))) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
- ((1 / 2) * ((2 * ((arccos . f) #Z (2 - 1))) / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
(1 / 2) * (2 * ((arccos . f) #Z (2 - 1))) is V22() V23() ext-real Element of REAL
((1 / 2) * (2 * ((arccos . f) #Z (2 - 1)))) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- (((1 / 2) * (2 * ((arccos . f) #Z (2 - 1)))) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . f is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
(arccos . f) / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- ((arccos . f) / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arcsin * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (arcsin * f) is V49() V50() V51() Element of K19(REAL)
(arcsin * f) `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom f is V49() V50() V51() Element of K19(REAL)
f1 is set
f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((arcsin * f) `| x) . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
((Z * f1) + f) ^2 is V22() V23() ext-real Element of REAL
K57(((Z * f1) + f),((Z * f1) + f)) is set
1 - (((Z * f1) + f) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((Z * f1) + f) ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (((Z * f1) + f) ^2))) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
diff ((arcsin * f),f1) is V22() V23() ext-real Element of REAL
diff (f,f1) is V22() V23() ext-real Element of REAL
(f . f1) ^2 is V22() V23() ext-real Element of REAL
K57((f . f1),(f . f1)) is set
1 - ((f . f1) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f . f1) ^2)) is V22() V23() ext-real Element of REAL
(diff (f,f1)) / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
f `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| x) . f1 is V22() V23() ext-real Element of REAL
((f `| x) . f1) / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((arcsin * f) `| x) . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
((Z * f1) + f) ^2 is V22() V23() ext-real Element of REAL
K57(((Z * f1) + f),((Z * f1) + f)) is set
1 - (((Z * f1) + f) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((Z * f1) + f) ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (((Z * f1) + f) ^2))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arccos * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (arccos * f) is V49() V50() V51() Element of K19(REAL)
(arccos * f) `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom f is V49() V50() V51() Element of K19(REAL)
f1 is set
f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((arccos * f) `| x) . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
((Z * f1) + f) ^2 is V22() V23() ext-real Element of REAL
K57(((Z * f1) + f),((Z * f1) + f)) is set
1 - (((Z * f1) + f) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((Z * f1) + f) ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (((Z * f1) + f) ^2))) is V22() V23() ext-real Element of REAL
- (Z / (sqrt (1 - (((Z * f1) + f) ^2)))) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
diff ((arccos * f),f1) is V22() V23() ext-real Element of REAL
diff (f,f1) is V22() V23() ext-real Element of REAL
(f . f1) ^2 is V22() V23() ext-real Element of REAL
K57((f . f1),(f . f1)) is set
1 - ((f . f1) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f . f1) ^2)) is V22() V23() ext-real Element of REAL
(diff (f,f1)) / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
- ((diff (f,f1)) / (sqrt (1 - ((f . f1) ^2)))) is V22() V23() ext-real Element of REAL
f `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| x) . f1 is V22() V23() ext-real Element of REAL
((f `| x) . f1) / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
- (((f `| x) . f1) / (sqrt (1 - ((f . f1) ^2)))) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - ((f . f1) ^2))) is V22() V23() ext-real Element of REAL
- (Z / (sqrt (1 - ((f . f1) ^2)))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((arccos * f) `| x) . f1 is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
((Z * f1) + f) ^2 is V22() V23() ext-real Element of REAL
K57(((Z * f1) + f),((Z * f1) + f)) is set
1 - (((Z * f1) + f) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((Z * f1) + f) ^2)) is V22() V23() ext-real Element of REAL
Z / (sqrt (1 - (((Z * f1) + f) ^2))) is V22() V23() ext-real Element of REAL
- (Z / (sqrt (1 - (((Z * f1) + f) ^2)))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) (#) arcsin) is V49() V50() V51() Element of K19(REAL)
((id Z) (#) arcsin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
(id Z) . f is V22() V23() ext-real Element of REAL
1 * f is V22() V23() ext-real Element of REAL
(1 * f) + 0 is V22() V23() ext-real Element of REAL
dom (id Z) is V49() V50() V51() Element of K19(REAL)
dom arcsin is V49() V50() V51() Element of K19(REAL)
(dom (id Z)) /\ (dom arcsin) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
(((id Z) (#) arcsin) `| Z) . f is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
f / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(arcsin . f) + (f / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
diff ((id Z),f) is V22() V23() ext-real Element of REAL
(arcsin . f) * (diff ((id Z),f)) is V22() V23() ext-real Element of REAL
(id Z) . f is V22() V23() ext-real Element of REAL
diff (arcsin,f) is V22() V23() ext-real Element of REAL
((id Z) . f) * (diff (arcsin,f)) is V22() V23() ext-real Element of REAL
((arcsin . f) * (diff ((id Z),f))) + (((id Z) . f) * (diff (arcsin,f))) is V22() V23() ext-real Element of REAL
(id Z) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) `| Z) . f is V22() V23() ext-real Element of REAL
(arcsin . f) * (((id Z) `| Z) . f) is V22() V23() ext-real Element of REAL
((arcsin . f) * (((id Z) `| Z) . f)) + (((id Z) . f) * (diff (arcsin,f))) is V22() V23() ext-real Element of REAL
(arcsin . f) * 1 is V22() V23() ext-real Element of REAL
((arcsin . f) * 1) + (((id Z) . f) * (diff (arcsin,f))) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
((id Z) . f) * (1 / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
((arcsin . f) * 1) + (((id Z) . f) * (1 / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
f * (1 / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
(arcsin . f) + (f * (1 / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id Z) (#) arcsin) `| Z) . f is V22() V23() ext-real Element of REAL
arcsin . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
f / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(arcsin . f) + (f / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) (#) arccos) is V49() V50() V51() Element of K19(REAL)
((id Z) (#) arccos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
(id Z) . f is V22() V23() ext-real Element of REAL
1 * f is V22() V23() ext-real Element of REAL
(1 * f) + 0 is V22() V23() ext-real Element of REAL
dom (id Z) is V49() V50() V51() Element of K19(REAL)
dom arccos is V49() V50() V51() Element of K19(REAL)
(dom (id Z)) /\ (dom arccos) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
(((id Z) (#) arccos) `| Z) . f is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
f / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(arccos . f) - (f / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
diff ((id Z),f) is V22() V23() ext-real Element of REAL
(arccos . f) * (diff ((id Z),f)) is V22() V23() ext-real Element of REAL
(id Z) . f is V22() V23() ext-real Element of REAL
diff (arccos,f) is V22() V23() ext-real Element of REAL
((id Z) . f) * (diff (arccos,f)) is V22() V23() ext-real Element of REAL
((arccos . f) * (diff ((id Z),f))) + (((id Z) . f) * (diff (arccos,f))) is V22() V23() ext-real Element of REAL
(id Z) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) `| Z) . f is V22() V23() ext-real Element of REAL
(arccos . f) * (((id Z) `| Z) . f) is V22() V23() ext-real Element of REAL
((arccos . f) * (((id Z) `| Z) . f)) + (((id Z) . f) * (diff (arccos,f))) is V22() V23() ext-real Element of REAL
(arccos . f) * 1 is V22() V23() ext-real Element of REAL
((arccos . f) * 1) + (((id Z) . f) * (diff (arccos,f))) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
((id Z) . f) * (- (1 / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
((arccos . f) * 1) + (((id Z) . f) * (- (1 / (sqrt (1 - (f ^2)))))) is V22() V23() ext-real Element of REAL
f * (- (1 / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
(arccos . f) + (f * (- (1 / (sqrt (1 - (f ^2)))))) is V22() V23() ext-real Element of REAL
f * (1 / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
(arccos . f) - (f * (1 / (sqrt (1 - (f ^2))))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id Z) (#) arccos) `| Z) . f is V22() V23() ext-real Element of REAL
arccos . f is V22() V23() ext-real Element of REAL
f ^2 is V22() V23() ext-real Element of REAL
K57(f,f) is set
1 - (f ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f ^2)) is V22() V23() ext-real Element of REAL
f / (sqrt (1 - (f ^2))) is V22() V23() ext-real Element of REAL
(arccos . f) - (f / (sqrt (1 - (f ^2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f (#) arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (f (#) arcsin) is V49() V50() V51() Element of K19(REAL)
(f (#) arcsin) `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom f is V49() V50() V51() Element of K19(REAL)
dom arcsin is V49() V50() V51() Element of K19(REAL)
(dom f) /\ (dom arcsin) is V49() V50() V51() Element of K19(REAL)
f1 is V22() V23() ext-real Element of REAL
((f (#) arcsin) `| x) . f1 is V22() V23() ext-real Element of REAL
arcsin . f1 is V22() V23() ext-real Element of REAL
Z * (arcsin . f1) is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
((Z * f1) + f) / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(Z * (arcsin . f1)) + (((Z * f1) + f) / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
diff (f,f1) is V22() V23() ext-real Element of REAL
(arcsin . f1) * (diff (f,f1)) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
diff (arcsin,f1) is V22() V23() ext-real Element of REAL
(f . f1) * (diff (arcsin,f1)) is V22() V23() ext-real Element of REAL
((arcsin . f1) * (diff (f,f1))) + ((f . f1) * (diff (arcsin,f1))) is V22() V23() ext-real Element of REAL
f `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| x) . f1 is V22() V23() ext-real Element of REAL
(arcsin . f1) * ((f `| x) . f1) is V22() V23() ext-real Element of REAL
((arcsin . f1) * ((f `| x) . f1)) + ((f . f1) * (diff (arcsin,f1))) is V22() V23() ext-real Element of REAL
(arcsin . f1) * Z is V22() V23() ext-real Element of REAL
((arcsin . f1) * Z) + ((f . f1) * (diff (arcsin,f1))) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(f . f1) * (1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
((arcsin . f1) * Z) + ((f . f1) * (1 / (sqrt (1 - (f1 ^2))))) is V22() V23() ext-real Element of REAL
((Z * f1) + f) * (1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
(Z * (arcsin . f1)) + (((Z * f1) + f) * (1 / (sqrt (1 - (f1 ^2))))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((f (#) arcsin) `| x) . f1 is V22() V23() ext-real Element of REAL
arcsin . f1 is V22() V23() ext-real Element of REAL
Z * (arcsin . f1) is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
((Z * f1) + f) / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(Z * (arcsin . f1)) + (((Z * f1) + f) / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f (#) arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (f (#) arccos) is V49() V50() V51() Element of K19(REAL)
(f (#) arccos) `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom f is V49() V50() V51() Element of K19(REAL)
dom arccos is V49() V50() V51() Element of K19(REAL)
(dom f) /\ (dom arccos) is V49() V50() V51() Element of K19(REAL)
f1 is V22() V23() ext-real Element of REAL
((f (#) arccos) `| x) . f1 is V22() V23() ext-real Element of REAL
arccos . f1 is V22() V23() ext-real Element of REAL
Z * (arccos . f1) is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
((Z * f1) + f) / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(Z * (arccos . f1)) - (((Z * f1) + f) / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
diff (f,f1) is V22() V23() ext-real Element of REAL
(arccos . f1) * (diff (f,f1)) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
diff (arccos,f1) is V22() V23() ext-real Element of REAL
(f . f1) * (diff (arccos,f1)) is V22() V23() ext-real Element of REAL
((arccos . f1) * (diff (f,f1))) + ((f . f1) * (diff (arccos,f1))) is V22() V23() ext-real Element of REAL
f `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| x) . f1 is V22() V23() ext-real Element of REAL
(arccos . f1) * ((f `| x) . f1) is V22() V23() ext-real Element of REAL
((arccos . f1) * ((f `| x) . f1)) + ((f . f1) * (diff (arccos,f1))) is V22() V23() ext-real Element of REAL
(arccos . f1) * Z is V22() V23() ext-real Element of REAL
((arccos . f1) * Z) + ((f . f1) * (diff (arccos,f1))) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
(f . f1) * (- (1 / (sqrt (1 - (f1 ^2))))) is V22() V23() ext-real Element of REAL
((arccos . f1) * Z) + ((f . f1) * (- (1 / (sqrt (1 - (f1 ^2)))))) is V22() V23() ext-real Element of REAL
(f . f1) * (1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
((arccos . f1) * Z) - ((f . f1) * (1 / (sqrt (1 - (f1 ^2))))) is V22() V23() ext-real Element of REAL
((Z * f1) + f) * (1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
(Z * (arccos . f1)) - (((Z * f1) + f) * (1 / (sqrt (1 - (f1 ^2))))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((f (#) arccos) `| x) . f1 is V22() V23() ext-real Element of REAL
arccos . f1 is V22() V23() ext-real Element of REAL
Z * (arccos . f1) is V22() V23() ext-real Element of REAL
Z * f1 is V22() V23() ext-real Element of REAL
(Z * f1) + f is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
((Z * f1) + f) / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(Z * (arccos . f1)) - (((Z * f1) + f) / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arcsin * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(1 / 2) (#) (arcsin * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) (arcsin * f)) is V49() V50() V51() Element of K19(REAL)
((1 / 2) (#) (arcsin * f)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (arcsin * f) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) + 0 is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((1 / 2) (#) (arcsin * f)) `| Z) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) ^2 is V22() V23() ext-real Element of REAL
K57((2 * x),(2 * x)) is set
1 - ((2 * x) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((2 * x) ^2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
diff ((arcsin * f),x) is V22() V23() ext-real Element of REAL
(1 / 2) * (diff ((arcsin * f),x)) is V22() V23() ext-real Element of REAL
(arcsin * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((arcsin * f) `| Z) . x is V22() V23() ext-real Element of REAL
(1 / 2) * (((arcsin * f) `| Z) . x) is V22() V23() ext-real Element of REAL
(2 * x) + 0 is V22() V23() ext-real Element of REAL
((2 * x) + 0) ^2 is V22() V23() ext-real Element of REAL
K57(((2 * x) + 0),((2 * x) + 0)) is set
1 - (((2 * x) + 0) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((2 * x) + 0) ^2)) is V22() V23() ext-real Element of REAL
2 / (sqrt (1 - (((2 * x) + 0) ^2))) is V22() V23() ext-real Element of REAL
(1 / 2) * (2 / (sqrt (1 - (((2 * x) + 0) ^2)))) is V22() V23() ext-real Element of REAL
(1 / 2) * 2 is V22() V23() ext-real Element of REAL
((1 / 2) * 2) / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((1 / 2) (#) (arcsin * f)) `| Z) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) ^2 is V22() V23() ext-real Element of REAL
K57((2 * x),(2 * x)) is set
1 - ((2 * x) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((2 * x) ^2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arccos * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(1 / 2) (#) (arccos * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((1 / 2) (#) (arccos * f)) is V49() V50() V51() Element of K19(REAL)
((1 / 2) (#) (arccos * f)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (arccos * f) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) + 0 is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((1 / 2) (#) (arccos * f)) `| Z) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) ^2 is V22() V23() ext-real Element of REAL
K57((2 * x),(2 * x)) is set
1 - ((2 * x) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((2 * x) ^2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - ((2 * x) ^2)))) is V22() V23() ext-real Element of REAL
diff ((arccos * f),x) is V22() V23() ext-real Element of REAL
(1 / 2) * (diff ((arccos * f),x)) is V22() V23() ext-real Element of REAL
(arccos * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((arccos * f) `| Z) . x is V22() V23() ext-real Element of REAL
(1 / 2) * (((arccos * f) `| Z) . x) is V22() V23() ext-real Element of REAL
(2 * x) + 0 is V22() V23() ext-real Element of REAL
((2 * x) + 0) ^2 is V22() V23() ext-real Element of REAL
K57(((2 * x) + 0),((2 * x) + 0)) is set
1 - (((2 * x) + 0) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (((2 * x) + 0) ^2)) is V22() V23() ext-real Element of REAL
2 / (sqrt (1 - (((2 * x) + 0) ^2))) is V22() V23() ext-real Element of REAL
- (2 / (sqrt (1 - (((2 * x) + 0) ^2)))) is V22() V23() ext-real Element of REAL
(1 / 2) * (- (2 / (sqrt (1 - (((2 * x) + 0) ^2))))) is V22() V23() ext-real Element of REAL
2 / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
(1 / 2) * (2 / (sqrt (1 - ((2 * x) ^2)))) is V22() V23() ext-real Element of REAL
- ((1 / 2) * (2 / (sqrt (1 - ((2 * x) ^2))))) is V22() V23() ext-real Element of REAL
(1 / 2) * 2 is V22() V23() ext-real Element of REAL
((1 / 2) * 2) / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
- (((1 / 2) * 2) / (sqrt (1 - ((2 * x) ^2)))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((1 / 2) (#) (arccos * f)) `| Z) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
(2 * x) ^2 is V22() V23() ext-real Element of REAL
K57((2 * x),(2 * x)) is set
1 - ((2 * x) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((2 * x) ^2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - ((2 * x) ^2))) is V22() V23() ext-real Element of REAL
- (1 / (sqrt (1 - ((2 * x) ^2)))) is V22() V23() ext-real Element of REAL
#R (1 / 2) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
Z is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#R (1 / 2)) * f) is V49() V50() V51() Element of K19(REAL)
((#R (1 / 2)) * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x - f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) f is V1() V6() set
x + (- f) is V1() V6() set
dom f is V49() V50() V51() Element of K19(REAL)
f1 is set
(- 1) (#) f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x + ((- 1) (#) f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x + ((- 1) (#) f)) is V49() V50() V51() Element of K19(REAL)
f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
0 * f1 is V22() V23() ext-real Element of REAL
1 + (0 * f1) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
(((#R (1 / 2)) * f) `| Z) . f1 is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
dom (x - f) is V49() V50() V51() Element of K19(REAL)
(x - f) . f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
(x . f1) - (f . f1) is V22() V23() ext-real Element of REAL
1 - (f . f1) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * f),f1) is V22() V23() ext-real Element of REAL
(1 / 2) - 1 is V22() V23() ext-real Element of REAL
(f . f1) #R ((1 / 2) - 1) is V22() V23() ext-real Element of REAL
(1 / 2) * ((f . f1) #R ((1 / 2) - 1)) is V22() V23() ext-real Element of REAL
diff (f,f1) is V22() V23() ext-real Element of REAL
((1 / 2) * ((f . f1) #R ((1 / 2) - 1))) * (diff (f,f1)) is V22() V23() ext-real Element of REAL
f `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| Z) . f1 is V22() V23() ext-real Element of REAL
((1 / 2) * ((f . f1) #R ((1 / 2) - 1))) * ((f `| Z) . f1) is V22() V23() ext-real Element of REAL
2 * (- 1) is V22() V23() ext-real V68() Element of REAL
(2 * (- 1)) * f1 is V22() V23() ext-real Element of REAL
0 + ((2 * (- 1)) * f1) is V22() V23() ext-real Element of REAL
((1 / 2) * ((f . f1) #R ((1 / 2) - 1))) * (0 + ((2 * (- 1)) * f1)) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
(((#R (1 / 2)) * f) `| Z) . f1 is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) arcsin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
(((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x - f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) f is V1() V6() set
x + (- f) is V1() V6() set
dom ((id Z) (#) arcsin) is V49() V50() V51() Element of K19(REAL)
dom ((#R (1 / 2)) * f) is V49() V50() V51() Element of K19(REAL)
(dom ((id Z) (#) arcsin)) /\ (dom ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
f1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
dom (x - f) is V49() V50() V51() Element of K19(REAL)
(x - f) . f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
(x . f1) - (f . f1) is V22() V23() ext-real Element of REAL
1 - (f . f1) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
(1 - (f1 ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . f1 is V22() V23() ext-real Element of REAL
arcsin . f1 is V22() V23() ext-real Element of REAL
diff (((id Z) (#) arcsin),f1) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * f),f1) is V22() V23() ext-real Element of REAL
(diff (((id Z) (#) arcsin),f1)) + (diff (((#R (1 / 2)) * f),f1)) is V22() V23() ext-real Element of REAL
((id Z) (#) arcsin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) (#) arcsin) `| Z) . f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arcsin) `| Z) . f1) + (diff (((#R (1 / 2)) * f),f1)) is V22() V23() ext-real Element of REAL
((#R (1 / 2)) * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#R (1 / 2)) * f) `| Z) . f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arcsin) `| Z) . f1) + ((((#R (1 / 2)) * f) `| Z) . f1) is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
f1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(arcsin . f1) + (f1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
((arcsin . f1) + (f1 / (sqrt (1 - (f1 ^2))))) + ((((#R (1 / 2)) * f) `| Z) . f1) is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arcsin . f1) + (f1 / (sqrt (1 - (f1 ^2))))) + (- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))))) is V22() V23() ext-real Element of REAL
((arcsin . f1) + (f1 / (sqrt (1 - (f1 ^2))))) - (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arcsin . f1) + (f1 / (sqrt (1 - (f1 ^2))))) - (f1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . f1 is V22() V23() ext-real Element of REAL
arcsin . f1 is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) arccos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) (#) arccos) - ((#R (1 / 2)) * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- ((#R (1 / 2)) * f) is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) ((#R (1 / 2)) * f) is V1() V6() set
((id Z) (#) arccos) + (- ((#R (1 / 2)) * f)) is V1() V6() set
dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
(((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x - f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f is V1() V6() V39() set
K58(1) (#) f is V1() V6() set
x + (- f) is V1() V6() set
dom ((id Z) (#) arccos) is V49() V50() V51() Element of K19(REAL)
dom ((#R (1 / 2)) * f) is V49() V50() V51() Element of K19(REAL)
(dom ((id Z) (#) arccos)) /\ (dom ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
f1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
dom (x - f) is V49() V50() V51() Element of K19(REAL)
(x - f) . f1 is V22() V23() ext-real Element of REAL
x . f1 is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
(x . f1) - (f . f1) is V22() V23() ext-real Element of REAL
1 - (f . f1) is V22() V23() ext-real Element of REAL
f . f1 is V22() V23() ext-real Element of REAL
(1 - (f1 ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . f1 is V22() V23() ext-real Element of REAL
arccos . f1 is V22() V23() ext-real Element of REAL
diff (((id Z) (#) arccos),f1) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * f),f1) is V22() V23() ext-real Element of REAL
(diff (((id Z) (#) arccos),f1)) - (diff (((#R (1 / 2)) * f),f1)) is V22() V23() ext-real Element of REAL
((id Z) (#) arccos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) (#) arccos) `| Z) . f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arccos) `| Z) . f1) - (diff (((#R (1 / 2)) * f),f1)) is V22() V23() ext-real Element of REAL
((#R (1 / 2)) * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#R (1 / 2)) * f) `| Z) . f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arccos) `| Z) . f1) - ((((#R (1 / 2)) * f) `| Z) . f1) is V22() V23() ext-real Element of REAL
f1 ^2 is V22() V23() ext-real Element of REAL
K57(f1,f1) is set
1 - (f1 ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - (f1 ^2)) is V22() V23() ext-real Element of REAL
f1 / (sqrt (1 - (f1 ^2))) is V22() V23() ext-real Element of REAL
(arccos . f1) - (f1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
((arccos . f1) - (f1 / (sqrt (1 - (f1 ^2))))) - ((((#R (1 / 2)) * f) `| Z) . f1) is V22() V23() ext-real Element of REAL
f1 #Z 2 is V22() V23() ext-real Element of REAL
1 - (f1 #Z 2) is V22() V23() ext-real Element of REAL
(1 - (f1 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arccos . f1) - (f1 / (sqrt (1 - (f1 ^2))))) - (- (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2))))) is V22() V23() ext-real Element of REAL
((arccos . f1) - (f1 / (sqrt (1 - (f1 ^2))))) + (f1 * ((1 - (f1 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arccos . f1) - (f1 / (sqrt (1 - (f1 ^2))))) + (f1 / (sqrt (1 - (f1 ^2)))) is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . f1 is V22() V23() ext-real Element of REAL
arccos . f1 is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arcsin * x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id f) (#) (arcsin * x) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id f) (#) (arcsin * x)) is V49() V50() V51() Element of K19(REAL)
((id f) (#) (arcsin * x)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (id f) is V49() V50() V51() Element of K19(REAL)
dom (arcsin * x) is V49() V50() V51() Element of K19(REAL)
(dom (id f)) /\ (dom (arcsin * x)) is V49() V50() V51() Element of K19(REAL)
1 / Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(id f) . f is V22() V23() ext-real Element of REAL
1 * f is V22() V23() ext-real Element of REAL
(1 * f) + 0 is V22() V23() ext-real Element of REAL
(arcsin * x) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((arcsin * x) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
(((1 / Z) * f) + 0) ^2 is V22() V23() ext-real Element of REAL
K57((((1 / Z) * f) + 0),(((1 / Z) * f) + 0)) is set
1 - ((((1 / Z) * f) + 0) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((((1 / Z) * f) + 0) ^2)) is V22() V23() ext-real Element of REAL
(1 / Z) / (sqrt (1 - ((((1 / Z) * f) + 0) ^2))) is V22() V23() ext-real Element of REAL
(1 / Z) / (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id f) (#) (arcsin * x)) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
arcsin . (f / Z) is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
f / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arcsin . (f / Z)) + (f / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
(arcsin * x) . f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
arcsin . (x . f) is V22() V23() ext-real Element of REAL
diff ((id f),f) is V22() V23() ext-real Element of REAL
((arcsin * x) . f) * (diff ((id f),f)) is V22() V23() ext-real Element of REAL
(id f) . f is V22() V23() ext-real Element of REAL
diff ((arcsin * x),f) is V22() V23() ext-real Element of REAL
((id f) . f) * (diff ((arcsin * x),f)) is V22() V23() ext-real Element of REAL
(((arcsin * x) . f) * (diff ((id f),f))) + (((id f) . f) * (diff ((arcsin * x),f))) is V22() V23() ext-real Element of REAL
(id f) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id f) `| f) . f is V22() V23() ext-real Element of REAL
((arcsin * x) . f) * (((id f) `| f) . f) is V22() V23() ext-real Element of REAL
(((arcsin * x) . f) * (((id f) `| f) . f)) + (((id f) . f) * (diff ((arcsin * x),f))) is V22() V23() ext-real Element of REAL
((arcsin * x) . f) * 1 is V22() V23() ext-real Element of REAL
(((arcsin * x) . f) * 1) + (((id f) . f) * (diff ((arcsin * x),f))) is V22() V23() ext-real Element of REAL
((arcsin * x) `| f) . f is V22() V23() ext-real Element of REAL
((id f) . f) * (((arcsin * x) `| f) . f) is V22() V23() ext-real Element of REAL
(((arcsin * x) . f) * 1) + (((id f) . f) * (((arcsin * x) `| f) . f)) is V22() V23() ext-real Element of REAL
f * (((arcsin * x) `| f) . f) is V22() V23() ext-real Element of REAL
((arcsin * x) . f) + (f * (((arcsin * x) `| f) . f)) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
f * (1 / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
(arcsin . (f / Z)) + (f * (1 / (Z * (sqrt (1 - ((f / Z) ^2)))))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id f) (#) (arcsin * x)) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
arcsin . (f / Z) is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
f / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arcsin . (f / Z)) + (f / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arccos * x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id f) (#) (arccos * x) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id f) (#) (arccos * x)) is V49() V50() V51() Element of K19(REAL)
((id f) (#) (arccos * x)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (id f) is V49() V50() V51() Element of K19(REAL)
dom (arccos * x) is V49() V50() V51() Element of K19(REAL)
(dom (id f)) /\ (dom (arccos * x)) is V49() V50() V51() Element of K19(REAL)
1 / Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(id f) . f is V22() V23() ext-real Element of REAL
1 * f is V22() V23() ext-real Element of REAL
(1 * f) + 0 is V22() V23() ext-real Element of REAL
(arccos * x) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((arccos * x) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
- (1 / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
(1 / Z) * f is V22() V23() ext-real Element of REAL
((1 / Z) * f) + 0 is V22() V23() ext-real Element of REAL
(((1 / Z) * f) + 0) ^2 is V22() V23() ext-real Element of REAL
K57((((1 / Z) * f) + 0),(((1 / Z) * f) + 0)) is set
1 - ((((1 / Z) * f) + 0) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((((1 / Z) * f) + 0) ^2)) is V22() V23() ext-real Element of REAL
(1 / Z) / (sqrt (1 - ((((1 / Z) * f) + 0) ^2))) is V22() V23() ext-real Element of REAL
- ((1 / Z) / (sqrt (1 - ((((1 / Z) * f) + 0) ^2)))) is V22() V23() ext-real Element of REAL
(1 / Z) / (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
- ((1 / Z) / (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id f) (#) (arccos * x)) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
arccos . (f / Z) is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
f / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arccos . (f / Z)) - (f / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
(arccos * x) . f is V22() V23() ext-real Element of REAL
x . f is V22() V23() ext-real Element of REAL
arccos . (x . f) is V22() V23() ext-real Element of REAL
diff ((id f),f) is V22() V23() ext-real Element of REAL
((arccos * x) . f) * (diff ((id f),f)) is V22() V23() ext-real Element of REAL
(id f) . f is V22() V23() ext-real Element of REAL
diff ((arccos * x),f) is V22() V23() ext-real Element of REAL
((id f) . f) * (diff ((arccos * x),f)) is V22() V23() ext-real Element of REAL
(((arccos * x) . f) * (diff ((id f),f))) + (((id f) . f) * (diff ((arccos * x),f))) is V22() V23() ext-real Element of REAL
(id f) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id f) `| f) . f is V22() V23() ext-real Element of REAL
((arccos * x) . f) * (((id f) `| f) . f) is V22() V23() ext-real Element of REAL
(((arccos * x) . f) * (((id f) `| f) . f)) + (((id f) . f) * (diff ((arccos * x),f))) is V22() V23() ext-real Element of REAL
((arccos * x) . f) * 1 is V22() V23() ext-real Element of REAL
(((arccos * x) . f) * 1) + (((id f) . f) * (diff ((arccos * x),f))) is V22() V23() ext-real Element of REAL
((arccos * x) `| f) . f is V22() V23() ext-real Element of REAL
((id f) . f) * (((arccos * x) `| f) . f) is V22() V23() ext-real Element of REAL
(((arccos * x) . f) * 1) + (((id f) . f) * (((arccos * x) `| f) . f)) is V22() V23() ext-real Element of REAL
f * (((arccos * x) `| f) . f) is V22() V23() ext-real Element of REAL
((arccos * x) . f) + (f * (((arccos * x) `| f) . f)) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
- (1 / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
f * (- (1 / (Z * (sqrt (1 - ((f / Z) ^2)))))) is V22() V23() ext-real Element of REAL
(arccos . (f / Z)) + (f * (- (1 / (Z * (sqrt (1 - ((f / Z) ^2))))))) is V22() V23() ext-real Element of REAL
f * (1 / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
(arccos . (f / Z)) - (f * (1 / (Z * (sqrt (1 - ((f / Z) ^2)))))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((id f) (#) (arccos * x)) `| f) . f is V22() V23() ext-real Element of REAL
f / Z is V22() V23() ext-real Element of REAL
arccos . (f / Z) is V22() V23() ext-real Element of REAL
(f / Z) ^2 is V22() V23() ext-real Element of REAL
K57((f / Z),(f / Z)) is set
1 - ((f / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((f / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((f / Z) ^2))) is V22() V23() ext-real Element of REAL
f / (Z * (sqrt (1 - ((f / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arccos . (f / Z)) - (f / (Z * (sqrt (1 - ((f / Z) ^2))))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z ^2 is V22() V23() ext-real Element of REAL
K57(Z,Z) is set
f is open V49() V50() V51() Element of K19(REAL)
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#R (1 / 2)) * x) is V49() V50() V51() Element of K19(REAL)
((#R (1 / 2)) * x) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f - f1 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f1 is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) f1 is V1() V6() set
f + (- f1) is V1() V6() set
dom x is V49() V50() V51() Element of K19(REAL)
f2 is set
(- 1) (#) f1 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f + ((- 1) (#) f1) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (f + ((- 1) (#) f1)) is V49() V50() V51() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
f . f2 is V22() V23() ext-real Element of REAL
0 * f2 is V22() V23() ext-real Element of REAL
(Z ^2) + (0 * f2) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
x . f2 is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
(((#R (1 / 2)) * x) `| f) . f2 is V22() V23() ext-real Element of REAL
f2 #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (f2 #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (f2 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f2 * (((Z ^2) - (f2 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f2 * (((Z ^2) - (f2 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
x . f2 is V22() V23() ext-real Element of REAL
dom (f - f1) is V49() V50() V51() Element of K19(REAL)
(f - f1) . f2 is V22() V23() ext-real Element of REAL
f . f2 is V22() V23() ext-real Element of REAL
f1 . f2 is V22() V23() ext-real Element of REAL
(f . f2) - (f1 . f2) is V22() V23() ext-real Element of REAL
(Z ^2) - (f1 . f2) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * x),f2) is V22() V23() ext-real Element of REAL
(1 / 2) - 1 is V22() V23() ext-real Element of REAL
(x . f2) #R ((1 / 2) - 1) is V22() V23() ext-real Element of REAL
(1 / 2) * ((x . f2) #R ((1 / 2) - 1)) is V22() V23() ext-real Element of REAL
diff (x,f2) is V22() V23() ext-real Element of REAL
((1 / 2) * ((x . f2) #R ((1 / 2) - 1))) * (diff (x,f2)) is V22() V23() ext-real Element of REAL
x `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . f2 is V22() V23() ext-real Element of REAL
((1 / 2) * ((x . f2) #R ((1 / 2) - 1))) * ((x `| f) . f2) is V22() V23() ext-real Element of REAL
2 * (- 1) is V22() V23() ext-real V68() Element of REAL
(2 * (- 1)) * f2 is V22() V23() ext-real Element of REAL
0 + ((2 * (- 1)) * f2) is V22() V23() ext-real Element of REAL
((1 / 2) * ((x . f2) #R ((1 / 2) - 1))) * (0 + ((2 * (- 1)) * f2)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
(((#R (1 / 2)) * x) `| f) . f2 is V22() V23() ext-real Element of REAL
f2 #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (f2 #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (f2 #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
f2 * (((Z ^2) - (f2 #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (f2 * (((Z ^2) - (f2 #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z ^2 is V22() V23() ext-real Element of REAL
K57(Z,Z) is set
f is open V49() V50() V51() Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arcsin * x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id f) (#) (arcsin * x) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id f) (#) (arcsin * x)) + ((#R (1 / 2)) * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (((id f) (#) (arcsin * x)) + ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
(((id f) (#) (arcsin * x)) + ((#R (1 / 2)) * f)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f1 - f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f2 is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) f2 is V1() V6() set
f1 + (- f2) is V1() V6() set
dom ((id f) (#) (arcsin * x)) is V49() V50() V51() Element of K19(REAL)
dom ((#R (1 / 2)) * f) is V49() V50() V51() Element of K19(REAL)
(dom ((id f) (#) (arcsin * x))) /\ (dom ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
f1 . x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (x #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (x #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
(x / Z) ^2 is V22() V23() ext-real Element of REAL
K57((x / Z),(x / Z)) is set
1 - ((x / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
1 - (x . x) is V22() V23() ext-real Element of REAL
1 - 1 is V22() V23() ext-real V68() Element of REAL
1 + (x . x) is V22() V23() ext-real Element of REAL
1 + (- 1) is V22() V23() ext-real V68() Element of REAL
(1 + (x . x)) * (1 - (x . x)) is V22() V23() ext-real Element of REAL
sqrt (Z ^2) is V22() V23() ext-real Element of REAL
(sqrt (Z ^2)) * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / ((sqrt (Z ^2)) * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(Z ^2) * (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
sqrt ((Z ^2) * (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (sqrt ((Z ^2) * (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(Z ^2) * 1 is V22() V23() ext-real Element of REAL
Z * (x / Z) is V22() V23() ext-real Element of REAL
(Z * (x / Z)) ^2 is V22() V23() ext-real Element of REAL
K57((Z * (x / Z)),(Z * (x / Z))) is set
((Z ^2) * 1) - ((Z * (x / Z)) ^2) is V22() V23() ext-real Element of REAL
(((Z ^2) * 1) - ((Z * (x / Z)) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * Z is V22() V23() ext-real Element of REAL
(x * Z) / Z is V22() V23() ext-real Element of REAL
((x * Z) / Z) ^2 is V22() V23() ext-real Element of REAL
K57(((x * Z) / Z),((x * Z) / Z)) is set
(Z ^2) - (((x * Z) / Z) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - (((x * Z) / Z) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
Z / Z is V22() V23() ext-real Element of REAL
x * (Z / Z) is V22() V23() ext-real Element of REAL
(x * (Z / Z)) ^2 is V22() V23() ext-real Element of REAL
K57((x * (Z / Z)),(x * (Z / Z))) is set
(Z ^2) - ((x * (Z / Z)) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - ((x * (Z / Z)) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * 1 is V22() V23() ext-real Element of REAL
(x * 1) ^2 is V22() V23() ext-real Element of REAL
K57((x * 1),(x * 1)) is set
(Z ^2) - ((x * 1) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - ((x * 1) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((((id f) (#) (arcsin * x)) + ((#R (1 / 2)) * f)) `| f) . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
arcsin . (x / Z) is V22() V23() ext-real Element of REAL
diff (((id f) (#) (arcsin * x)),x) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * f),x) is V22() V23() ext-real Element of REAL
(diff (((id f) (#) (arcsin * x)),x)) + (diff (((#R (1 / 2)) * f),x)) is V22() V23() ext-real Element of REAL
((id f) (#) (arcsin * x)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id f) (#) (arcsin * x)) `| f) . x is V22() V23() ext-real Element of REAL
((((id f) (#) (arcsin * x)) `| f) . x) + (diff (((#R (1 / 2)) * f),x)) is V22() V23() ext-real Element of REAL
((#R (1 / 2)) * f) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#R (1 / 2)) * f) `| f) . x is V22() V23() ext-real Element of REAL
((((id f) (#) (arcsin * x)) `| f) . x) + ((((#R (1 / 2)) * f) `| f) . x) is V22() V23() ext-real Element of REAL
(x / Z) ^2 is V22() V23() ext-real Element of REAL
K57((x / Z),(x / Z)) is set
1 - ((x / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
x / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
((arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) + ((((#R (1 / 2)) * f) `| f) . x) is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (x #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (x #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) + (- (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2))))) is V22() V23() ext-real Element of REAL
((arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) - (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
x * (1 / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
((arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) - (x * (1 / (Z * (sqrt (1 - ((x / Z) ^2)))))) is V22() V23() ext-real Element of REAL
((arcsin . (x / Z)) + (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) - (x / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((((id f) (#) (arcsin * x)) + ((#R (1 / 2)) * f)) `| f) . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
arcsin . (x / Z) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
Z ^2 is V22() V23() ext-real Element of REAL
K57(Z,Z) is set
f is open V49() V50() V51() Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
arccos * x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id f) (#) (arccos * x) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id f) (#) (arccos * x)) - ((#R (1 / 2)) * f) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- ((#R (1 / 2)) * f) is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) ((#R (1 / 2)) * f) is V1() V6() set
((id f) (#) (arccos * x)) + (- ((#R (1 / 2)) * f)) is V1() V6() set
dom (((id f) (#) (arccos * x)) - ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
(((id f) (#) (arccos * x)) - ((#R (1 / 2)) * f)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f1 - f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- f2 is V1() V6() V39() set
K58(1) (#) f2 is V1() V6() set
f1 + (- f2) is V1() V6() set
dom ((id f) (#) (arccos * x)) is V49() V50() V51() Element of K19(REAL)
dom ((#R (1 / 2)) * f) is V49() V50() V51() Element of K19(REAL)
(dom ((id f) (#) (arccos * x))) /\ (dom ((#R (1 / 2)) * f)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
f1 . x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (x #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (x #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
(x / Z) ^2 is V22() V23() ext-real Element of REAL
K57((x / Z),(x / Z)) is set
1 - ((x / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
1 - (x . x) is V22() V23() ext-real Element of REAL
1 - 1 is V22() V23() ext-real V68() Element of REAL
1 + (x . x) is V22() V23() ext-real Element of REAL
1 + (- 1) is V22() V23() ext-real V68() Element of REAL
(1 + (x . x)) * (1 - (x . x)) is V22() V23() ext-real Element of REAL
sqrt (Z ^2) is V22() V23() ext-real Element of REAL
(sqrt (Z ^2)) * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / ((sqrt (Z ^2)) * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(Z ^2) * (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
sqrt ((Z ^2) * (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
1 / (sqrt ((Z ^2) * (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(Z ^2) * 1 is V22() V23() ext-real Element of REAL
Z * (x / Z) is V22() V23() ext-real Element of REAL
(Z * (x / Z)) ^2 is V22() V23() ext-real Element of REAL
K57((Z * (x / Z)),(Z * (x / Z))) is set
((Z ^2) * 1) - ((Z * (x / Z)) ^2) is V22() V23() ext-real Element of REAL
(((Z ^2) * 1) - ((Z * (x / Z)) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * Z is V22() V23() ext-real Element of REAL
(x * Z) / Z is V22() V23() ext-real Element of REAL
((x * Z) / Z) ^2 is V22() V23() ext-real Element of REAL
K57(((x * Z) / Z),((x * Z) / Z)) is set
(Z ^2) - (((x * Z) / Z) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - (((x * Z) / Z) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
Z / Z is V22() V23() ext-real Element of REAL
x * (Z / Z) is V22() V23() ext-real Element of REAL
(x * (Z / Z)) ^2 is V22() V23() ext-real Element of REAL
K57((x * (Z / Z)),(x * (Z / Z))) is set
(Z ^2) - ((x * (Z / Z)) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - ((x * (Z / Z)) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * 1 is V22() V23() ext-real Element of REAL
(x * 1) ^2 is V22() V23() ext-real Element of REAL
K57((x * 1),(x * 1)) is set
(Z ^2) - ((x * 1) ^2) is V22() V23() ext-real Element of REAL
((Z ^2) - ((x * 1) ^2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((((id f) (#) (arccos * x)) - ((#R (1 / 2)) * f)) `| f) . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
arccos . (x / Z) is V22() V23() ext-real Element of REAL
diff (((id f) (#) (arccos * x)),x) is V22() V23() ext-real Element of REAL
diff (((#R (1 / 2)) * f),x) is V22() V23() ext-real Element of REAL
(diff (((id f) (#) (arccos * x)),x)) - (diff (((#R (1 / 2)) * f),x)) is V22() V23() ext-real Element of REAL
((id f) (#) (arccos * x)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id f) (#) (arccos * x)) `| f) . x is V22() V23() ext-real Element of REAL
((((id f) (#) (arccos * x)) `| f) . x) - (diff (((#R (1 / 2)) * f),x)) is V22() V23() ext-real Element of REAL
((#R (1 / 2)) * f) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((#R (1 / 2)) * f) `| f) . x is V22() V23() ext-real Element of REAL
((((id f) (#) (arccos * x)) `| f) . x) - ((((#R (1 / 2)) * f) `| f) . x) is V22() V23() ext-real Element of REAL
(x / Z) ^2 is V22() V23() ext-real Element of REAL
K57((x / Z),(x / Z)) is set
1 - ((x / Z) ^2) is V22() V23() ext-real Element of REAL
sqrt (1 - ((x / Z) ^2)) is V22() V23() ext-real Element of REAL
Z * (sqrt (1 - ((x / Z) ^2))) is V22() V23() ext-real Element of REAL
x / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
(arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
((arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) - ((((#R (1 / 2)) * f) `| f) . x) is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
(Z ^2) - (x #Z 2) is V22() V23() ext-real Element of REAL
((Z ^2) - (x #Z 2)) #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
- (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
((arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) - (- (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2))))) is V22() V23() ext-real Element of REAL
((arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) + (x * (((Z ^2) - (x #Z 2)) #R (- (1 / 2)))) is V22() V23() ext-real Element of REAL
1 / (Z * (sqrt (1 - ((x / Z) ^2)))) is V22() V23() ext-real Element of REAL
x * (1 / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
((arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) + (x * (1 / (Z * (sqrt (1 - ((x / Z) ^2)))))) is V22() V23() ext-real Element of REAL
((arccos . (x / Z)) - (x / (Z * (sqrt (1 - ((x / Z) ^2)))))) + (x / (Z * (sqrt (1 - ((x / Z) ^2))))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((((id f) (#) (arccos * x)) - ((#R (1 / 2)) * f)) `| f) . x is V22() V23() ext-real Element of REAL
x / Z is V22() V23() ext-real Element of REAL
arccos . (x / Z) is V22() V23() ext-real Element of REAL
Z is V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
#Z Z is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
(#Z Z) * (sin ^) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
1 / Z is V22() V23() ext-real Element of REAL
- (1 / Z) is V22() V23() ext-real Element of REAL
(- (1 / Z)) (#) ((#Z Z) * (sin ^)) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((- (1 / Z)) (#) ((#Z Z) * (sin ^))) is V49() V50() V51() Element of K19(REAL)
Z + 1 is V22() V23() ext-real V68() Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
((- (1 / Z)) (#) ((#Z Z) * (sin ^))) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z Z) * (sin ^)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
dom (sin ^) is V49() V50() V51() Element of K19(REAL)
x is set
x is V22() V23() ext-real Element of REAL
(((- (1 / Z)) (#) ((#Z Z) * (sin ^))) `| f) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
sin . x is V22() V23() ext-real Element of REAL
(sin . x) #Z (Z + 1) is V22() V23() ext-real Element of REAL
(cos . x) / ((sin . x) #Z (Z + 1)) is V22() V23() ext-real Element of REAL
(sin ^) . x is V22() V23() ext-real Element of REAL
(sin . x) " is V22() V23() ext-real Element of REAL
1 / (sin . x) is V22() V23() ext-real Element of REAL
diff (((#Z Z) * (sin ^)),x) is V22() V23() ext-real Element of REAL
(- (1 / Z)) * (diff (((#Z Z) * (sin ^)),x)) is V22() V23() ext-real Element of REAL
Z - 1 is V22() V23() ext-real V68() Element of REAL
((sin ^) . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * (((sin ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
diff ((sin ^),x) is V22() V23() ext-real Element of REAL
(Z * (((sin ^) . x) #Z (Z - 1))) * (diff ((sin ^),x)) is V22() V23() ext-real Element of REAL
(- (1 / Z)) * ((Z * (((sin ^) . x) #Z (Z - 1))) * (diff ((sin ^),x))) is V22() V23() ext-real Element of REAL
(sin ^) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin ^) `| f) . x is V22() V23() ext-real Element of REAL
(Z * (((sin ^) . x) #Z (Z - 1))) * (((sin ^) `| f) . x) is V22() V23() ext-real Element of REAL
(- (1 / Z)) * ((Z * (((sin ^) . x) #Z (Z - 1))) * (((sin ^) `| f) . x)) is V22() V23() ext-real Element of REAL
(sin . x) ^2 is V22() V23() ext-real Element of REAL
K57((sin . x),(sin . x)) is set
(cos . x) / ((sin . x) ^2) is V22() V23() ext-real Element of REAL
- ((cos . x) / ((sin . x) ^2)) is V22() V23() ext-real Element of REAL
(Z * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2))) is V22() V23() ext-real Element of REAL
(- (1 / Z)) * ((Z * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2)))) is V22() V23() ext-real Element of REAL
(1 / Z) * Z is V22() V23() ext-real Element of REAL
((1 / Z) * Z) * (((sin ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(((1 / Z) * Z) * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2))) is V22() V23() ext-real Element of REAL
- ((((1 / Z) * Z) * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2)))) is V22() V23() ext-real Element of REAL
1 * (((sin ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(1 * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2))) is V22() V23() ext-real Element of REAL
- ((1 * (((sin ^) . x) #Z (Z - 1))) * (- ((cos . x) / ((sin . x) ^2)))) is V22() V23() ext-real Element of REAL
(1 / (sin . x)) #Z (Z - 1) is V22() V23() ext-real Element of REAL
(sin . x) #Z 2 is V22() V23() ext-real Element of REAL
(cos . x) / ((sin . x) #Z 2) is V22() V23() ext-real Element of REAL
- ((cos . x) / ((sin . x) #Z 2)) is V22() V23() ext-real Element of REAL
((1 / (sin . x)) #Z (Z - 1)) * (- ((cos . x) / ((sin . x) #Z 2))) is V22() V23() ext-real Element of REAL
- (((1 / (sin . x)) #Z (Z - 1)) * (- ((cos . x) / ((sin . x) #Z 2)))) is V22() V23() ext-real Element of REAL
(sin . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
1 / ((sin . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(- ((cos . x) / ((sin . x) #Z 2))) * (1 / ((sin . x) #Z (Z - 1))) is V22() V23() ext-real Element of REAL
- ((- ((cos . x) / ((sin . x) #Z 2))) * (1 / ((sin . x) #Z (Z - 1)))) is V22() V23() ext-real Element of REAL
((cos . x) / ((sin . x) #Z 2)) * (1 / ((sin . x) #Z (Z - 1))) is V22() V23() ext-real Element of REAL
((cos . x) / ((sin . x) #Z 2)) / ((sin . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
((sin . x) #Z 2) * ((sin . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(cos . x) / (((sin . x) #Z 2) * ((sin . x) #Z (Z - 1))) is V22() V23() ext-real Element of REAL
2 + (Z - 1) is V22() V23() ext-real V68() Element of REAL
(sin . x) #Z (2 + (Z - 1)) is V22() V23() ext-real Element of REAL
(cos . x) / ((sin . x) #Z (2 + (Z - 1))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((- (1 / Z)) (#) ((#Z Z) * (sin ^))) `| f) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
sin . x is V22() V23() ext-real Element of REAL
(sin . x) #Z (Z + 1) is V22() V23() ext-real Element of REAL
(cos . x) / ((sin . x) #Z (Z + 1)) is V22() V23() ext-real Element of REAL
Z is V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
#Z Z is V1() V4( REAL ) V5( REAL ) V6() V33( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
(#Z Z) * (cos ^) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
1 / Z is V22() V23() ext-real Element of REAL
(1 / Z) (#) ((#Z Z) * (cos ^)) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((1 / Z) (#) ((#Z Z) * (cos ^))) is V49() V50() V51() Element of K19(REAL)
Z + 1 is V22() V23() ext-real V68() Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
((1 / Z) (#) ((#Z Z) * (cos ^))) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z Z) * (cos ^)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
dom (cos ^) is V49() V50() V51() Element of K19(REAL)
x is set
x is V22() V23() ext-real Element of REAL
(((1 / Z) (#) ((#Z Z) * (cos ^))) `| f) . x is V22() V23() ext-real Element of REAL
sin . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
(cos . x) #Z (Z + 1) is V22() V23() ext-real Element of REAL
(sin . x) / ((cos . x) #Z (Z + 1)) is V22() V23() ext-real Element of REAL
(cos ^) . x is V22() V23() ext-real Element of REAL
(cos . x) " is V22() V23() ext-real Element of REAL
1 / (cos . x) is V22() V23() ext-real Element of REAL
diff (((#Z Z) * (cos ^)),x) is V22() V23() ext-real Element of REAL
(1 / Z) * (diff (((#Z Z) * (cos ^)),x)) is V22() V23() ext-real Element of REAL
Z - 1 is V22() V23() ext-real V68() Element of REAL
((cos ^) . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
Z * (((cos ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
diff ((cos ^),x) is V22() V23() ext-real Element of REAL
(Z * (((cos ^) . x) #Z (Z - 1))) * (diff ((cos ^),x)) is V22() V23() ext-real Element of REAL
(1 / Z) * ((Z * (((cos ^) . x) #Z (Z - 1))) * (diff ((cos ^),x))) is V22() V23() ext-real Element of REAL
(cos ^) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((cos ^) `| f) . x is V22() V23() ext-real Element of REAL
(Z * (((cos ^) . x) #Z (Z - 1))) * (((cos ^) `| f) . x) is V22() V23() ext-real Element of REAL
(1 / Z) * ((Z * (((cos ^) . x) #Z (Z - 1))) * (((cos ^) `| f) . x)) is V22() V23() ext-real Element of REAL
(cos . x) ^2 is V22() V23() ext-real Element of REAL
K57((cos . x),(cos . x)) is set
(sin . x) / ((cos . x) ^2) is V22() V23() ext-real Element of REAL
(Z * (((cos ^) . x) #Z (Z - 1))) * ((sin . x) / ((cos . x) ^2)) is V22() V23() ext-real Element of REAL
(1 / Z) * ((Z * (((cos ^) . x) #Z (Z - 1))) * ((sin . x) / ((cos . x) ^2))) is V22() V23() ext-real Element of REAL
(1 / Z) * Z is V22() V23() ext-real Element of REAL
((1 / Z) * Z) * (((cos ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(((1 / Z) * Z) * (((cos ^) . x) #Z (Z - 1))) * ((sin . x) / ((cos . x) ^2)) is V22() V23() ext-real Element of REAL
1 * (((cos ^) . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(1 * (((cos ^) . x) #Z (Z - 1))) * ((sin . x) / ((cos . x) ^2)) is V22() V23() ext-real Element of REAL
(1 / (cos . x)) #Z (Z - 1) is V22() V23() ext-real Element of REAL
(cos . x) #Z 2 is V22() V23() ext-real Element of REAL
(sin . x) / ((cos . x) #Z 2) is V22() V23() ext-real Element of REAL
((1 / (cos . x)) #Z (Z - 1)) * ((sin . x) / ((cos . x) #Z 2)) is V22() V23() ext-real Element of REAL
(cos . x) #Z (Z - 1) is V22() V23() ext-real Element of REAL
1 / ((cos . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(1 / ((cos . x) #Z (Z - 1))) * ((sin . x) / ((cos . x) #Z 2)) is V22() V23() ext-real Element of REAL
((sin . x) / ((cos . x) #Z 2)) / ((cos . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
((cos . x) #Z 2) * ((cos . x) #Z (Z - 1)) is V22() V23() ext-real Element of REAL
(sin . x) / (((cos . x) #Z 2) * ((cos . x) #Z (Z - 1))) is V22() V23() ext-real Element of REAL
2 + (Z - 1) is V22() V23() ext-real V68() Element of REAL
(cos . x) #Z (2 + (Z - 1)) is V22() V23() ext-real Element of REAL
(sin . x) / ((cos . x) #Z (2 + (Z - 1))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((1 / Z) (#) ((#Z Z) * (cos ^))) `| f) . x is V22() V23() ext-real Element of REAL
sin . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
(cos . x) #Z (Z + 1) is V22() V23() ext-real Element of REAL
(sin . x) / ((cos . x) #Z (Z + 1)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= 0 } is set
sin * ln is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin * ln) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(sin * ln) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin * ln) `| Z) . f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
cos . (ln . f) is V22() V23() ext-real Element of REAL
(cos . (ln . f)) / f is V22() V23() ext-real Element of REAL
diff ((sin * ln),f) is V22() V23() ext-real Element of REAL
diff (sin,(ln . f)) is V22() V23() ext-real Element of REAL
diff (ln,f) is V22() V23() ext-real Element of REAL
(diff (sin,(ln . f))) * (diff (ln,f)) is V22() V23() ext-real Element of REAL
(cos . (ln . f)) * (diff (ln,f)) is V22() V23() ext-real Element of REAL
1 / f is V22() V23() ext-real Element of REAL
(cos . (ln . f)) * (1 / f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin * ln) `| Z) . f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
cos . (ln . f) is V22() V23() ext-real Element of REAL
(cos . (ln . f)) / f is V22() V23() ext-real Element of REAL
cos * ln is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cos * ln) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(cos * ln) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((cos * ln) `| Z) . f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
sin . (ln . f) is V22() V23() ext-real Element of REAL
(sin . (ln . f)) / f is V22() V23() ext-real Element of REAL
- ((sin . (ln . f)) / f) is V22() V23() ext-real Element of REAL
diff ((cos * ln),f) is V22() V23() ext-real Element of REAL
diff (cos,(ln . f)) is V22() V23() ext-real Element of REAL
diff (ln,f) is V22() V23() ext-real Element of REAL
(diff (cos,(ln . f))) * (diff (ln,f)) is V22() V23() ext-real Element of REAL
- (sin . (ln . f)) is V22() V23() ext-real Element of REAL
(- (sin . (ln . f))) * (diff (ln,f)) is V22() V23() ext-real Element of REAL
1 / f is V22() V23() ext-real Element of REAL
(- (sin . (ln . f))) * (1 / f) is V22() V23() ext-real Element of REAL
(- (sin . (ln . f))) / f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((cos * ln) `| Z) . f is V22() V23() ext-real Element of REAL
ln . f is V22() V23() ext-real Element of REAL
sin . (ln . f) is V22() V23() ext-real Element of REAL
(sin . (ln . f)) / f is V22() V23() ext-real Element of REAL
- ((sin . (ln . f)) / f) is V22() V23() ext-real Element of REAL
sin * exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin * exp_R) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(sin * exp_R) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin * exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
cos . (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (cos . (exp_R . f)) is V22() V23() ext-real Element of REAL
diff ((sin * exp_R),f) is V22() V23() ext-real Element of REAL
diff (sin,(exp_R . f)) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (sin,(exp_R . f))) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
(cos . (exp_R . f)) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin * exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
cos . (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (cos . (exp_R . f)) is V22() V23() ext-real Element of REAL
cos * exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cos * exp_R) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(cos * exp_R) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((cos * exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
sin . (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (sin . (exp_R . f)) is V22() V23() ext-real Element of REAL
- ((exp_R . f) * (sin . (exp_R . f))) is V22() V23() ext-real Element of REAL
diff ((cos * exp_R),f) is V22() V23() ext-real Element of REAL
diff (cos,(exp_R . f)) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (cos,(exp_R . f))) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
- (sin . (exp_R . f)) is V22() V23() ext-real Element of REAL
(- (sin . (exp_R . f))) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
(- (sin . (exp_R . f))) * (exp_R . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((cos * exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
sin . (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (sin . (exp_R . f)) is V22() V23() ext-real Element of REAL
- ((exp_R . f) * (sin . (exp_R . f))) is V22() V23() ext-real Element of REAL
exp_R * cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R * cos) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R * cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R * cos) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
exp_R . (cos . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(exp_R . (cos . f)) * (sin . f) is V22() V23() ext-real Element of REAL
- ((exp_R . (cos . f)) * (sin . f)) is V22() V23() ext-real Element of REAL
diff ((exp_R * cos),f) is V22() V23() ext-real Element of REAL
diff (exp_R,(cos . f)) is V22() V23() ext-real Element of REAL
diff (cos,f) is V22() V23() ext-real Element of REAL
(diff (exp_R,(cos . f))) * (diff (cos,f)) is V22() V23() ext-real Element of REAL
- (sin . f) is V22() V23() ext-real Element of REAL
(diff (exp_R,(cos . f))) * (- (sin . f)) is V22() V23() ext-real Element of REAL
(exp_R . (cos . f)) * (- (sin . f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R * cos) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
exp_R . (cos . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(exp_R . (cos . f)) * (sin . f) is V22() V23() ext-real Element of REAL
- ((exp_R . (cos . f)) * (sin . f)) is V22() V23() ext-real Element of REAL
exp_R * sin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R * sin) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R * sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R * sin) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
exp_R . (sin . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(exp_R . (sin . f)) * (cos . f) is V22() V23() ext-real Element of REAL
diff ((exp_R * sin),f) is V22() V23() ext-real Element of REAL
diff (exp_R,(sin . f)) is V22() V23() ext-real Element of REAL
diff (sin,f) is V22() V23() ext-real Element of REAL
(diff (exp_R,(sin . f))) * (diff (sin,f)) is V22() V23() ext-real Element of REAL
(diff (exp_R,(sin . f))) * (cos . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R * sin) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
exp_R . (sin . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(exp_R . (sin . f)) * (cos . f) is V22() V23() ext-real Element of REAL
sin + cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin + cos) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(sin + cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((sin + cos) `| Z) . f is V22() V23() ext-real Element of REAL
diff (sin,f) is V22() V23() ext-real Element of REAL
diff (cos,f) is V22() V23() ext-real Element of REAL
(diff (sin,f)) + (diff (cos,f)) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(cos . f) + (diff (cos,f)) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
- (sin . f) is V22() V23() ext-real Element of REAL
(cos . f) + (- (sin . f)) is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin + cos) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
sin - cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- cos is V1() V6() V39() set
K58(1) is V22() V23() V68() set
K58(1) (#) cos is V1() V6() set
sin + (- cos) is V1() V6() set
dom (sin - cos) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(sin - cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((sin - cos) `| Z) . f is V22() V23() ext-real Element of REAL
diff (sin,f) is V22() V23() ext-real Element of REAL
diff (cos,f) is V22() V23() ext-real Element of REAL
(diff (sin,f)) - (diff (cos,f)) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(cos . f) - (diff (cos,f)) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
- (sin . f) is V22() V23() ext-real Element of REAL
(cos . f) - (- (sin . f)) is V22() V23() ext-real Element of REAL
(cos . f) + (sin . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((sin - cos) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(cos . f) + (sin . f) is V22() V23() ext-real Element of REAL
exp_R (#) (sin - cos) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R (#) (sin - cos)) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R (#) (sin - cos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(dom (sin - cos)) /\ (dom exp_R) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
((exp_R (#) (sin - cos)) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
2 * (exp_R . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(2 * (exp_R . f)) * (sin . f) is V22() V23() ext-real Element of REAL
(sin - cos) . f is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
((sin - cos) . f) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
diff ((sin - cos),f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (diff ((sin - cos),f)) is V22() V23() ext-real Element of REAL
(((sin - cos) . f) * (diff (exp_R,f))) + ((exp_R . f) * (diff ((sin - cos),f))) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(sin . f) - (cos . f) is V22() V23() ext-real Element of REAL
((sin . f) - (cos . f)) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
(((sin . f) - (cos . f)) * (diff (exp_R,f))) + ((exp_R . f) * (diff ((sin - cos),f))) is V22() V23() ext-real Element of REAL
((sin . f) - (cos . f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
(((sin . f) - (cos . f)) * (exp_R . f)) + ((exp_R . f) * (diff ((sin - cos),f))) is V22() V23() ext-real Element of REAL
(sin - cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin - cos) `| Z) . f is V22() V23() ext-real Element of REAL
(exp_R . f) * (((sin - cos) `| Z) . f) is V22() V23() ext-real Element of REAL
(((sin . f) - (cos . f)) * (exp_R . f)) + ((exp_R . f) * (((sin - cos) `| Z) . f)) is V22() V23() ext-real Element of REAL
(cos . f) + (sin . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((cos . f) + (sin . f)) is V22() V23() ext-real Element of REAL
(((sin . f) - (cos . f)) * (exp_R . f)) + ((exp_R . f) * ((cos . f) + (sin . f))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R (#) (sin - cos)) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
2 * (exp_R . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(2 * (exp_R . f)) * (sin . f) is V22() V23() ext-real Element of REAL
exp_R (#) (sin + cos) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R (#) (sin + cos)) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R (#) (sin + cos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(dom (sin + cos)) /\ (dom exp_R) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
((exp_R (#) (sin + cos)) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
2 * (exp_R . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(2 * (exp_R . f)) * (cos . f) is V22() V23() ext-real Element of REAL
(sin + cos) . f is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
((sin + cos) . f) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
diff ((sin + cos),f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (diff ((sin + cos),f)) is V22() V23() ext-real Element of REAL
(((sin + cos) . f) * (diff (exp_R,f))) + ((exp_R . f) * (diff ((sin + cos),f))) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(sin . f) + (cos . f) is V22() V23() ext-real Element of REAL
((sin . f) + (cos . f)) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
(((sin . f) + (cos . f)) * (diff (exp_R,f))) + ((exp_R . f) * (diff ((sin + cos),f))) is V22() V23() ext-real Element of REAL
((sin . f) + (cos . f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
(((sin . f) + (cos . f)) * (exp_R . f)) + ((exp_R . f) * (diff ((sin + cos),f))) is V22() V23() ext-real Element of REAL
(sin + cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin + cos) `| Z) . f is V22() V23() ext-real Element of REAL
(exp_R . f) * (((sin + cos) `| Z) . f) is V22() V23() ext-real Element of REAL
(((sin . f) + (cos . f)) * (exp_R . f)) + ((exp_R . f) * (((sin + cos) `| Z) . f)) is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((cos . f) - (sin . f)) is V22() V23() ext-real Element of REAL
(((sin . f) + (cos . f)) * (exp_R . f)) + ((exp_R . f) * ((cos . f) - (sin . f))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R (#) (sin + cos)) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
2 * (exp_R . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(2 * (exp_R . f)) * (cos . f) is V22() V23() ext-real Element of REAL
(sin + cos) / exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((sin + cos) / exp_R) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
((sin + cos) / exp_R) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
exp_R " {0} is V49() V50() V51() Element of K19(REAL)
(dom exp_R) \ (exp_R " {0}) is V49() V50() V51() Element of K19(REAL)
(dom (sin + cos)) /\ ((dom exp_R) \ (exp_R " {0})) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((sin + cos) / exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
2 * (sin . f) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
- ((2 * (sin . f)) / (exp_R . f)) is V22() V23() ext-real Element of REAL
(sin + cos) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(sin . f) + (cos . f) is V22() V23() ext-real Element of REAL
diff (((sin + cos) / exp_R),f) is V22() V23() ext-real Element of REAL
diff ((sin + cos),f) is V22() V23() ext-real Element of REAL
(diff ((sin + cos),f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (exp_R,f)) * ((sin + cos) . f) is V22() V23() ext-real Element of REAL
((diff ((sin + cos),f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f)) is V22() V23() ext-real Element of REAL
(exp_R . f) ^2 is V22() V23() ext-real Element of REAL
K57((exp_R . f),(exp_R . f)) is set
(((diff ((sin + cos),f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(sin + cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin + cos) `| Z) . f is V22() V23() ext-real Element of REAL
(((sin + cos) `| Z) . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((((sin + cos) `| Z) . f) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f)) is V22() V23() ext-real Element of REAL
(((((sin + cos) `| Z) . f) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
((cos . f) - (sin . f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
(((cos . f) - (sin . f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f)) is V22() V23() ext-real Element of REAL
((((cos . f) - (sin . f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin + cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((sin . f) + (cos . f)) is V22() V23() ext-real Element of REAL
(((cos . f) - (sin . f)) * (exp_R . f)) - ((exp_R . f) * ((sin . f) + (cos . f))) is V22() V23() ext-real Element of REAL
((((cos . f) - (sin . f)) * (exp_R . f)) - ((exp_R . f) * ((sin . f) + (cos . f)))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
- (2 * (sin . f)) is V22() V23() ext-real Element of REAL
(- (2 * (sin . f))) * (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((- (2 * (sin . f))) * (exp_R . f)) / ((exp_R . f) * (exp_R . f)) is V22() V23() ext-real Element of REAL
(exp_R . f) / ((exp_R . f) * (exp_R . f)) is V22() V23() ext-real Element of REAL
(- (2 * (sin . f))) * ((exp_R . f) / ((exp_R . f) * (exp_R . f))) is V22() V23() ext-real Element of REAL
(exp_R . f) / (exp_R . f) is V22() V23() ext-real Element of REAL
((exp_R . f) / (exp_R . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
(- (2 * (sin . f))) * (((exp_R . f) / (exp_R . f)) / (exp_R . f)) is V22() V23() ext-real Element of REAL
1 / (exp_R . f) is V22() V23() ext-real Element of REAL
(- (2 * (sin . f))) * (1 / (exp_R . f)) is V22() V23() ext-real Element of REAL
(- (2 * (sin . f))) / (exp_R . f) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((sin + cos) / exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
2 * (sin . f) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
- ((2 * (sin . f)) / (exp_R . f)) is V22() V23() ext-real Element of REAL
(sin - cos) / exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((sin - cos) / exp_R) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
((sin - cos) / exp_R) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
exp_R " {0} is V49() V50() V51() Element of K19(REAL)
(dom exp_R) \ (exp_R " {0}) is V49() V50() V51() Element of K19(REAL)
(dom (sin - cos)) /\ ((dom exp_R) \ (exp_R " {0})) is V49() V50() V51() Element of K19(REAL)
f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((sin - cos) / exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
2 * (cos . f) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
(sin - cos) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(sin . f) - (cos . f) is V22() V23() ext-real Element of REAL
diff (((sin - cos) / exp_R),f) is V22() V23() ext-real Element of REAL
diff ((sin - cos),f) is V22() V23() ext-real Element of REAL
(diff ((sin - cos),f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (exp_R,f)) * ((sin - cos) . f) is V22() V23() ext-real Element of REAL
((diff ((sin - cos),f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f)) is V22() V23() ext-real Element of REAL
(exp_R . f) ^2 is V22() V23() ext-real Element of REAL
K57((exp_R . f),(exp_R . f)) is set
(((diff ((sin - cos),f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(sin - cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin - cos) `| Z) . f is V22() V23() ext-real Element of REAL
(((sin - cos) `| Z) . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((((sin - cos) `| Z) . f) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f)) is V22() V23() ext-real Element of REAL
(((((sin - cos) `| Z) . f) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(cos . f) + (sin . f) is V22() V23() ext-real Element of REAL
((cos . f) + (sin . f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
(((cos . f) + (sin . f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f)) is V22() V23() ext-real Element of REAL
((((cos . f) + (sin . f)) * (exp_R . f)) - ((diff (exp_R,f)) * ((sin - cos) . f))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((sin . f) - (cos . f)) is V22() V23() ext-real Element of REAL
(((cos . f) + (sin . f)) * (exp_R . f)) - ((exp_R . f) * ((sin . f) - (cos . f))) is V22() V23() ext-real Element of REAL
((((cos . f) + (sin . f)) * (exp_R . f)) - ((exp_R . f) * ((sin . f) - (cos . f)))) / ((exp_R . f) ^2) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) * (exp_R . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((2 * (cos . f)) * (exp_R . f)) / ((exp_R . f) * (exp_R . f)) is V22() V23() ext-real Element of REAL
(exp_R . f) / ((exp_R . f) * (exp_R . f)) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) * ((exp_R . f) / ((exp_R . f) * (exp_R . f))) is V22() V23() ext-real Element of REAL
(exp_R . f) / (exp_R . f) is V22() V23() ext-real Element of REAL
((exp_R . f) / (exp_R . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) * (((exp_R . f) / (exp_R . f)) / (exp_R . f)) is V22() V23() ext-real Element of REAL
1 / (exp_R . f) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) * (1 / (exp_R . f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((sin - cos) / exp_R) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
2 * (cos . f) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / (exp_R . f) is V22() V23() ext-real Element of REAL
exp_R (#) sin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R (#) sin) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R (#) sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((exp_R (#) sin) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(sin . f) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
diff (sin,f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (diff (sin,f)) is V22() V23() ext-real Element of REAL
((sin . f) * (diff (exp_R,f))) + ((exp_R . f) * (diff (sin,f))) is V22() V23() ext-real Element of REAL
(sin . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((sin . f) * (exp_R . f)) + ((exp_R . f) * (diff (sin,f))) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(exp_R . f) * (cos . f) is V22() V23() ext-real Element of REAL
((sin . f) * (exp_R . f)) + ((exp_R . f) * (cos . f)) is V22() V23() ext-real Element of REAL
(sin . f) + (cos . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((sin . f) + (cos . f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R (#) sin) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(sin . f) + (cos . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((sin . f) + (cos . f)) is V22() V23() ext-real Element of REAL
exp_R (#) cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (exp_R (#) cos) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
(exp_R (#) cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
((exp_R (#) cos) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(cos . f) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
diff (cos,f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (diff (cos,f)) is V22() V23() ext-real Element of REAL
((cos . f) * (diff (exp_R,f))) + ((exp_R . f) * (diff (cos,f))) is V22() V23() ext-real Element of REAL
(cos . f) * (exp_R . f) is V22() V23() ext-real Element of REAL
((cos . f) * (exp_R . f)) + ((exp_R . f) * (diff (cos,f))) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
- (sin . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * (- (sin . f)) is V22() V23() ext-real Element of REAL
((cos . f) * (exp_R . f)) + ((exp_R . f) * (- (sin . f))) is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((cos . f) - (sin . f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((exp_R (#) cos) `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(cos . f) - (sin . f) is V22() V23() ext-real Element of REAL
(exp_R . f) * ((cos . f) - (sin . f)) is V22() V23() ext-real Element of REAL
sin / cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
Z is V22() V23() ext-real Element of REAL
cos . Z is V22() V23() ext-real Element of REAL
diff ((sin / cos),Z) is V22() V23() ext-real Element of REAL
(cos . Z) ^2 is V22() V23() ext-real Element of REAL
K57((cos . Z),(cos . Z)) is set
1 / ((cos . Z) ^2) is V22() V23() ext-real Element of REAL
diff (sin,Z) is V22() V23() ext-real Element of REAL
(diff (sin,Z)) * (cos . Z) is V22() V23() ext-real Element of REAL
diff (cos,Z) is V22() V23() ext-real Element of REAL
sin . Z is V22() V23() ext-real Element of REAL
(diff (cos,Z)) * (sin . Z) is V22() V23() ext-real Element of REAL
((diff (sin,Z)) * (cos . Z)) - ((diff (cos,Z)) * (sin . Z)) is V22() V23() ext-real Element of REAL
(((diff (sin,Z)) * (cos . Z)) - ((diff (cos,Z)) * (sin . Z))) / ((cos . Z) ^2) is V22() V23() ext-real Element of REAL
(cos . Z) * (cos . Z) is V22() V23() ext-real Element of REAL
((cos . Z) * (cos . Z)) - ((diff (cos,Z)) * (sin . Z)) is V22() V23() ext-real Element of REAL
(((cos . Z) * (cos . Z)) - ((diff (cos,Z)) * (sin . Z))) / ((cos . Z) ^2) is V22() V23() ext-real Element of REAL
- (sin . Z) is V22() V23() ext-real Element of REAL
(- (sin . Z)) * (sin . Z) is V22() V23() ext-real Element of REAL
((cos . Z) * (cos . Z)) - ((- (sin . Z)) * (sin . Z)) is V22() V23() ext-real Element of REAL
(((cos . Z) * (cos . Z)) - ((- (sin . Z)) * (sin . Z))) / ((cos . Z) ^2) is V22() V23() ext-real Element of REAL
(sin . Z) * (sin . Z) is V22() V23() ext-real Element of REAL
((cos . Z) * (cos . Z)) + ((sin . Z) * (sin . Z)) is V22() V23() ext-real Element of REAL
(((cos . Z) * (cos . Z)) + ((sin . Z) * (sin . Z))) / ((cos . Z) ^2) is V22() V23() ext-real Element of REAL
cos / sin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
Z is V22() V23() ext-real Element of REAL
sin . Z is V22() V23() ext-real Element of REAL
diff ((cos / sin),Z) is V22() V23() ext-real Element of REAL
(sin . Z) ^2 is V22() V23() ext-real Element of REAL
K57((sin . Z),(sin . Z)) is set
1 / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
- (1 / ((sin . Z) ^2)) is V22() V23() ext-real Element of REAL
diff (cos,Z) is V22() V23() ext-real Element of REAL
(diff (cos,Z)) * (sin . Z) is V22() V23() ext-real Element of REAL
diff (sin,Z) is V22() V23() ext-real Element of REAL
cos . Z is V22() V23() ext-real Element of REAL
(diff (sin,Z)) * (cos . Z) is V22() V23() ext-real Element of REAL
((diff (cos,Z)) * (sin . Z)) - ((diff (sin,Z)) * (cos . Z)) is V22() V23() ext-real Element of REAL
(((diff (cos,Z)) * (sin . Z)) - ((diff (sin,Z)) * (cos . Z))) / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
- (sin . Z) is V22() V23() ext-real Element of REAL
(- (sin . Z)) * (sin . Z) is V22() V23() ext-real Element of REAL
((- (sin . Z)) * (sin . Z)) - ((diff (sin,Z)) * (cos . Z)) is V22() V23() ext-real Element of REAL
(((- (sin . Z)) * (sin . Z)) - ((diff (sin,Z)) * (cos . Z))) / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
(sin . Z) * (sin . Z) is V22() V23() ext-real Element of REAL
- ((sin . Z) * (sin . Z)) is V22() V23() ext-real Element of REAL
(cos . Z) * (cos . Z) is V22() V23() ext-real Element of REAL
(- ((sin . Z) * (sin . Z))) - ((cos . Z) * (cos . Z)) is V22() V23() ext-real Element of REAL
((- ((sin . Z) * (sin . Z))) - ((cos . Z) * (cos . Z))) / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
(cos . Z) ^2 is V22() V23() ext-real Element of REAL
K57((cos . Z),(cos . Z)) is set
((cos . Z) ^2) + ((sin . Z) * (sin . Z)) is V22() V23() ext-real Element of REAL
- (((cos . Z) ^2) + ((sin . Z) * (sin . Z))) is V22() V23() ext-real Element of REAL
(- (((cos . Z) ^2) + ((sin . Z) * (sin . Z)))) / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
((cos . Z) ^2) + ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
(((cos . Z) ^2) + ((sin . Z) ^2)) / ((sin . Z) ^2) is V22() V23() ext-real Element of REAL
- ((((cos . Z) ^2) + ((sin . Z) ^2)) / ((sin . Z) ^2)) is V22() V23() ext-real Element of REAL
(#Z 2) * (sin / cos) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z 2) * (sin / cos)) is V49() V50() V51() Element of K19(REAL)
3 is V11() V21() V22() V23() ext-real V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
Z is open V49() V50() V51() Element of K19(REAL)
((#Z 2) * (sin / cos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin / cos) is V49() V50() V51() Element of K19(REAL)
f is set
f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((#Z 2) * (sin / cos)) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
2 * (sin . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(cos . f) #Z 3 is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / ((cos . f) #Z 3) is V22() V23() ext-real Element of REAL
(sin / cos) . f is V22() V23() ext-real Element of REAL
(cos . f) " is V22() V23() ext-real Element of REAL
(sin . f) * ((cos . f) ") is V22() V23() ext-real Element of REAL
1 / (cos . f) is V22() V23() ext-real Element of REAL
(sin . f) * (1 / (cos . f)) is V22() V23() ext-real Element of REAL
(sin . f) / (cos . f) is V22() V23() ext-real Element of REAL
diff (((#Z 2) * (sin / cos)),f) is V22() V23() ext-real Element of REAL
2 - 1 is V22() V23() ext-real V68() Element of REAL
((sin / cos) . f) #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (((sin / cos) . f) #Z (2 - 1)) is V22() V23() ext-real Element of REAL
diff ((sin / cos),f) is V22() V23() ext-real Element of REAL
(2 * (((sin / cos) . f) #Z (2 - 1))) * (diff ((sin / cos),f)) is V22() V23() ext-real Element of REAL
(cos . f) ^2 is V22() V23() ext-real Element of REAL
K57((cos . f),(cos . f)) is set
1 / ((cos . f) ^2) is V22() V23() ext-real Element of REAL
(2 * (((sin / cos) . f) #Z (2 - 1))) * (1 / ((cos . f) ^2)) is V22() V23() ext-real Element of REAL
((sin / cos) . f) #Z 1 is V22() V23() ext-real Element of REAL
2 * (((sin / cos) . f) #Z 1) is V22() V23() ext-real Element of REAL
(2 * (((sin / cos) . f) #Z 1)) / ((cos . f) ^2) is V22() V23() ext-real Element of REAL
2 * ((sin . f) / (cos . f)) is V22() V23() ext-real Element of REAL
(2 * ((sin . f) / (cos . f))) / ((cos . f) ^2) is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / (cos . f) is V22() V23() ext-real Element of REAL
((2 * (sin . f)) / (cos . f)) / ((cos . f) ^2) is V22() V23() ext-real Element of REAL
(cos . f) * ((cos . f) ^2) is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / ((cos . f) * ((cos . f) ^2)) is V22() V23() ext-real Element of REAL
(cos . f) #Z 2 is V22() V23() ext-real Element of REAL
(cos . f) * ((cos . f) #Z 2) is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / ((cos . f) * ((cos . f) #Z 2)) is V22() V23() ext-real Element of REAL
(cos . f) #Z 1 is V22() V23() ext-real Element of REAL
((cos . f) #Z 1) * ((cos . f) #Z 2) is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / (((cos . f) #Z 1) * ((cos . f) #Z 2)) is V22() V23() ext-real Element of REAL
1 + 2 is V22() V23() ext-real V68() Element of REAL
(cos . f) #Z (1 + 2) is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / ((cos . f) #Z (1 + 2)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((#Z 2) * (sin / cos)) `| Z) . f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
2 * (sin . f) is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
(cos . f) #Z 3 is V22() V23() ext-real Element of REAL
(2 * (sin . f)) / ((cos . f) #Z 3) is V22() V23() ext-real Element of REAL
(#Z 2) * (cos / sin) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((#Z 2) * (cos / sin)) is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
((#Z 2) * (cos / sin)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cos / sin) is V49() V50() V51() Element of K19(REAL)
f is set
f is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((#Z 2) * (cos / sin)) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
2 * (cos . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(sin . f) #Z 3 is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / ((sin . f) #Z 3) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / ((sin . f) #Z 3)) is V22() V23() ext-real Element of REAL
(cos / sin) . f is V22() V23() ext-real Element of REAL
(sin . f) " is V22() V23() ext-real Element of REAL
(cos . f) * ((sin . f) ") is V22() V23() ext-real Element of REAL
1 / (sin . f) is V22() V23() ext-real Element of REAL
(cos . f) * (1 / (sin . f)) is V22() V23() ext-real Element of REAL
(cos . f) / (sin . f) is V22() V23() ext-real Element of REAL
diff (((#Z 2) * (cos / sin)),f) is V22() V23() ext-real Element of REAL
2 - 1 is V22() V23() ext-real V68() Element of REAL
((cos / sin) . f) #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (((cos / sin) . f) #Z (2 - 1)) is V22() V23() ext-real Element of REAL
diff ((cos / sin),f) is V22() V23() ext-real Element of REAL
(2 * (((cos / sin) . f) #Z (2 - 1))) * (diff ((cos / sin),f)) is V22() V23() ext-real Element of REAL
(sin . f) ^2 is V22() V23() ext-real Element of REAL
K57((sin . f),(sin . f)) is set
1 / ((sin . f) ^2) is V22() V23() ext-real Element of REAL
- (1 / ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
(2 * (((cos / sin) . f) #Z (2 - 1))) * (- (1 / ((sin . f) ^2))) is V22() V23() ext-real Element of REAL
(2 * (((cos / sin) . f) #Z (2 - 1))) * (1 / ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
- ((2 * (((cos / sin) . f) #Z (2 - 1))) * (1 / ((sin . f) ^2))) is V22() V23() ext-real Element of REAL
((cos / sin) . f) #Z 1 is V22() V23() ext-real Element of REAL
2 * (((cos / sin) . f) #Z 1) is V22() V23() ext-real Element of REAL
(2 * (((cos / sin) . f) #Z 1)) / ((sin . f) ^2) is V22() V23() ext-real Element of REAL
- ((2 * (((cos / sin) . f) #Z 1)) / ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
2 * ((cos . f) / (sin . f)) is V22() V23() ext-real Element of REAL
(2 * ((cos . f) / (sin . f))) / ((sin . f) ^2) is V22() V23() ext-real Element of REAL
- ((2 * ((cos . f) / (sin . f))) / ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / (sin . f) is V22() V23() ext-real Element of REAL
((2 * (cos . f)) / (sin . f)) / ((sin . f) ^2) is V22() V23() ext-real Element of REAL
- (((2 * (cos . f)) / (sin . f)) / ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
(sin . f) * ((sin . f) ^2) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / ((sin . f) * ((sin . f) ^2)) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / ((sin . f) * ((sin . f) ^2))) is V22() V23() ext-real Element of REAL
(sin . f) #Z 2 is V22() V23() ext-real Element of REAL
(sin . f) * ((sin . f) #Z 2) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / ((sin . f) * ((sin . f) #Z 2)) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / ((sin . f) * ((sin . f) #Z 2))) is V22() V23() ext-real Element of REAL
(sin . f) #Z 1 is V22() V23() ext-real Element of REAL
((sin . f) #Z 1) * ((sin . f) #Z 2) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / (((sin . f) #Z 1) * ((sin . f) #Z 2)) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / (((sin . f) #Z 1) * ((sin . f) #Z 2))) is V22() V23() ext-real Element of REAL
1 + 2 is V22() V23() ext-real V68() Element of REAL
(sin . f) #Z (1 + 2) is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / ((sin . f) #Z (1 + 2)) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / ((sin . f) #Z (1 + 2))) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(((#Z 2) * (cos / sin)) `| Z) . f is V22() V23() ext-real Element of REAL
cos . f is V22() V23() ext-real Element of REAL
2 * (cos . f) is V22() V23() ext-real Element of REAL
sin . f is V22() V23() ext-real Element of REAL
(sin . f) #Z 3 is V22() V23() ext-real Element of REAL
(2 * (cos . f)) / ((sin . f) #Z 3) is V22() V23() ext-real Element of REAL
- ((2 * (cos . f)) / ((sin . f) #Z 3)) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(sin / cos) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((sin / cos) * f) is V49() V50() V51() Element of K19(REAL)
((sin / cos) * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
(1 / 2) * x is V22() V23() ext-real Element of REAL
((1 / 2) * x) + 0 is V22() V23() ext-real Element of REAL
x / 2 is V22() V23() ext-real Element of REAL
dom f is V49() V50() V51() Element of K19(REAL)
x is set
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
cos . (f . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((sin / cos) * f) `| Z) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
1 + (cos . x) is V22() V23() ext-real Element of REAL
1 / (1 + (cos . x)) is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
cos . (f . x) is V22() V23() ext-real Element of REAL
diff (((sin / cos) * f),x) is V22() V23() ext-real Element of REAL
diff ((sin / cos),(f . x)) is V22() V23() ext-real Element of REAL
diff (f,x) is V22() V23() ext-real Element of REAL
(diff ((sin / cos),(f . x))) * (diff (f,x)) is V22() V23() ext-real Element of REAL
(cos . (f . x)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (f . x)),(cos . (f . x))) is set
1 / ((cos . (f . x)) ^2) is V22() V23() ext-real Element of REAL
(1 / ((cos . (f . x)) ^2)) * (diff (f,x)) is V22() V23() ext-real Element of REAL
(diff (f,x)) / ((cos . (f . x)) ^2) is V22() V23() ext-real Element of REAL
x / 2 is V22() V23() ext-real Element of REAL
cos . (x / 2) is V22() V23() ext-real Element of REAL
(cos . (x / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (x / 2)),(cos . (x / 2))) is set
(diff (f,x)) / ((cos . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
f `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| Z) . x is V22() V23() ext-real Element of REAL
((f `| Z) . x) / ((cos . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
(1 / 2) / ((cos . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
2 * ((cos . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
1 / (2 * ((cos . (x / 2)) ^2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((sin / cos) * f) `| Z) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
1 + (cos . x) is V22() V23() ext-real Element of REAL
1 / (1 + (cos . x)) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(cos / sin) * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((cos / sin) * f) is V49() V50() V51() Element of K19(REAL)
((cos / sin) * f) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
(1 / 2) * x is V22() V23() ext-real Element of REAL
((1 / 2) * x) + 0 is V22() V23() ext-real Element of REAL
x / 2 is V22() V23() ext-real Element of REAL
dom f is V49() V50() V51() Element of K19(REAL)
x is set
x is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
sin . (f . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((cos / sin) * f) `| Z) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
1 - (cos . x) is V22() V23() ext-real Element of REAL
1 / (1 - (cos . x)) is V22() V23() ext-real Element of REAL
- (1 / (1 - (cos . x))) is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
sin . (f . x) is V22() V23() ext-real Element of REAL
diff (((cos / sin) * f),x) is V22() V23() ext-real Element of REAL
diff ((cos / sin),(f . x)) is V22() V23() ext-real Element of REAL
diff (f,x) is V22() V23() ext-real Element of REAL
(diff ((cos / sin),(f . x))) * (diff (f,x)) is V22() V23() ext-real Element of REAL
(sin . (f . x)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (f . x)),(sin . (f . x))) is set
1 / ((sin . (f . x)) ^2) is V22() V23() ext-real Element of REAL
- (1 / ((sin . (f . x)) ^2)) is V22() V23() ext-real Element of REAL
(- (1 / ((sin . (f . x)) ^2))) * (diff (f,x)) is V22() V23() ext-real Element of REAL
(1 / ((sin . (f . x)) ^2)) * (diff (f,x)) is V22() V23() ext-real Element of REAL
- ((1 / ((sin . (f . x)) ^2)) * (diff (f,x))) is V22() V23() ext-real Element of REAL
(diff (f,x)) / ((sin . (f . x)) ^2) is V22() V23() ext-real Element of REAL
- ((diff (f,x)) / ((sin . (f . x)) ^2)) is V22() V23() ext-real Element of REAL
x / 2 is V22() V23() ext-real Element of REAL
sin . (x / 2) is V22() V23() ext-real Element of REAL
(sin . (x / 2)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (x / 2)),(sin . (x / 2))) is set
(diff (f,x)) / ((sin . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
- ((diff (f,x)) / ((sin . (x / 2)) ^2)) is V22() V23() ext-real Element of REAL
f `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| Z) . x is V22() V23() ext-real Element of REAL
((f `| Z) . x) / ((sin . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
- (((f `| Z) . x) / ((sin . (x / 2)) ^2)) is V22() V23() ext-real Element of REAL
(1 / 2) / ((sin . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
- ((1 / 2) / ((sin . (x / 2)) ^2)) is V22() V23() ext-real Element of REAL
2 * ((sin . (x / 2)) ^2) is V22() V23() ext-real Element of REAL
1 / (2 * ((sin . (x / 2)) ^2)) is V22() V23() ext-real Element of REAL
- (1 / (2 * ((sin . (x / 2)) ^2))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((cos / sin) * f) `| Z) . x is V22() V23() ext-real Element of REAL
cos . x is V22() V23() ext-real Element of REAL
1 - (cos . x) is V22() V23() ext-real Element of REAL
1 / (1 - (cos . x)) is V22() V23() ext-real Element of REAL
- (1 / (1 - (cos . x))) is V22() V23() ext-real Element of REAL