:: FDIFF_5 semantic presentation

REAL is non empty V49() V50() V51() V55() V62() set
NAT is non empty V15() V16() V17() V49() V50() V51() V52() V53() V54() V55() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V49() V55() V62() set
{} is set
the empty V15() V16() V17() V19() V20() V21() V23() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V60() set is empty V15() V16() V17() V19() V20() V21() V23() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V60() set
1 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V49() V50() V51() V52() V53() V54() V60() V61() Element of NAT
{{},1} is set
K20(REAL,REAL) is V39() V40() V41() set
K19(K20(REAL,REAL)) is set
K20(NAT,REAL) is V39() V40() V41() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V39() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V39() set
K19(K20(COMPLEX,COMPLEX)) is set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
RAT is non empty V49() V50() V51() V52() V55() V62() set
INT is non empty V49() V50() V51() V52() V53() V55() V62() set
NAT is non empty V15() V16() V17() V49() V50() V51() V52() V53() V54() V55() set
K19(NAT) is set
K19(NAT) is set
0 is V15() V16() V17() V21() V22() V23() ext-real non negative V49() V50() V51() V52() V53() V54() V60() V61() Element of NAT
ln is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
exp_R is Relation-like REAL -defined REAL -valued V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
exp_R " is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
K320(REAL,ln) is V49() V50() V51() Element of K19(REAL)
right_open_halfline 0 is V49() V50() V51() Element of K19(REAL)
+infty is non empty ext-real positive non negative set
K138(0,+infty) is set
K321(REAL,ln) is V49() V50() V51() Element of K19(REAL)
{0} is V49() V50() V51() V52() V53() V54() set
sin is Relation-like REAL -defined REAL -valued V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
K320(REAL,sin) is V49() V50() V51() Element of K19(REAL)
cos is Relation-like REAL -defined REAL -valued V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
K320(REAL,cos) is V49() V50() V51() Element of K19(REAL)
2 is non empty V15() V16() V17() V21() V22() V23() ext-real positive non negative V49() V50() V51() V52() V53() V54() V60() V61() Element of NAT
#Z 2 is Relation-like REAL -defined REAL -valued V6() V30( REAL , REAL ) V39() V40() V41() Element of K19(K20(REAL,REAL))
Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x + x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x + x) is set
(x + x) `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
dom x is set
dom x is set
(dom x) /\ (dom x) is set
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
0 * x is V22() V23() ext-real Element of REAL
(0 * x) + Z is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
2 - 1 is V22() V23() ext-real V60() Element of REAL
x is V22() V23() ext-real Element of REAL
(x `| f) . x is V22() V23() ext-real Element of REAL
x #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (x #Z (2 - 1)) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x + x) `| f) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) + (diff (x,x)) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) + (diff (x,x)) is V22() V23() ext-real Element of REAL
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) + ((x `| f) . x) is V22() V23() ext-real Element of REAL
0 + ((x `| f) . x) is V22() V23() ext-real Element of REAL
x #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (x #Z (2 - 1)) is V22() V23() ext-real Element of REAL
x |^ 1 is V22() V23() ext-real Element of REAL
2 * (x |^ 1) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x + x) `| f) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x - x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x - x) is set
(x - x) `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
dom x is set
dom x is set
(dom x) /\ (dom x) is set
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
0 * x is V22() V23() ext-real Element of REAL
(0 * x) + Z is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
2 - 1 is V22() V23() ext-real V60() Element of REAL
x is V22() V23() ext-real Element of REAL
(x `| f) . x is V22() V23() ext-real Element of REAL
x #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (x #Z (2 - 1)) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x - x) `| f) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
- (2 * x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) - (diff (x,x)) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) - (diff (x,x)) is V22() V23() ext-real Element of REAL
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) - ((x `| f) . x) is V22() V23() ext-real Element of REAL
0 - ((x `| f) . x) is V22() V23() ext-real Element of REAL
x #Z (2 - 1) is V22() V23() ext-real Element of REAL
2 * (x #Z (2 - 1)) is V22() V23() ext-real Element of REAL
0 - (2 * (x #Z (2 - 1))) is V22() V23() ext-real Element of REAL
x |^ 1 is V22() V23() ext-real Element of REAL
2 * (x |^ 1) is V22() V23() ext-real Element of REAL
0 - (2 * (x |^ 1)) is V22() V23() ext-real Element of REAL
- (2 * (x |^ 1)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x - x) `| f) . x is V22() V23() ext-real Element of REAL
2 * x is V22() V23() ext-real Element of REAL
- (2 * x) is V22() V23() ext-real Element of REAL
1 / 2 is V22() V23() ext-real Element of REAL
#R (1 / 2) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (#R (1 / 2)) is set
- (1 / 2) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
(#R (1 / 2)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
f is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((#R (1 / 2)) `| Z) . f is V22() V23() ext-real Element of REAL
f #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
(1 / 2) * (f #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
diff ((#R (1 / 2)),f) is V22() V23() ext-real Element of REAL
(1 / 2) - 1 is V22() V23() ext-real Element of REAL
f #R ((1 / 2) - 1) is V22() V23() ext-real Element of REAL
(1 / 2) * (f #R ((1 / 2) - 1)) is V22() V23() ext-real Element of REAL
f is V22() V23() ext-real Element of REAL
((#R (1 / 2)) `| Z) . f is V22() V23() ext-real Element of REAL
f #R (- (1 / 2)) is V22() V23() ext-real Element of REAL
(1 / 2) * (f #R (- (1 / 2))) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
2 * Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x / x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x / x) is set
(x / x) `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom x is set
dom x is set
x " {0} is set
(dom x) \ (x " {0}) is Element of K19((dom x))
K19((dom x)) is set
(dom x) /\ ((dom x) \ (x " {0})) is Element of K19((dom x))
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + Z is V22() V23() ext-real Element of REAL
- 1 is V22() V23() ext-real V60() Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
(- 1) * x is V22() V23() ext-real Element of REAL
((- 1) * x) + Z is V22() V23() ext-real Element of REAL
Z - x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| f) . x is V22() V23() ext-real Element of REAL
Z - x is V22() V23() ext-real Element of REAL
(Z - x) ^2 is V22() V23() ext-real Element of REAL
K57((Z - x),(Z - x)) is set
(2 * Z) / ((Z - x) ^2) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
Z + x is V22() V23() ext-real Element of REAL
diff ((x / x),x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
(x . x) ^2 is V22() V23() ext-real Element of REAL
K57((x . x),(x . x)) is set
(((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| f) . x) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| f) . x) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| f) . x) * (x . x)) - (((x `| f) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| f) . x) * (x . x)) - (((x `| f) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
1 * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - (((x `| f) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - (((x `| f) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
(- 1) * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - ((- 1) * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - ((- 1) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| f) . x is V22() V23() ext-real Element of REAL
Z - x is V22() V23() ext-real Element of REAL
(Z - x) ^2 is V22() V23() ext-real Element of REAL
K57((Z - x),(Z - x)) is set
(2 * Z) / ((Z - x) ^2) is V22() V23() ext-real Element of REAL
Z is V22() V23() ext-real Element of REAL
2 * Z is V22() V23() ext-real Element of REAL
f is open V49() V50() V51() Element of K19(REAL)
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x / x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x / x) is set
(x / x) `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + Z is V22() V23() ext-real Element of REAL
dom x is set
dom x is set
x " {0} is set
(dom x) \ (x " {0}) is Element of K19((dom x))
K19((dom x)) is set
(dom x) /\ ((dom x) \ (x " {0})) is Element of K19((dom x))
- Z 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
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + (- Z) is V22() V23() ext-real Element of REAL
(1 * x) - Z is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| f) . x is V22() V23() ext-real Element of REAL
x + Z is V22() V23() ext-real Element of REAL
(x + Z) ^2 is V22() V23() ext-real Element of REAL
K57((x + Z),(x + Z)) is set
(2 * Z) / ((x + Z) ^2) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x - Z is V22() V23() ext-real Element of REAL
diff ((x / x),x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
(x . x) ^2 is V22() V23() ext-real Element of REAL
K57((x . x),(x . x)) is set
(((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| f) . x) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| f) . x) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| f is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| f) . x is V22() V23() ext-real Element of REAL
((x `| f) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| f) . x) * (x . x)) - (((x `| f) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| f) . x) * (x . x)) - (((x `| f) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
1 * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - (((x `| f) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - (((x `| f) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
1 * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - (1 * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - (1 * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| f) . x is V22() V23() ext-real Element of REAL
x + Z is V22() V23() ext-real Element of REAL
(x + Z) ^2 is V22() V23() ext-real Element of REAL
K57((x + Z),(x + Z)) is set
(2 * Z) / ((x + Z) ^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
Z - f is V22() V23() ext-real Element of REAL
x is open V49() V50() V51() Element of K19(REAL)
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
x / x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (x / x) is set
(x / x) `| x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
- 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
x . x is V22() V23() ext-real Element of REAL
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + (- Z) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
(1 * x) + (- f) is V22() V23() ext-real Element of REAL
(1 * x) - Z is V22() V23() ext-real Element of REAL
(1 * x) - f 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
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + (- Z) is V22() V23() ext-real Element of REAL
dom x is set
dom x is set
x " {0} is set
(dom x) \ (x " {0}) is Element of K19((dom x))
K19((dom x)) is set
(dom x) /\ ((dom x) \ (x " {0})) is Element of K19((dom x))
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
1 * x is V22() V23() ext-real Element of REAL
(1 * x) + (- f) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| x) . x is V22() V23() ext-real Element of REAL
x - f is V22() V23() ext-real Element of REAL
(x - f) ^2 is V22() V23() ext-real Element of REAL
K57((x - f),(x - f)) is set
(Z - f) / ((x - f) ^2) is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x . x is V22() V23() ext-real Element of REAL
x - Z is V22() V23() ext-real Element of REAL
diff ((x / x),x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
diff (x,x) is V22() V23() ext-real Element of REAL
(diff (x,x)) * (x . x) is V22() V23() ext-real Element of REAL
((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
(x . x) ^2 is V22() V23() ext-real Element of REAL
K57((x . x),(x . x)) is set
(((diff (x,x)) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| x) . x is V22() V23() ext-real Element of REAL
((x `| x) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| x) . x) * (x . x)) - ((diff (x,x)) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| x) . x) * (x . x)) - ((diff (x,x)) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x `| x is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(x `| x) . x is V22() V23() ext-real Element of REAL
((x `| x) . x) * (x . x) is V22() V23() ext-real Element of REAL
(((x `| x) . x) * (x . x)) - (((x `| x) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((((x `| x) . x) * (x . x)) - (((x `| x) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
1 * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - (((x `| x) . x) * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - (((x `| x) . x) * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
1 * (x . x) is V22() V23() ext-real Element of REAL
(1 * (x . x)) - (1 * (x . x)) is V22() V23() ext-real Element of REAL
((1 * (x . x)) - (1 * (x . x))) / ((x . x) ^2) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((x / x) `| x) . x is V22() V23() ext-real Element of REAL
x - f is V22() V23() ext-real Element of REAL
(x - f) ^2 is V22() V23() ext-real Element of REAL
K57((x - f),(x - f)) is set
(Z - f) / ((x - f) ^2) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) ^) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (id Z) is set
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
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
(id Z) . x is V22() V23() ext-real Element of REAL
(((id Z) ^) `| Z) . x is V22() V23() ext-real Element of REAL
diff (((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) ^2 is V22() V23() ext-real Element of REAL
K57(((id Z) . x),((id Z) . x)) is set
(diff ((id Z),x)) / (((id Z) . x) ^2) is V22() V23() ext-real Element of REAL
- ((diff ((id Z),x)) / (((id Z) . x) ^2)) is V22() V23() ext-real Element of REAL
(id Z) `| Z is Relation-like REAL -defined REAL -valued 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) ^2) is V22() V23() ext-real Element of REAL
- ((((id Z) `| Z) . x) / (((id Z) . x) ^2)) is V22() V23() ext-real Element of REAL
1 / (((id Z) . x) ^2) is V22() V23() ext-real Element of REAL
- (1 / (((id Z) . x) ^2)) is V22() V23() ext-real Element of REAL
x ^2 is V22() V23() ext-real Element of REAL
K57(x,x) is set
1 / (x ^2) is V22() V23() ext-real Element of REAL
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((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 ^2) is V22() V23() ext-real Element of REAL
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
sin * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin * ((id Z) ^)) is set
rng ((id Z) ^) is V49() V50() V51() set
(id Z) " {0} is set
f is set
dom (id Z) is set
(id Z) . f is V22() V23() ext-real Element of REAL
dom ((id Z) ^) is set
dom (id Z) is set
(dom (id Z)) \ ((id Z) " {0}) is Element of K19((dom (id Z)))
K19((dom (id Z))) is set
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
sin * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(sin * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin * ((id Z) ^)) is set
dom ((id Z) ^) is set
x is set
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
((sin * ((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 ^2) 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
(1 / (x ^2)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
- ((1 / (x ^2)) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
diff ((sin * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (sin,(((id Z) ^) . x)) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
(diff (sin,(((id Z) ^) . x))) * (diff (((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)) * (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) ")) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
((id Z) ^) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) ^) `| Z) . x is V22() V23() ext-real Element of REAL
(cos . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x) is V22() V23() ext-real Element of REAL
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
(cos . (((id Z) . x) ")) * (- (1 / (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
cos . (1 * (x ")) is V22() V23() ext-real Element of REAL
(cos . (1 * (x "))) * (- (1 / (x ^2))) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) * (- (1 / (x ^2))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((sin * ((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 ^2) 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
(1 / (x ^2)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
- ((1 / (x ^2)) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cos * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (cos * ((id Z) ^)) is set
(cos * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) ^) is set
x is set
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
((cos * ((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 ^2) 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
(1 / (x ^2)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((id Z) ^) . x is V22() V23() ext-real Element of REAL
diff (cos,(((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)) is V22() V23() ext-real Element of REAL
diff ((cos * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
diff (((id Z) ^),x) is V22() V23() ext-real Element of REAL
(diff (cos,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
(sin . (((id Z) ^) . x)) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
- ((sin . (((id Z) ^) . x)) * (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
sin . (((id Z) . x) ") is V22() V23() ext-real Element of REAL
(sin . (((id Z) . x) ")) * (diff (((id Z) ^),x)) is V22() V23() ext-real Element of REAL
- ((sin . (((id Z) . x) ")) * (diff (((id Z) ^),x))) is V22() V23() ext-real Element of REAL
((id Z) ^) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(((id Z) ^) `| Z) . x is V22() V23() ext-real Element of REAL
(sin . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x) is V22() V23() ext-real Element of REAL
- ((sin . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x)) is V22() V23() ext-real Element of REAL
- (1 / (x ^2)) is V22() V23() ext-real Element of REAL
(sin . (((id Z) . x) ")) * (- (1 / (x ^2))) is V22() V23() ext-real Element of REAL
- ((sin . (((id Z) . x) ")) * (- (1 / (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 "))) * (- (1 / (x ^2))) is V22() V23() ext-real Element of REAL
- ((sin . (1 * (x "))) * (- (1 / (x ^2)))) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) * (- (1 / (x ^2))) is V22() V23() ext-real Element of REAL
- ((sin . (1 / x)) * (- (1 / (x ^2)))) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) * (1 / (x ^2)) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
((cos * ((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 ^2) 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
(1 / (x ^2)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
sin * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) (sin * ((id Z) ^)) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) (#) (sin * ((id Z) ^))) is set
((id Z) (#) (sin * ((id Z) ^))) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (id Z) is set
dom (sin * ((id Z) ^)) is set
(dom (id Z)) /\ (dom (sin * ((id Z) ^))) is set
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 ((id Z) ^) is set
x is set
x is V22() V23() ext-real Element of REAL
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . x is V22() V23() ext-real Element of REAL
(sin * ((id Z) ^)) . x is V22() V23() ext-real Element of REAL
diff ((id Z),x) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . 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 ((sin * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
((id Z) . x) * (diff ((sin * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
(((sin * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(id Z) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) `| Z) . x is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) * (((id Z) `| Z) . x) is V22() V23() ext-real Element of REAL
(((sin * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) * 1 is V22() V23() ext-real Element of REAL
(((sin * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
x * (diff ((sin * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) + (x * (diff ((sin * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(sin * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
x * (((sin * ((id Z) ^)) `| Z) . x) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) + (x * (((sin * ((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 ^2) 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
(1 / (x ^2)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
- ((1 / (x ^2)) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
x * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) + (x * (- ((1 / (x ^2)) * (cos . (1 / x))))) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
1 / (x * x) is V22() V23() ext-real Element of REAL
x * (1 / (x * x)) is V22() V23() ext-real Element of REAL
(x * (1 / (x * x))) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) - ((x * (1 / (x * x))) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
(1 / x) * (1 / x) is V22() V23() ext-real Element of REAL
x * ((1 / x) * (1 / x)) is V22() V23() ext-real Element of REAL
(x * ((1 / x) * (1 / x))) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) - ((x * ((1 / x) * (1 / x))) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
x * (1 / x) is V22() V23() ext-real Element of REAL
(x * (1 / x)) * (1 / x) is V22() V23() ext-real Element of REAL
((x * (1 / x)) * (1 / x)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) - (((x * (1 / x)) * (1 / x)) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
1 * (1 / x) is V22() V23() ext-real Element of REAL
(1 * (1 / x)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) - ((1 * (1 / x)) * (cos . (1 / 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
(1 / x) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
(sin . (((id Z) ^) . x)) - ((1 / x) * (cos . (1 / 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) ")) - ((1 / x) * (cos . (1 / x))) 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 "))) - ((1 / x) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
sin . (1 / x) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((id Z) (#) (sin * ((id Z) ^))) `| Z) . 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
cos . (1 / x) is V22() V23() ext-real Element of REAL
(1 / x) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
(sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cos * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) (#) (cos * ((id Z) ^)) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((id Z) (#) (cos * ((id Z) ^))) is set
((id Z) (#) (cos * ((id Z) ^))) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (id Z) is set
dom (cos * ((id Z) ^)) is set
(dom (id Z)) /\ (dom (cos * ((id Z) ^))) is set
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 ((id Z) ^) is set
x is set
x is V22() V23() ext-real Element of REAL
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . x is V22() V23() ext-real Element of REAL
(cos * ((id Z) ^)) . x is V22() V23() ext-real Element of REAL
diff ((id Z),x) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . 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 ((cos * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
((id Z) . x) * (diff ((cos * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(id Z) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((id Z) `| Z) . x is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) * (((id Z) `| Z) . x) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) * 1 is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
x * (diff ((cos * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + (x * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(cos * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((cos * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
x * (((cos * ((id Z) ^)) `| Z) . x) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + (x * (((cos * ((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 ^2) 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
(1 / (x ^2)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
x * ((1 / (x ^2)) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + (x * ((1 / (x ^2)) * (sin . (1 / x)))) is V22() V23() ext-real Element of REAL
x * x is V22() V23() ext-real Element of REAL
1 / (x * x) is V22() V23() ext-real Element of REAL
x * (1 / (x * x)) is V22() V23() ext-real Element of REAL
(x * (1 / (x * x))) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + ((x * (1 / (x * x))) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
(1 / x) * (1 / x) is V22() V23() ext-real Element of REAL
x * ((1 / x) * (1 / x)) is V22() V23() ext-real Element of REAL
(x * ((1 / x) * (1 / x))) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + ((x * ((1 / x) * (1 / x))) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
x * (1 / x) is V22() V23() ext-real Element of REAL
(x * (1 / x)) * (1 / x) is V22() V23() ext-real Element of REAL
((x * (1 / x)) * (1 / x)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + (((x * (1 / x)) * (1 / x)) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
1 * (1 / x) is V22() V23() ext-real Element of REAL
(1 * (1 / x)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) + ((1 * (1 / x)) * (sin . (1 / 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
(1 / x) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
(cos . (((id Z) ^) . x)) + ((1 / x) * (sin . (1 / 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) ")) + ((1 / x) * (sin . (1 / x))) 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
cos . (1 * (x ")) is V22() V23() ext-real Element of REAL
(cos . (1 * (x "))) + ((1 / x) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
cos . (1 / x) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
x is V22() V23() ext-real Element of REAL
(((id Z) (#) (cos * ((id Z) ^))) `| Z) . 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
sin . (1 / x) is V22() V23() ext-real Element of REAL
(1 / x) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
Z is open V49() V50() V51() Element of K19(REAL)
id Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(id Z) ^ is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
sin * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
cos * ((id Z) ^) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
(sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) is set
((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
dom (sin * ((id Z) ^)) is set
dom (cos * ((id Z) ^)) is set
(dom (sin * ((id Z) ^))) /\ (dom (cos * ((id Z) ^))) is set
dom ((id Z) ^) is set
x is set
x is V22() V23() ext-real Element of REAL
(((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x is V22() V23() ext-real Element of REAL
(cos * ((id Z) ^)) . x is V22() V23() ext-real Element of REAL
diff ((sin * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) * (diff ((sin * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
(sin * ((id Z) ^)) . x is V22() V23() ext-real Element of REAL
diff ((cos * ((id Z) ^)),x) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x)) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (diff ((sin * ((id Z) ^)),x))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(sin * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((sin * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) * (((sin * ((id Z) ^)) `| Z) . x) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (((sin * ((id Z) ^)) `| Z) . x)) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id 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 ^2) 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
(1 / (x ^2)) * (cos . (1 / x)) is V22() V23() ext-real Element of REAL
- ((1 / (x ^2)) * (cos . (1 / x))) is V22() V23() ext-real Element of REAL
((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) is V22() V23() ext-real Element of REAL
(cos * ((id Z) ^)) `| Z is Relation-like REAL -defined REAL -valued V6() V39() V40() V41() Element of K19(K20(REAL,REAL))
((cos * ((id Z) ^)) `| Z) . x is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) * (((cos * ((id Z) ^)) `| Z) . x) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (((cos * ((id Z) ^)) `| Z) . x)) is V22() V23() ext-real Element of REAL
sin . (1 / x) is V22() V23() ext-real Element of REAL
(1 / (x ^2)) * (sin . (1 / x)) is V22() V23() ext-real Element of REAL
((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
(((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / 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)) * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
((cos . (((id Z) ^) . x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / 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) ")) * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
((cos . (((id Z) . x) ")) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) 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
cos . (1 * (x ")) is V22() V23() ext-real Element of REAL
(cos . (1 * (x "))) * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
((cos . (1 * (x "))) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) is V22() V23() ext-real Element of REAL
(cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x)))) is V22() V23() ext-real Element of REAL
((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / 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)) * ((1 / (x ^2)) * (sin . (1 / x))) is V22() V23() ext-real Element of REAL
((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (((id Z) ^) . x)) * ((1 / (x ^2)) * (sin . (1 / x)))) is V22() V23() ext-real Element of REAL
sin . (((id Z) . x) ") is V22() V23() ext-real Element of REAL
(sin . (((id Z