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