:: FDIFF_8 semantic presentation

REAL is V11() V49() V50() V51() V55() V70() set
NAT is V11() V15() V16() V17() V49() V50() V51() V52() V53() V54() V55() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V11() V49() V55() V70() set
0 is V11() V15() V16() V17() V19() V20() V21() V23() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V68() set
1 is V11() V15() V16() V17() V21() V22() V23() ext-real positive non negative V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
{0,1} is V11() V49() V50() V51() V52() V53() V54() set
INT is V11() V49() V50() V51() V52() V53() V55() V70() 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,()) is set
K19(K20(NAT,())) is set
RAT is V11() V49() V50() V51() V52() V55() V70() set
NAT is V11() V15() V16() V17() V49() V50() V51() V52() V53() V54() V55() set
K19(NAT) is set
K19(NAT) 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() V30( REAL , REAL ) 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)
0 is V11() V15() V16() V17() V19() V20() V21() V22() V23() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V68() V69() Element of NAT
right_open_halfline 0 is V49() V50() V51() Element of K19(REAL)

K138(0,+infty) is set
rng ln is V49() V50() V51() Element of K19(REAL)
2 is V11() V15() V16() V17() V21() V22() V23() ext-real positive non negative V49() V50() V51() V52() V53() V54() V68() V69() Element of NAT
cos is V1() V4( REAL ) V5( REAL ) V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
sin is V1() V4( REAL ) V5( REAL ) V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
sin / cos is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cos / sin is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
#Z 2 is V1() V4( REAL ) V5( REAL ) V6() V30( 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))
is V11() V49() V50() V51() V52() V53() V54() set
tan is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom tan is V49() V50() V51() Element of K19(REAL)
Z is V22() V23() ext-real Element of REAL
cos . Z is V22() V23() ext-real Element of REAL
dom sin is V49() V50() V51() Element of K19(REAL)
dom cos is V49() V50() V51() Element of K19(REAL)
cos " is V49() V50() V51() Element of K19(REAL)
() \ () is V49() V50() V51() Element of K19(REAL)
() /\ (() \ ()) is V49() V50() V51() Element of K19(REAL)
dom () is V49() V50() V51() Element of K19(REAL)
cot is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom cot is V49() V50() V51() Element of K19(REAL)
Z is V22() V23() ext-real Element of REAL
sin . Z is V22() V23() ext-real Element of REAL
dom cos is V49() V50() V51() Element of K19(REAL)
dom sin is V49() V50() V51() Element of K19(REAL)
sin " is V49() V50() V51() Element of K19(REAL)
() \ () is V49() V50() V51() Element of K19(REAL)
() /\ (() \ ()) is V49() V50() V51() Element of K19(REAL)
sin ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom () is V49() V50() V51() Element of K19(REAL)
Z is V15() V16() V17() V21() V23() ext-real V68() 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))
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))
dom (x / f) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
(x / f) . x is V22() V23() ext-real Element of REAL
((x / f) . x) #Z Z is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
(x . x) #Z Z is V22() V23() ext-real Element of REAL
f . x is V22() V23() ext-real Element of REAL
(f . x) #Z Z is V22() V23() ext-real Element of REAL
((x . x) #Z Z) / ((f . x) #Z Z) is V22() V23() ext-real Element of REAL
K59(((f . x) #Z Z)) is V22() set
K57(((x . x) #Z Z),K59(((f . x) #Z Z))) is set
(x . x) / (f . x) is V22() V23() ext-real Element of REAL
K59((f . x)) is V22() set
K57((x . x),K59((f . x))) is set
((x . x) / (f . x)) #Z Z is V22() V23() ext-real Element of REAL
((x . x) / (f . x)) |^ Z is V22() V23() ext-real Element of REAL
(x . x) |^ Z is V22() V23() ext-real Element of REAL
(f . x) |^ Z is V22() V23() ext-real Element of REAL
((x . x) |^ Z) / ((f . x) |^ Z) is V22() V23() ext-real Element of REAL
K59(((f . x) |^ Z)) is V22() set
K57(((x . x) |^ Z),K59(((f . x) |^ Z))) is set
((x . x) #Z Z) / ((f . x) |^ Z) is V22() V23() ext-real Element of REAL
K57(((x . x) #Z Z),K59(((f . x) |^ Z))) is set
Z 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
(- Z) - f is V22() V23() ext-real Element of REAL
K58(f) is V22() set
K56((- Z),K58(f)) is set
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))
x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f / x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (f / x) is V49() V50() V51() Element of K19(REAL)
(f / x) `| 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 x is V49() V50() V51() Element of K19(REAL)
x " is V49() V50() V51() Element of K19(REAL)
(dom x) \ (x " ) is V49() V50() V51() Element of K19(REAL)
(dom f) /\ ((dom x) \ (x " )) is V49() V50() V51() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
x . f2 is V22() V23() ext-real Element of REAL
x ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x ^) 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
f2 - (- Z) is V22() V23() ext-real Element of REAL
K58((- Z)) is V22() set
K56(f2,K58((- Z))) is set
x . f2 is V22() V23() ext-real Element of REAL
f2 - f is V22() V23() ext-real Element of REAL
K56(f2,K58(f)) is set
f2 is V22() V23() ext-real Element of REAL
((f / x) `| x) . f2 is V22() V23() ext-real Element of REAL
f2 - f is V22() V23() ext-real Element of REAL
K56(f2,K58(f)) is set
(f2 - f) ^2 is V22() V23() ext-real Element of REAL
K57((f2 - f),(f2 - f)) is set
((- Z) - f) / ((f2 - f) ^2) is V22() V23() ext-real Element of REAL
K59(((f2 - f) ^2)) is V22() set
K57(((- Z) - f),K59(((f2 - f) ^2))) is set
{ b1 where b1 is V22() V23() ext-real Element of REAL : not b1 <= 0 } is set
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) ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
ln * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (ln * ((id Z) ^)) is V49() V50() V51() Element of K19(REAL)
(ln * ((id Z) ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) ^) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
(id Z) . x is V22() V23() ext-real Element of REAL
((id Z) . x) " is V22() V23() ext-real Element of REAL
1 / x is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
f is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(id Z) . x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
((id Z) . x) " is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
diff ((ln * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
(diff (((id Z) ^),x)) / (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
K59((((id Z) ^) . x)) is V22() set
K57((diff (((id Z) ^),x)),K59((((id Z) ^) . x))) is set
x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((ln * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
1 / x is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
- (1 / x) is V22() V23() ext-real Element of REAL
(id Z) . x is V22() V23() ext-real Element of REAL
diff ((ln * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
(diff (((id Z) ^),x)) / (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
K59((((id Z) ^) . x)) is V22() set
K57((diff (((id Z) ^),x)),K59((((id Z) ^) . x))) is set
((id Z) ^) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) ^) `| Z) . x is V22() V23() ext-real Element of REAL
((((id Z) ^) `| Z) . x) / (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
K57(((((id Z) ^) `| Z) . x),K59((((id Z) ^) . x))) is set
((id Z) . x) " is V22() V23() ext-real Element of REAL
((((id Z) ^) `| Z) . x) / (((id Z) . x) ") is V22() V23() ext-real Element of REAL
K59((((id Z) . x) ")) is V22() set
K57(((((id Z) ^) `| Z) . x),K59((((id Z) . x) "))) is set
x " is V22() V23() ext-real Element of REAL
1 * (x ") is V22() V23() ext-real Element of REAL
((((id Z) ^) `| Z) . x) / (1 * (x ")) is V22() V23() ext-real Element of REAL
K59((1 * (x "))) is V22() set
K57(((((id Z) ^) `| Z) . x),K59((1 * (x ")))) is set
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
K59((x ^2)) is V22() set
K57(1,K59((x ^2))) is set
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
(- (1 / (x ^2))) / (1 * (x ")) is V22() V23() ext-real Element of REAL
K57((- (1 / (x ^2))),K59((1 * (x ")))) is set
x / (x ^2) is V22() V23() ext-real Element of REAL
K57(x,K59((x ^2))) is set
- (x / (x ^2)) is V22() V23() ext-real Element of REAL
x / x is V22() V23() ext-real Element of REAL
K57(x,K59(x)) is set
(x / x) / x is V22() V23() ext-real Element of REAL
K57((x / x),K59(x)) is set
- ((x / x) / x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((ln * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
1 / x is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
- (1 / x) 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))
tan * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (tan * f) is V49() V50() V51() Element of K19(REAL)
(tan * 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)
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
dom () 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
cos . (f . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((tan * f) `| x) . x is V22() V23() ext-real Element of REAL
Z * x is V22() V23() ext-real Element of REAL
(Z * x) + f is V22() V23() ext-real Element of REAL
cos . ((Z * x) + f) is V22() V23() ext-real Element of REAL
(cos . ((Z * x) + f)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ((Z * x) + f)),(cos . ((Z * x) + f))) is set
Z / ((cos . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ((Z * x) + f)) ^2)) is V22() set
K57(Z,K59(((cos . ((Z * x) + f)) ^2))) is set
f . x is V22() V23() ext-real Element of REAL
cos . (f . x) is V22() V23() ext-real Element of REAL
diff ((tan * f),x) is V22() V23() ext-real Element of REAL
diff (tan,(f . x)) is V22() V23() ext-real Element of REAL
diff (f,x) is V22() V23() ext-real Element of REAL
(diff (tan,(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
K59(((cos . (f . x)) ^2)) is V22() set
K57(1,K59(((cos . (f . x)) ^2))) is set
(1 / ((cos . (f . x)) ^2)) * (diff (f,x)) is V22() V23() ext-real Element of REAL
(diff (f,x)) / ((cos . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K57((diff (f,x)),K59(((cos . ((Z * x) + f)) ^2))) is set
f `| x is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(f `| x) . x is V22() V23() ext-real Element of REAL
((f `| x) . x) / ((cos . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K57(((f `| x) . x),K59(((cos . ((Z * x) + f)) ^2))) is set
x is V22() V23() ext-real Element of REAL
((tan * f) `| x) . x is V22() V23() ext-real Element of REAL
Z * x is V22() V23() ext-real Element of REAL
(Z * x) + f is V22() V23() ext-real Element of REAL
cos . ((Z * x) + f) is V22() V23() ext-real Element of REAL
(cos . ((Z * x) + f)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ((Z * x) + f)),(cos . ((Z * x) + f))) is set
Z / ((cos . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ((Z * x) + f)) ^2)) is V22() set
K57(Z,K59(((cos . ((Z * x) + f)) ^2))) is set
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))
cot * f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cot * f) is V49() V50() V51() Element of K19(REAL)
(cot * 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)
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
dom () 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
sin . (f . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * f) `| x) . x is V22() V23() ext-real Element of REAL
Z * x is V22() V23() ext-real Element of REAL
(Z * x) + f is V22() V23() ext-real Element of REAL
sin . ((Z * x) + f) is V22() V23() ext-real Element of REAL
(sin . ((Z * x) + f)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ((Z * x) + f)),(sin . ((Z * x) + f))) is set
Z / ((sin . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ((Z * x) + f)) ^2)) is V22() set
K57(Z,K59(((sin . ((Z * x) + f)) ^2))) is set
- (Z / ((sin . ((Z * x) + f)) ^2)) 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 ((cot * f),x) is V22() V23() ext-real Element of REAL
diff (cot,(f . x)) is V22() V23() ext-real Element of REAL
diff (f,x) is V22() V23() ext-real Element of REAL
(diff (cot,(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
K59(((sin . (f . x)) ^2)) is V22() set
K57(1,K59(((sin . (f . x)) ^2))) is set
- (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
(diff (f,x)) / ((sin . (f . x)) ^2) is V22() V23() ext-real Element of REAL
K57((diff (f,x)),K59(((sin . (f . x)) ^2))) is set
- ((diff (f,x)) / ((sin . (f . x)) ^2)) is V22() V23() ext-real Element of REAL
(diff (f,x)) / ((sin . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K57((diff (f,x)),K59(((sin . ((Z * x) + f)) ^2))) is set
- ((diff (f,x)) / ((sin . ((Z * x) + f)) ^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) . x is V22() V23() ext-real Element of REAL
((f `| x) . x) / ((sin . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K57(((f `| x) . x),K59(((sin . ((Z * x) + f)) ^2))) is set
- (((f `| x) . x) / ((sin . ((Z * x) + f)) ^2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * f) `| x) . x is V22() V23() ext-real Element of REAL
Z * x is V22() V23() ext-real Element of REAL
(Z * x) + f is V22() V23() ext-real Element of REAL
sin . ((Z * x) + f) is V22() V23() ext-real Element of REAL
(sin . ((Z * x) + f)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ((Z * x) + f)),(sin . ((Z * x) + f))) is set
Z / ((sin . ((Z * x) + f)) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ((Z * x) + f)) ^2)) is V22() set
K57(Z,K59(((sin . ((Z * x) + f)) ^2))) is set
- (Z / ((sin . ((Z * x) + 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) ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
tan * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (tan * ((id Z) ^)) is V49() V50() V51() Element of K19(REAL)
(tan * ((id Z) ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) ^) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
cos . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
dom () is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
cos . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((tan * ((id Z) ^)) `| Z) . 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 is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
cos . (1 / x) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (1 / x)),(cos . (1 / x))) is set
(x ^2) * ((cos . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
1 / ((x ^2) * ((cos . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K59(((x ^2) * ((cos . (1 / x)) ^2))) is V22() set
K57(1,K59(((x ^2) * ((cos . (1 / x)) ^2)))) is set
- (1 / ((x ^2) * ((cos . (1 / x)) ^2))) is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
cos . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
diff ((tan * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (tan,(((id Z) ^) . x)) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
(diff (tan,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
(cos . (((id Z) ^) . x)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (((id Z) ^) . x)),(cos . (((id Z) ^) . x))) is set
1 / ((cos . (((id Z) ^) . x)) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . (((id Z) ^) . x)) ^2)) is V22() set
K57(1,K59(((cos . (((id Z) ^) . x)) ^2))) is set
(1 / ((cos . (((id Z) ^) . x)) ^2)) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
(id Z) . x is V22() V23() ext-real Element of REAL
((id Z) . x) " is V22() V23() ext-real Element of REAL
cos . (((id Z) . x) ") is V22() V23() ext-real Element of REAL
(cos . (((id Z) . x) ")) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (((id Z) . x) ")),(cos . (((id Z) . x) "))) is set
(diff (((id Z) ^),x)) / ((cos . (((id Z) . x) ")) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . (((id Z) . x) ")) ^2)) is V22() set
K57((diff (((id Z) ^),x)),K59(((cos . (((id Z) . x) ")) ^2))) is set
x " is V22() V23() ext-real Element of REAL
1 * (x ") is V22() V23() ext-real Element of REAL
cos . (1 * (x ")) is V22() V23() ext-real Element of REAL
(cos . (1 * (x "))) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (1 * (x "))),(cos . (1 * (x ")))) is set
(diff (((id Z) ^),x)) / ((cos . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . (1 * (x "))) ^2)) is V22() set
K57((diff (((id Z) ^),x)),K59(((cos . (1 * (x "))) ^2))) is set
((id Z) ^) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) ^) `| Z) . x is V22() V23() ext-real Element of REAL
((((id Z) ^) `| Z) . x) / ((cos . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K57(((((id Z) ^) `| Z) . x),K59(((cos . (1 * (x "))) ^2))) is set
1 / (x ^2) is V22() V23() ext-real Element of REAL
K59((x ^2)) is V22() set
K57(1,K59((x ^2))) is set
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
(- (1 / (x ^2))) / ((cos . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K57((- (1 / (x ^2))),K59(((cos . (1 * (x "))) ^2))) is set
- 1 is V22() V23() ext-real V68() Element of REAL
(- 1) / (x ^2) is V22() V23() ext-real Element of REAL
K57((- 1),K59((x ^2))) is set
((- 1) / (x ^2)) / ((cos . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . (1 / x)) ^2)) is V22() set
K57(((- 1) / (x ^2)),K59(((cos . (1 / x)) ^2))) is set
(- 1) / ((x ^2) * ((cos . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K57((- 1),K59(((x ^2) * ((cos . (1 / x)) ^2)))) is set
x is V22() V23() ext-real Element of REAL
((tan * ((id Z) ^)) `| Z) . 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 is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
cos . (1 / x) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . (1 / x)),(cos . (1 / x))) is set
(x ^2) * ((cos . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
1 / ((x ^2) * ((cos . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K59(((x ^2) * ((cos . (1 / x)) ^2))) is V22() set
K57(1,K59(((x ^2) * ((cos . (1 / x)) ^2)))) is set
- (1 / ((x ^2) * ((cos . (1 / x)) ^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) ^ is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cot * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cot * ((id Z) ^)) is V49() V50() V51() Element of K19(REAL)
(cot * ((id Z) ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) ^) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
sin . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
dom () is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
sin . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * ((id Z) ^)) `| Z) . 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 is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
sin . (1 / x) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (1 / x)),(sin . (1 / x))) is set
(x ^2) * ((sin . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
1 / ((x ^2) * ((sin . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K59(((x ^2) * ((sin . (1 / x)) ^2))) is V22() set
K57(1,K59(((x ^2) * ((sin . (1 / x)) ^2)))) is set
((id Z) ^) . x is V22() V23() ext-real Element of REAL
sin . (((id Z) ^) . x) is V22() V23() ext-real Element of REAL
diff ((cot * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (cot,(((id Z) ^) . x)) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
(diff (cot,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
(sin . (((id Z) ^) . x)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (((id Z) ^) . x)),(sin . (((id Z) ^) . x))) is set
1 / ((sin . (((id Z) ^) . x)) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . (((id Z) ^) . x)) ^2)) is V22() set
K57(1,K59(((sin . (((id Z) ^) . x)) ^2))) is set
- (1 / ((sin . (((id Z) ^) . x)) ^2)) is V22() V23() ext-real Element of REAL
(- (1 / ((sin . (((id Z) ^) . x)) ^2))) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
(diff (((id Z) ^),x)) / ((sin . (((id Z) ^) . x)) ^2) is V22() V23() ext-real Element of REAL
K57((diff (((id Z) ^),x)),K59(((sin . (((id Z) ^) . x)) ^2))) is set
- ((diff (((id Z) ^),x)) / ((sin . (((id Z) ^) . x)) ^2)) is V22() V23() ext-real Element of REAL
(id Z) . x is V22() V23() ext-real Element of REAL
((id Z) . x) " is V22() V23() ext-real Element of REAL
sin . (((id Z) . x) ") is V22() V23() ext-real Element of REAL
(sin . (((id Z) . x) ")) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (((id Z) . x) ")),(sin . (((id Z) . x) "))) is set
(diff (((id Z) ^),x)) / ((sin . (((id Z) . x) ")) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . (((id Z) . x) ")) ^2)) is V22() set
K57((diff (((id Z) ^),x)),K59(((sin . (((id Z) . x) ")) ^2))) is set
- ((diff (((id Z) ^),x)) / ((sin . (((id Z) . x) ")) ^2)) is V22() V23() ext-real Element of REAL
x " is V22() V23() ext-real Element of REAL
1 * (x ") is V22() V23() ext-real Element of REAL
sin . (1 * (x ")) is V22() V23() ext-real Element of REAL
(sin . (1 * (x "))) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (1 * (x "))),(sin . (1 * (x ")))) is set
(diff (((id Z) ^),x)) / ((sin . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . (1 * (x "))) ^2)) is V22() set
K57((diff (((id Z) ^),x)),K59(((sin . (1 * (x "))) ^2))) is set
- ((diff (((id Z) ^),x)) / ((sin . (1 * (x "))) ^2)) 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) . x is V22() V23() ext-real Element of REAL
((((id Z) ^) `| Z) . x) / ((sin . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K57(((((id Z) ^) `| Z) . x),K59(((sin . (1 * (x "))) ^2))) is set
- (((((id Z) ^) `| Z) . x) / ((sin . (1 * (x "))) ^2)) is V22() V23() ext-real Element of REAL
1 / (x ^2) is V22() V23() ext-real Element of REAL
K59((x ^2)) is V22() set
K57(1,K59((x ^2))) is set
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
(- (1 / (x ^2))) / ((sin . (1 * (x "))) ^2) is V22() V23() ext-real Element of REAL
K57((- (1 / (x ^2))),K59(((sin . (1 * (x "))) ^2))) is set
- ((- (1 / (x ^2))) / ((sin . (1 * (x "))) ^2)) is V22() V23() ext-real Element of REAL
- 1 is V22() V23() ext-real V68() Element of REAL
(- 1) / (x ^2) is V22() V23() ext-real Element of REAL
K57((- 1),K59((x ^2))) is set
((- 1) / (x ^2)) / ((sin . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . (1 / x)) ^2)) is V22() set
K57(((- 1) / (x ^2)),K59(((sin . (1 / x)) ^2))) is set
- (((- 1) / (x ^2)) / ((sin . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
(- 1) / ((x ^2) * ((sin . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K57((- 1),K59(((x ^2) * ((sin . (1 / x)) ^2)))) is set
- ((- 1) / ((x ^2) * ((sin . (1 / x)) ^2))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * ((id Z) ^)) `| Z) . 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 is V22() V23() ext-real Element of REAL
K59(x) is V22() set
K57(1,K59(x)) is set
sin . (1 / x) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . (1 / x)),(sin . (1 / x))) is set
(x ^2) * ((sin . (1 / x)) ^2) is V22() V23() ext-real Element of REAL
1 / ((x ^2) * ((sin . (1 / x)) ^2)) is V22() V23() ext-real Element of REAL
K59(((x ^2) * ((sin . (1 / x)) ^2))) is V22() set
K57(1,K59(((x ^2) * ((sin . (1 / x)) ^2)))) is set
Z is V22() V23() ext-real Element of REAL
2 * Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
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))
f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
Z (#) f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x + (Z (#) f2) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
tan * (x + (Z (#) f2)) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (tan * (x + (Z (#) f2))) is V49() V50() V51() Element of K19(REAL)
(tan * (x + (Z (#) f2))) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x + (Z (#) f2)) is V49() V50() V51() Element of K19(REAL)
dom x is V49() V50() V51() Element of K19(REAL)
dom (Z (#) f2) is V49() V50() V51() Element of K19(REAL)
(dom x) /\ (dom (Z (#) f2)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
dom () is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((tan * (x + (Z (#) f2))) `| f) . x is V22() V23() ext-real Element of REAL
(2 * Z) * x is V22() V23() ext-real Element of REAL
x + ((2 * Z) * x) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
f + (x * x) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
Z * (x ^2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x ^2)) is V22() V23() ext-real Element of REAL
cos . ((f + (x * x)) + (Z * (x ^2))) is V22() V23() ext-real Element of REAL
(cos . ((f + (x * x)) + (Z * (x ^2)))) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ((f + (x * x)) + (Z * (x ^2)))),(cos . ((f + (x * x)) + (Z * (x ^2))))) is set
(x + ((2 * Z) * x)) / ((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() set
K57((x + ((2 * Z) * x)),K59(((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
(Z (#) f2) . x is V22() V23() ext-real Element of REAL
(x . x) + ((Z (#) f2) . x) is V22() V23() ext-real Element of REAL
f2 . x is V22() V23() ext-real Element of REAL
Z * (f2 . x) is V22() V23() ext-real Element of REAL
(x . x) + (Z * (f2 . x)) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (f2 . x)) is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
Z * (x #Z 2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x #Z 2)) is V22() V23() ext-real Element of REAL
x |^ 2 is V22() V23() ext-real Element of REAL
Z * (x |^ 2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x |^ 2)) is V22() V23() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
diff ((tan * (x + (Z (#) f2))),x) is V22() V23() ext-real Element of REAL
diff (tan,((x + (Z (#) f2)) . x)) is V22() V23() ext-real Element of REAL
diff ((x + (Z (#) f2)),x) is V22() V23() ext-real Element of REAL
(diff (tan,((x + (Z (#) f2)) . x))) * (diff ((x + (Z (#) f2)),x)) is V22() V23() ext-real Element of REAL
(cos . ((x + (Z (#) f2)) . x)) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ((x + (Z (#) f2)) . x)),(cos . ((x + (Z (#) f2)) . x))) is set
1 / ((cos . ((x + (Z (#) f2)) . x)) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ((x + (Z (#) f2)) . x)) ^2)) is V22() set
K57(1,K59(((cos . ((x + (Z (#) f2)) . x)) ^2))) is set
(1 / ((cos . ((x + (Z (#) f2)) . x)) ^2)) * (diff ((x + (Z (#) f2)),x)) is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((x + (Z (#) f2)) `| f) . x is V22() V23() ext-real Element of REAL
(((x + (Z (#) f2)) `| f) . x) / ((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K57((((x + (Z (#) f2)) `| f) . x),K59(((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
x is V22() V23() ext-real Element of REAL
((tan * (x + (Z (#) f2))) `| f) . x is V22() V23() ext-real Element of REAL
(2 * Z) * x is V22() V23() ext-real Element of REAL
x + ((2 * Z) * x) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
f + (x * x) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
Z * (x ^2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x ^2)) is V22() V23() ext-real Element of REAL
cos . ((f + (x * x)) + (Z * (x ^2))) is V22() V23() ext-real Element of REAL
(cos . ((f + (x * x)) + (Z * (x ^2)))) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ((f + (x * x)) + (Z * (x ^2)))),(cos . ((f + (x * x)) + (Z * (x ^2))))) is set
(x + ((2 * Z) * x)) / ((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() set
K57((x + ((2 * Z) * x)),K59(((cos . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
Z is V22() V23() ext-real Element of REAL
2 * Z is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
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))
f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
Z (#) f2 is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x + (Z (#) f2) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cot * (x + (Z (#) f2)) is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cot * (x + (Z (#) f2))) is V49() V50() V51() Element of K19(REAL)
(cot * (x + (Z (#) f2))) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x + (Z (#) f2)) is V49() V50() V51() Element of K19(REAL)
dom x is V49() V50() V51() Element of K19(REAL)
dom (Z (#) f2) is V49() V50() V51() Element of K19(REAL)
(dom x) /\ (dom (Z (#) f2)) is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
dom () is V49() V50() V51() Element of K19(REAL)
x is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * (x + (Z (#) f2))) `| f) . x is V22() V23() ext-real Element of REAL
(2 * Z) * x is V22() V23() ext-real Element of REAL
x + ((2 * Z) * x) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
f + (x * x) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
Z * (x ^2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x ^2)) is V22() V23() ext-real Element of REAL
sin . ((f + (x * x)) + (Z * (x ^2))) is V22() V23() ext-real Element of REAL
(sin . ((f + (x * x)) + (Z * (x ^2)))) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ((f + (x * x)) + (Z * (x ^2)))),(sin . ((f + (x * x)) + (Z * (x ^2))))) is set
(x + ((2 * Z) * x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() set
K57((x + ((2 * Z) * x)),K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
- ((x + ((2 * Z) * x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) . x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
(Z (#) f2) . x is V22() V23() ext-real Element of REAL
(x . x) + ((Z (#) f2) . x) is V22() V23() ext-real Element of REAL
f2 . x is V22() V23() ext-real Element of REAL
Z * (f2 . x) is V22() V23() ext-real Element of REAL
(x . x) + (Z * (f2 . x)) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (f2 . x)) is V22() V23() ext-real Element of REAL
x #Z 2 is V22() V23() ext-real Element of REAL
Z * (x #Z 2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x #Z 2)) is V22() V23() ext-real Element of REAL
x |^ 2 is V22() V23() ext-real Element of REAL
Z * (x |^ 2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x |^ 2)) is V22() V23() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V22() V23() ext-real Element of REAL
diff ((cot * (x + (Z (#) f2))),x) is V22() V23() ext-real Element of REAL
diff (cot,((x + (Z (#) f2)) . x)) is V22() V23() ext-real Element of REAL
diff ((x + (Z (#) f2)),x) is V22() V23() ext-real Element of REAL
(diff (cot,((x + (Z (#) f2)) . x))) * (diff ((x + (Z (#) f2)),x)) is V22() V23() ext-real Element of REAL
(sin . ((x + (Z (#) f2)) . x)) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ((x + (Z (#) f2)) . x)),(sin . ((x + (Z (#) f2)) . x))) is set
1 / ((sin . ((x + (Z (#) f2)) . x)) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ((x + (Z (#) f2)) . x)) ^2)) is V22() set
K57(1,K59(((sin . ((x + (Z (#) f2)) . x)) ^2))) is set
- (1 / ((sin . ((x + (Z (#) f2)) . x)) ^2)) is V22() V23() ext-real Element of REAL
(- (1 / ((sin . ((x + (Z (#) f2)) . x)) ^2))) * (diff ((x + (Z (#) f2)),x)) is V22() V23() ext-real Element of REAL
(diff ((x + (Z (#) f2)),x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K57((diff ((x + (Z (#) f2)),x)),K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
- ((diff ((x + (Z (#) f2)),x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() V23() ext-real Element of REAL
(x + (Z (#) f2)) `| f is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((x + (Z (#) f2)) `| f) . x is V22() V23() ext-real Element of REAL
(((x + (Z (#) f2)) `| f) . x) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K57((((x + (Z (#) f2)) `| f) . x),K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
- ((((x + (Z (#) f2)) `| f) . x) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cot * (x + (Z (#) f2))) `| f) . x is V22() V23() ext-real Element of REAL
(2 * Z) * x is V22() V23() ext-real Element of REAL
x + ((2 * Z) * x) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
f + (x * x) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
Z * (x ^2) is V22() V23() ext-real Element of REAL
(f + (x * x)) + (Z * (x ^2)) is V22() V23() ext-real Element of REAL
sin . ((f + (x * x)) + (Z * (x ^2))) is V22() V23() ext-real Element of REAL
(sin . ((f + (x * x)) + (Z * (x ^2)))) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ((f + (x * x)) + (Z * (x ^2)))),(sin . ((f + (x * x)) + (Z * (x ^2))))) is set
(x + ((2 * Z) * x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() set
K57((x + ((2 * Z) * x)),K59(((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2))) is set
- ((x + ((2 * Z) * x)) / ((sin . ((f + (x * x)) + (Z * (x ^2)))) ^2)) is V22() V23() ext-real Element of REAL
tan * exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom () is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
() `| 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
cos . () is V22() V23() ext-real Element of REAL
dom () 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
cos . () is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(() `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
cos . () is V22() V23() ext-real Element of REAL
(cos . ()) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ()),(cos . ())) is set
() / ((cos . ()) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ()) ^2)) is V22() set
K57((),K59(((cos . ()) ^2))) is set
diff ((),f) is V22() V23() ext-real Element of REAL
diff (tan,()) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (tan,())) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
1 / ((cos . ()) ^2) is V22() V23() ext-real Element of REAL
K57(1,K59(((cos . ()) ^2))) is set
(1 / ((cos . ()) ^2)) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(() `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
cos . () is V22() V23() ext-real Element of REAL
(cos . ()) ^2 is V22() V23() ext-real Element of REAL
K57((cos . ()),(cos . ())) is set
() / ((cos . ()) ^2) is V22() V23() ext-real Element of REAL
K59(((cos . ()) ^2)) is V22() set
K57((),K59(((cos . ()) ^2))) is set
cot * exp_R is V1() V4( REAL ) V5( REAL ) V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom () is V49() V50() V51() Element of K19(REAL)
Z is open V49() V50() V51() Element of K19(REAL)
() `| 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
sin . () is V22() V23() ext-real Element of REAL
dom () 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
sin . () is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(() `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
sin . () is V22() V23() ext-real Element of REAL
(sin . ()) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ()),(sin . ())) is set
() / ((sin . ()) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . ()) ^2)) is V22() set
K57((),K59(((sin . ()) ^2))) is set
- (() / ((sin . ()) ^2)) is V22() V23() ext-real Element of REAL
diff ((),f) is V22() V23() ext-real Element of REAL
diff (cot,()) is V22() V23() ext-real Element of REAL
diff (exp_R,f) is V22() V23() ext-real Element of REAL
(diff (cot,())) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
1 / ((sin . ()) ^2) is V22() V23() ext-real Element of REAL
K57(1,K59(((sin . ()) ^2))) is set
- (1 / ((sin . ()) ^2)) is V22() V23() ext-real Element of REAL
(- (1 / ((sin . ()) ^2))) * (diff (exp_R,f)) is V22() V23() ext-real Element of REAL
(diff (exp_R,f)) / ((sin . ()) ^2) is V22() V23() ext-real Element of REAL
K57((diff (exp_R,f)),K59(((sin . ()) ^2))) is set
- ((diff (exp_R,f)) / ((sin . ()) ^2)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
(() `| Z) . f is V22() V23() ext-real Element of REAL
exp_R . f is V22() V23() ext-real Element of REAL
sin . () is V22() V23() ext-real Element of REAL
(sin . ()) ^2 is V22() V23() ext-real Element of REAL
K57((sin . ()),(sin . ())) is set
() / ((sin . ()) ^2) is V22() V23() ext-real Element of REAL
K59(((sin . (