:: TAYLOR_2 semantic presentation

REAL is V1() V63() V75() V76() V77() V81() set
NAT is V75() V76() V77() V78() V79() V80() V81() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V63() V75() V81() set
K7(REAL,REAL) is V33() V34() V35() set
K6(K7(REAL,REAL)) is set
omega is V75() V76() V77() V78() V79() V80() V81() set
K6(omega) is set
K6(NAT) is set
RAT is V1() V63() V75() V76() V77() V78() V81() set
INT is V1() V63() V75() V76() V77() V78() V79() V81() set
K7(NAT,REAL) is V33() V34() V35() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V33() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V33() set
K6(K7(COMPLEX,COMPLEX)) is set
PFuncs (REAL,REAL) is set
K7(NAT,(PFuncs (REAL,REAL))) is set
K6(K7(NAT,(PFuncs (REAL,REAL)))) is set
1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
sin is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
cos is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
K394(REAL,sin) is V75() V76() V77() Element of K6(REAL)
K394(REAL,cos) is V75() V76() V77() Element of K6(REAL)
K158() is V11() Element of COMPLEX
cos . 0 is V11() real ext-real Element of REAL
sin . 0 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive Element of REAL
2 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
exp_R is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
K394(REAL,exp_R) is V75() V76() V77() Element of K6(REAL)
[#] REAL is V75() V76() V77() Element of K6(REAL)
K395(REAL,exp_R) is V75() V76() V77() Element of K6(REAL)
K147(0) is V75() V76() V77() Element of K6(REAL)
exp_R . 0 is V11() real ext-real Element of REAL
0 is V1() V75() V76() V77() V78() V79() V80() V81() set
r is V11() real ext-real Element of REAL
abs r is V11() real ext-real Element of REAL
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r |^ x is V11() real ext-real Element of REAL
abs (r |^ x) is V11() real ext-real Element of REAL
(abs r) |^ x is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r |^ g is V11() real ext-real Element of REAL
abs (r |^ g) is V11() real ext-real Element of REAL
(abs r) |^ g is V11() real ext-real Element of REAL
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r |^ (g + 1) is V11() real ext-real Element of REAL
abs (r |^ (g + 1)) is V11() real ext-real Element of REAL
(abs r) |^ (g + 1) is V11() real ext-real Element of REAL
r * (r |^ g) is V11() real ext-real Element of REAL
abs (r * (r |^ g)) is V11() real ext-real Element of REAL
(abs r) * (abs (r |^ g)) is V11() real ext-real Element of REAL
r |^ 0 is V11() real ext-real Element of REAL
abs (r |^ 0) is V11() real ext-real Element of REAL
abs 1 is V11() real ext-real V74() Element of REAL
(abs r) |^ 0 is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
x is V75() V76() V77() Element of K6(REAL)
g is V11() real ext-real set
Taylor (r,x,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(r + 1) ! is V11() real ext-real Element of REAL
x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom x is set
g is V11() real ext-real Element of REAL
- g is V11() real ext-real Element of REAL
].(- g),g.[ is open V75() V76() V77() Element of K6(REAL)
diff (x,].(- g),g.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (x,].(- g),g.[)) . (r + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
x . g is V11() real ext-real Element of REAL
(x,].(- g),g.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (x,].(- g),g.[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x,].(- g),g.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (x,].(- g),g.[,g)) . r is V11() real ext-real Element of REAL
g |^ (r + 1) is V11() real ext-real Element of REAL
0 - g is V11() real ext-real Element of REAL
0 + g is V11() real ext-real Element of REAL
].(0 - g),(0 + g).[ is open V75() V76() V77() Element of K6(REAL)
Taylor (x,].(0 - g),(0 + g).[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (Taylor (x,].(0 - g),(0 + g).[,0,g)) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (Taylor (x,].(0 - g),(0 + g).[,0,g))) . r is V11() real ext-real Element of REAL
diff (x,].(0 - g),(0 + g).[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (x,].(0 - g),(0 + g).[)) . (r + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g - 0 is V11() real ext-real Element of REAL
(g - 0) |^ (r + 1) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p * (g - 0) is V11() real ext-real Element of REAL
0 + (p * (g - 0)) is V11() real ext-real Element of REAL
((diff (x,].(0 - g),(0 + g).[)) . (r + 1)) . (0 + (p * (g - 0))) is V11() real ext-real Element of REAL
(((diff (x,].(0 - g),(0 + g).[)) . (r + 1)) . (0 + (p * (g - 0)))) * ((g - 0) |^ (r + 1)) is V11() real ext-real Element of REAL
((((diff (x,].(0 - g),(0 + g).[)) . (r + 1)) . (0 + (p * (g - 0)))) * ((g - 0) |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
((Partial_Sums (Taylor (x,].(0 - g),(0 + g).[,0,g))) . r) + (((((diff (x,].(0 - g),(0 + g).[)) . (r + 1)) . (0 + (p * (g - 0)))) * ((g - 0) |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
p * g is V11() real ext-real Element of REAL
((diff (x,].(- g),g.[)) . (r + 1)) . (p * g) is V11() real ext-real Element of REAL
(((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1)) is V11() real ext-real Element of REAL
((((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
((Partial_Sums (x,].(- g),g.[,g)) . r) + (((((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(r + 1) ! is V11() real ext-real Element of REAL
x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom x is set
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
g - g is V11() real ext-real Element of REAL
g + g is V11() real ext-real Element of REAL
].(g - g),(g + g).[ is open V75() V76() V77() Element of K6(REAL)
diff (x,].(g - g),(g + g).[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (x,].(g - g),(g + g).[)) . (r + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
x . p is V11() real ext-real Element of REAL
Taylor (x,].(g - g),(g + g).[,g,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (Taylor (x,].(g - g),(g + g).[,g,p)) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (Taylor (x,].(g - g),(g + g).[,g,p))) . r is V11() real ext-real Element of REAL
(x . p) - ((Partial_Sums (Taylor (x,].(g - g),(g + g).[,g,p))) . r) is V11() real ext-real Element of REAL
abs ((x . p) - ((Partial_Sums (Taylor (x,].(g - g),(g + g).[,g,p))) . r)) is V11() real ext-real Element of REAL
p - g is V11() real ext-real Element of REAL
(p - g) |^ (r + 1) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n * (p - g) is V11() real ext-real Element of REAL
g + (n * (p - g)) is V11() real ext-real Element of REAL
((diff (x,].(g - g),(g + g).[)) . (r + 1)) . (g + (n * (p - g))) is V11() real ext-real Element of REAL
(((diff (x,].(g - g),(g + g).[)) . (r + 1)) . (g + (n * (p - g)))) * ((p - g) |^ (r + 1)) is V11() real ext-real Element of REAL
((((diff (x,].(g - g),(g + g).[)) . (r + 1)) . (g + (n * (p - g)))) * ((p - g) |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
((Partial_Sums (Taylor (x,].(g - g),(g + g).[,g,p))) . r) + (((((diff (x,].(g - g),(g + g).[)) . (r + 1)) . (g + (n * (p - g)))) * ((p - g) |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(r + 1) ! is V11() real ext-real Element of REAL
x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom x is set
g is V11() real ext-real Element of REAL
- g is V11() real ext-real Element of REAL
].(- g),g.[ is open V75() V76() V77() Element of K6(REAL)
diff (x,].(- g),g.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (x,].(- g),g.[)) . (r + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
x . g is V11() real ext-real Element of REAL
(x,].(- g),g.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (x,].(- g),g.[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x,].(- g),g.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (x,].(- g),g.[,g)) . r is V11() real ext-real Element of REAL
(x . g) - ((Partial_Sums (x,].(- g),g.[,g)) . r) is V11() real ext-real Element of REAL
abs ((x . g) - ((Partial_Sums (x,].(- g),g.[,g)) . r)) is V11() real ext-real Element of REAL
g |^ (r + 1) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p * g is V11() real ext-real Element of REAL
((diff (x,].(- g),g.[)) . (r + 1)) . (p * g) is V11() real ext-real Element of REAL
(((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1)) is V11() real ext-real Element of REAL
((((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
((Partial_Sums (x,].(- g),g.[,g)) . r) + (((((diff (x,].(- g),g.[)) . (r + 1)) . (p * g)) * (g |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
r is open V75() V76() V77() Element of K6(REAL)
x is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
x | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (x | r) is set
dom x is set
(dom x) /\ r is V75() V76() V77() Element of K6(REAL)
r is open V75() V76() V77() Element of K6(REAL)
exp_R `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
exp_R | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | r) is set
x is V11() real ext-real Element of REAL
(exp_R `| r) . x is V11() real ext-real Element of REAL
(exp_R | r) . x is V11() real ext-real Element of REAL
diff (exp_R,x) is V11() real ext-real Element of REAL
exp_R . x is V11() real ext-real Element of REAL
dom (exp_R `| r) is set
r is open V75() V76() V77() Element of K6(REAL)
diff (exp_R,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
exp_R | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,r)) . x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,r)) . (g + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,r)) . g) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
exp_R `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (exp_R,r)) . 0 is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
r is open V75() V76() V77() Element of K6(REAL)
diff (exp_R,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,r)) . x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
((diff (exp_R,r)) . x) . g is V11() real ext-real Element of REAL
exp_R . g is V11() real ext-real Element of REAL
exp_R | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | r) is set
(exp_R | r) . g is V11() real ext-real Element of REAL
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r ! is V11() real ext-real Element of REAL
0 - 0 is V1() V11() real ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() Element of REAL
abs (0 - 0) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
].(- x),x.[ is open V75() V76() V77() Element of K6(REAL)
g is V11() real ext-real Element of REAL
(exp_R,].(- x),x.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (exp_R,].(- x),x.[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(exp_R,].(- x),x.[,g) . r is V11() real ext-real Element of REAL
g |^ r is V11() real ext-real Element of REAL
(g |^ r) / (r !) is V11() real ext-real Element of REAL
0 - x is V11() real ext-real Element of REAL
0 + x is V11() real ext-real Element of REAL
].(0 - x),(0 + x).[ is open V75() V76() V77() Element of K6(REAL)
exp_R | ].(- x),x.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | ].(- x),x.[) is set
diff (exp_R,].(- x),x.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (exp_R,].(- x),x.[)) . r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,].(- x),x.[)) . r) . 0 is V11() real ext-real Element of REAL
g - 0 is V11() real ext-real Element of REAL
(g - 0) |^ r is V11() real ext-real Element of REAL
(((diff (exp_R,].(- x),x.[)) . r) . 0) * ((g - 0) |^ r) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- x),x.[)) . r) . 0) * ((g - 0) |^ r)) / (r !) is V11() real ext-real Element of REAL
(exp_R | ].(- x),x.[) . 0 is V11() real ext-real Element of REAL
((exp_R | ].(- x),x.[) . 0) * (g |^ r) is V11() real ext-real Element of REAL
(((exp_R | ].(- x),x.[) . 0) * (g |^ r)) / (r !) is V11() real ext-real Element of REAL
(exp_R . 0) * (g |^ r) is V11() real ext-real Element of REAL
((exp_R . 0) * (g |^ r)) / (r !) is V11() real ext-real Element of REAL
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
r + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(r + 1) ! is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
].(- x),x.[ is open V75() V76() V77() Element of K6(REAL)
g is V11() real ext-real Element of REAL
diff (exp_R,].(- x),x.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (exp_R,].(- x),x.[)) . (r + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g * g is V11() real ext-real Element of REAL
((diff (exp_R,].(- x),x.[)) . (r + 1)) . (g * g) is V11() real ext-real Element of REAL
g |^ (r + 1) is V11() real ext-real Element of REAL
(((diff (exp_R,].(- x),x.[)) . (r + 1)) . (g * g)) * (g |^ (r + 1)) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- x),x.[)) . (r + 1)) . (g * g)) * (g |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- x),x.[)) . (r + 1)) . (g * g)) * (g |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
exp_R . (g * g) is V11() real ext-real Element of REAL
abs (exp_R . (g * g)) is V11() real ext-real Element of REAL
abs g is V11() real ext-real Element of REAL
(abs g) |^ (r + 1) is V11() real ext-real Element of REAL
(abs (exp_R . (g * g))) * ((abs g) |^ (r + 1)) is V11() real ext-real Element of REAL
((abs (exp_R . (g * g))) * ((abs g) |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
(g * g) - 0 is V11() real ext-real Element of REAL
abs ((g * g) - 0) is V11() real ext-real Element of REAL
abs g is V11() real ext-real Element of REAL
(abs g) * (abs g) is V11() real ext-real Element of REAL
g * (abs g) is V11() real ext-real Element of REAL
0 - x is V11() real ext-real Element of REAL
0 + x is V11() real ext-real Element of REAL
].(0 - x),(0 + x).[ is open V75() V76() V77() Element of K6(REAL)
g - 0 is V11() real ext-real Element of REAL
abs (g - 0) is V11() real ext-real Element of REAL
x * 1 is V11() real ext-real Element of REAL
(abs g) * g is V11() real ext-real Element of REAL
exp_R | ].(- x),x.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | ].(- x),x.[) is set
abs ((r + 1) !) is V11() real ext-real Element of REAL
(exp_R | ].(- x),x.[) . (g * g) is V11() real ext-real Element of REAL
((exp_R | ].(- x),x.[) . (g * g)) * (g |^ (r + 1)) is V11() real ext-real Element of REAL
(((exp_R | ].(- x),x.[) . (g * g)) * (g |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
abs ((((exp_R | ].(- x),x.[) . (g * g)) * (g |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
(exp_R . (g * g)) * (g |^ (r + 1)) is V11() real ext-real Element of REAL
((exp_R . (g * g)) * (g |^ (r + 1))) / ((r + 1) !) is V11() real ext-real Element of REAL
abs (((exp_R . (g * g)) * (g |^ (r + 1))) / ((r + 1) !)) is V11() real ext-real Element of REAL
abs ((exp_R . (g * g)) * (g |^ (r + 1))) is V11() real ext-real Element of REAL
(abs ((exp_R . (g * g)) * (g |^ (r + 1)))) / (abs ((r + 1) !)) is V11() real ext-real Element of REAL
abs (g |^ (r + 1)) is V11() real ext-real Element of REAL
(abs (exp_R . (g * g))) * (abs (g |^ (r + 1))) is V11() real ext-real Element of REAL
((abs (exp_R . (g * g))) * (abs (g |^ (r + 1)))) / ((r + 1) !) is V11() real ext-real Element of REAL
r is open V75() V76() V77() Element of K6(REAL)
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
x - 1 is V11() real ext-real Element of REAL
diff (exp_R,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (exp_R,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,r)) . g) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
exp_R | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(exp_R | r) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p is V11() real ext-real Element of REAL
dom ((diff (exp_R,r)) . g) is set
exp_R | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | r) is set
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (exp_R,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
exp_R . r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p |^ n1 is V11() real ext-real Element of REAL
n |^ n1 is V11() real ext-real Element of REAL
n1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p |^ (n1 + 1) is V11() real ext-real Element of REAL
n |^ (n1 + 1) is V11() real ext-real Element of REAL
0 * p is V11() real ext-real Element of REAL
(p |^ n1) * p is V11() real ext-real Element of REAL
(n |^ n1) * n is V11() real ext-real Element of REAL
n |^ 0 is V11() real ext-real Element of REAL
p |^ 0 is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p |^ n1 is V11() real ext-real Element of REAL
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p |^ m1 is V11() real ext-real Element of REAL
n |^ m1 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
0 - r is V11() real ext-real Element of REAL
0 + r is V11() real ext-real Element of REAL
].(0 - r),(0 + r).[ is open V75() V76() V77() Element of K6(REAL)
p - 0 is V11() real ext-real Element of REAL
abs (p - 0) is V11() real ext-real Element of REAL
abs p is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(abs p) |^ g is V11() real ext-real Element of REAL
g |^ g is V11() real ext-real Element of REAL
g ! is V11() real ext-real Element of REAL
1 * r is V11() real ext-real Element of REAL
n * (abs p) is V11() real ext-real Element of REAL
abs n is V11() real ext-real Element of REAL
(abs n) * (abs p) is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
(n * p) - 0 is V11() real ext-real Element of REAL
abs ((n * p) - 0) is V11() real ext-real Element of REAL
(diff (exp_R,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
p |^ g is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
exp_R . (n * p) is V11() real ext-real Element of REAL
(exp_R . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((exp_R . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((exp_R . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
(p |^ g) / (g !) is V11() real ext-real Element of REAL
(exp_R . (n * p)) * ((p |^ g) / (g !)) is V11() real ext-real Element of REAL
abs ((exp_R . (n * p)) * ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
abs (exp_R . (n * p)) is V11() real ext-real Element of REAL
abs ((p |^ g) / (g !)) is V11() real ext-real Element of REAL
(abs (exp_R . (n * p))) * (abs ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
dom exp_R is set
([#] REAL) /\ (dom exp_R) is V75() V76() V77() Element of K6(REAL)
n1 is V11() real ext-real Element of REAL
diff (exp_R,n1) is V11() real ext-real Element of REAL
exp_R | ([#] REAL) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
abs (p |^ g) is V11() real ext-real Element of REAL
abs (g !) is V11() real ext-real Element of REAL
(abs (p |^ g)) / (abs (g !)) is V11() real ext-real Element of REAL
(abs (p |^ g)) / (g !) is V11() real ext-real Element of REAL
((abs p) |^ g) / (g !) is V11() real ext-real Element of REAL
(g |^ g) / (g !) is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - r & not r <= b₁ ) } is set
n1 is V11() real ext-real Element of REAL
x * ((g |^ g) / (g !)) is V11() real ext-real Element of REAL
x * (g |^ g) is V11() real ext-real Element of REAL
(x * (g |^ g)) / (g !) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
((diff (exp_R,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
p |^ g is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n * p is V11() real ext-real Element of REAL
((diff (exp_R,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
p |^ g is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
g ! is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
g |^ g is V11() real ext-real Element of REAL
x * (g |^ g) is V11() real ext-real Element of REAL
(x * (g |^ g)) / (g !) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
x rExpSeq is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
r (#) (x rExpSeq) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
lim (x rExpSeq) is V11() real ext-real Element of REAL
lim (r (#) (x rExpSeq)) is V11() real ext-real Element of REAL
r * 0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
x |^ p is V11() real ext-real Element of REAL
p ! is V11() real ext-real Element of REAL
(x |^ p) / (p !) is V11() real ext-real Element of REAL
r * ((x |^ p) / (p !)) is V11() real ext-real Element of REAL
(r (#) (x rExpSeq)) . p is V11() real ext-real Element of REAL
(x rExpSeq) . p is V11() real ext-real Element of REAL
r * ((x rExpSeq) . p) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
x |^ p is V11() real ext-real Element of REAL
p ! is V11() real ext-real Element of REAL
(r (#) (x rExpSeq)) . p is V11() real ext-real Element of REAL
((r (#) (x rExpSeq)) . p) - 0 is V11() real ext-real Element of REAL
abs (((r (#) (x rExpSeq)) . p) - 0) is V11() real ext-real Element of REAL
(x |^ p) / (p !) is V11() real ext-real Element of REAL
r * ((x |^ p) / (p !)) is V11() real ext-real Element of REAL
abs (r * ((x |^ p) / (p !))) is V11() real ext-real Element of REAL
abs r is V11() real ext-real Element of REAL
abs ((x |^ p) / (p !)) is V11() real ext-real Element of REAL
(abs r) * (abs ((x |^ p) / (p !))) is V11() real ext-real Element of REAL
r * (abs ((x |^ p) / (p !))) is V11() real ext-real Element of REAL
r * (x |^ p) is V11() real ext-real Element of REAL
(r * (x |^ p)) / (p !) is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
x |^ p is V11() real ext-real Element of REAL
r * (x |^ p) is V11() real ext-real Element of REAL
p ! is V11() real ext-real Element of REAL
(r * (x |^ p)) / (p !) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (exp_R,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
n is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,].(- r),r.[)) . n is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n ! is V11() real ext-real Element of REAL
g |^ n is V11() real ext-real Element of REAL
g * (g |^ n) is V11() real ext-real Element of REAL
(g * (g |^ n)) / (n !) is V11() real ext-real Element of REAL
n1 is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 * n1 is V11() real ext-real Element of REAL
((diff (exp_R,].(- r),r.[)) . n) . (m1 * n1) is V11() real ext-real Element of REAL
n1 |^ n is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (exp_R,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p is V11() real ext-real Element of REAL
exp_R . p is V11() real ext-real Element of REAL
(exp_R,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (exp_R,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (exp_R,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (exp_R,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(exp_R . p) - ((Partial_Sums (exp_R,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((exp_R . p) - ((Partial_Sums (exp_R,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
(diff (exp_R,].(- r),r.[)) . (g + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p |^ (g + 1) is V11() real ext-real Element of REAL
(g + 1) ! is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
((diff (exp_R,].(- r),r.[)) . (g + 1)) . (n * p) is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1)) is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !) is V11() real ext-real Element of REAL
abs (((((diff (exp_R,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !)) is V11() real ext-real Element of REAL
p is V11() real ext-real set
exp_R . p is V11() real ext-real Element of REAL
(exp_R,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (exp_R,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (exp_R,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (exp_R,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(exp_R . p) - ((Partial_Sums (exp_R,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((exp_R . p) - ((Partial_Sums (exp_R,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
r rExpSeq is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
abs r is V11() real ext-real Element of REAL
(abs r) rExpSeq is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(r rExpSeq) . x is V11() real ext-real Element of REAL
abs ((r rExpSeq) . x) is V11() real ext-real Element of REAL
((abs r) rExpSeq) . x is V11() real ext-real Element of REAL
x ! is V11() real ext-real Element of REAL
r |^ x is V11() real ext-real Element of REAL
(r |^ x) / (x !) is V11() real ext-real Element of REAL
abs ((r |^ x) / (x !)) is V11() real ext-real Element of REAL
abs (r |^ x) is V11() real ext-real Element of REAL
abs (x !) is V11() real ext-real Element of REAL
(abs (r |^ x)) / (abs (x !)) is V11() real ext-real Element of REAL
(abs (r |^ x)) / (x !) is V11() real ext-real Element of REAL
(abs r) |^ x is V11() real ext-real Element of REAL
((abs r) |^ x) / (x !) is V11() real ext-real Element of REAL
abs (r rExpSeq) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
0 - 0 is V1() V11() real ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() Element of REAL
abs (0 - 0) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(exp_R,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (exp_R,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x rExpSeq is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
exp_R . x is V11() real ext-real Element of REAL
Sum (exp_R,].(- r),r.[,x) is V11() real ext-real Element of REAL
0 - r is V11() real ext-real Element of REAL
0 + r is V11() real ext-real Element of REAL
].(0 - r),(0 + r).[ is open V75() V76() V77() Element of K6(REAL)
exp_R | ].(- r),r.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (exp_R | ].(- r),r.[) is set
g is set
(exp_R,].(- r),r.[,x) . g is V11() real ext-real Element of REAL
diff (exp_R,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (exp_R,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (exp_R,].(- r),r.[)) . g) . 0 is V11() real ext-real Element of REAL
x - 0 is V11() real ext-real Element of REAL
(x - 0) |^ g is V11() real ext-real Element of REAL
(((diff (exp_R,].(- r),r.[)) . g) . 0) * ((x - 0) |^ g) is V11() real ext-real Element of REAL
g ! is V11() real ext-real Element of REAL
((((diff (exp_R,].(- r),r.[)) . g) . 0) * ((x - 0) |^ g)) / (g !) is V11() real ext-real Element of REAL
(exp_R | ].(- r),r.[) . 0 is V11() real ext-real Element of REAL
x |^ g is V11() real ext-real Element of REAL
((exp_R | ].(- r),r.[) . 0) * (x |^ g) is V11() real ext-real Element of REAL
(((exp_R | ].(- r),r.[) . 0) * (x |^ g)) / (g !) is V11() real ext-real Element of REAL
(exp_R . 0) * (x |^ g) is V11() real ext-real Element of REAL
((exp_R . 0) * (x |^ g)) / (g !) is V11() real ext-real Element of REAL
(x rExpSeq) . g is V11() real ext-real Element of REAL
- sin is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
K43(1) is V11() real ext-real non positive set
K43(1) (#) sin is Relation-like REAL -defined V21() total V33() V34() V35() set
r is open V75() V76() V77() Element of K6(REAL)
sin `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
cos `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- sin) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (sin | r) is set
dom (cos | r) is set
dom sin is set
(dom sin) /\ r is V75() V76() V77() Element of K6(REAL)
dom cos is set
(dom cos) /\ r is V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(sin `| r) . x is V11() real ext-real Element of REAL
(cos | r) . x is V11() real ext-real Element of REAL
diff (sin,x) is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
dom (cos `| r) is set
dom ((- sin) | r) is set
(- 1) (#) sin is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((- 1) (#) sin) is set
(dom ((- 1) (#) sin)) /\ r is V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(cos `| r) . x is V11() real ext-real Element of REAL
((- sin) | r) . x is V11() real ext-real Element of REAL
diff (cos,x) is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
- (sin . x) is V11() real ext-real Element of REAL
(- 1) * (sin . x) is V11() real ext-real Element of REAL
(- sin) . x is V11() real ext-real Element of REAL
dom (sin `| r) is set
r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
- r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
K43(1) (#) r is Relation-like REAL -defined V21() V33() V34() V35() set
x is V75() V76() V77() Element of K6(REAL)
(- r) `| x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
r `| x is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
- (r `| x) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
K43(1) (#) (r `| x) is Relation-like REAL -defined V21() V33() V34() V35() set
(- 1) (#) (r `| x) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
r is open V75() V76() V77() Element of K6(REAL)
diff (sin,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
diff (cos,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . (2 * x) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ x is V11() real ext-real Element of REAL
((- 1) |^ x) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(2 * x) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . ((2 * x) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ x) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . (2 * x) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . ((2 * x) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
x + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (x + 1) is V11() real ext-real Element of REAL
((- 1) |^ (x + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . (2 * g) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ g is V11() real ext-real Element of REAL
((- 1) |^ g) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . ((2 * g) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . (2 * g) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . ((2 * g) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (g + 1) is V11() real ext-real Element of REAL
((- 1) |^ (g + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
2 * (g + 1) is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . (2 * (g + 1)) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(2 * (g + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . ((2 * (g + 1)) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . (2 * (g + 1)) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . ((2 * (g + 1)) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(g + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ ((g + 1) + 1) is V11() real ext-real Element of REAL
((- 1) |^ ((g + 1) + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((2 * g) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,r)) . (((2 * g) + 1) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,r)) . ((2 * g) + 1)) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(cos | r) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) (#) ((cos | r) `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
cos `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) (#) (cos `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) (#) sin is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) (#) sin) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) (#) (((- 1) (#) sin) | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) (#) ((- 1) (#) (sin | r)) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ g) * (- 1) is V11() real ext-real Element of REAL
(((- 1) |^ g) * (- 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . (((2 * g) + 1) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,r)) . ((2 * g) + 1)) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(sin | r) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) ((sin | r) `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
sin `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) (sin `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,r)) . (2 * (g + 1))) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) ((cos | r) `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) (cos `| r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) (((- 1) (#) sin) | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) (#) ((- 1) (#) (sin | r)) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ (g + 1)) * (- 1) is V11() real ext-real Element of REAL
(((- 1) |^ (g + 1)) * (- 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,r)) . (2 * (g + 1))) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * 0) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (cos,r)) . ((2 * 0) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . 0 is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,r)) . 0) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(cos | r) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
cos `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- sin) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
1 (#) ((- sin) | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) (#) sin is V1() Relation-like REAL -defined REAL -valued V21() total V30( REAL , REAL ) V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) (#) sin) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ 0 is V11() real ext-real Element of REAL
((- 1) |^ 0) (#) (((- 1) (#) sin) | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ 0) (#) ((- 1) (#) (sin | r)) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ 0) * (- 1) is V11() real ext-real Element of REAL
(((- 1) |^ 0) * (- 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (0 + 1) is V11() real ext-real Element of REAL
((- 1) |^ (0 + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (sin,r)) . (2 * 0) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
1 (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ 0) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (cos,r)) . (2 * 0) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
1 (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ 0) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (sin,r)) . ((2 * 0) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(diff (sin,r)) . 0 is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,r)) . 0) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(sin | r) `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
sin `| r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
0 - 0 is V1() V11() real ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() Element of REAL
abs (0 - 0) is V11() real ext-real Element of REAL
r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * r is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * r) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ r is V11() real ext-real Element of REAL
((2 * r) + 1) ! is V11() real ext-real Element of REAL
(2 * r) ! is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
].(- x),x.[ is open V75() V76() V77() Element of K6(REAL)
g is V11() real ext-real Element of REAL
(sin,].(- x),x.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- x),x.[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(sin,].(- x),x.[,g) . (2 * r) is V11() real ext-real Element of REAL
(sin,].(- x),x.[,g) . ((2 * r) + 1) is V11() real ext-real Element of REAL
g |^ ((2 * r) + 1) is V11() real ext-real Element of REAL
((- 1) |^ r) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
(((- 1) |^ r) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(cos,].(- x),x.[,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- x),x.[,0,g) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(cos,].(- x),x.[,g) . (2 * r) is V11() real ext-real Element of REAL
g |^ (2 * r) is V11() real ext-real Element of REAL
((- 1) |^ r) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
(((- 1) |^ r) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
(cos,].(- x),x.[,g) . ((2 * r) + 1) is V11() real ext-real Element of REAL
0 - x is V11() real ext-real Element of REAL
0 + x is V11() real ext-real Element of REAL
].(0 - x),(0 + x).[ is open V75() V76() V77() Element of K6(REAL)
cos | ].(- x),x.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (cos | ].(- x),x.[) is set
((- 1) |^ r) (#) (cos | ].(- x),x.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ r) (#) (cos | ].(- x),x.[)) is set
diff (sin,].(- x),x.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (sin,].(- x),x.[)) . ((2 * r) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,].(- x),x.[)) . ((2 * r) + 1)) . 0 is V11() real ext-real Element of REAL
g - 0 is V11() real ext-real Element of REAL
(g - 0) |^ ((2 * r) + 1) is V11() real ext-real Element of REAL
(((diff (sin,].(- x),x.[)) . ((2 * r) + 1)) . 0) * ((g - 0) |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((diff (sin,].(- x),x.[)) . ((2 * r) + 1)) . 0) * ((g - 0) |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(((- 1) |^ r) (#) (cos | ].(- x),x.[)) . 0 is V11() real ext-real Element of REAL
((((- 1) |^ r) (#) (cos | ].(- x),x.[)) . 0) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
(((((- 1) |^ r) (#) (cos | ].(- x),x.[)) . 0) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(cos | ].(- x),x.[) . 0 is V11() real ext-real Element of REAL
((- 1) |^ r) * ((cos | ].(- x),x.[) . 0) is V11() real ext-real Element of REAL
(((- 1) |^ r) * ((cos | ].(- x),x.[) . 0)) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * ((cos | ].(- x),x.[) . 0)) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
((- 1) |^ r) * (cos . 0) is V11() real ext-real Element of REAL
(((- 1) |^ r) * (cos . 0)) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * (cos . 0)) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
sin | ].(- x),x.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((- 1) |^ r) (#) (sin | ].(- x),x.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ r) (#) (sin | ].(- x),x.[)) is set
dom (sin | ].(- x),x.[) is set
diff (cos,].(- x),x.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (cos,].(- x),x.[)) . (2 * r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,].(- x),x.[)) . (2 * r)) . 0 is V11() real ext-real Element of REAL
(g - 0) |^ (2 * r) is V11() real ext-real Element of REAL
(((diff (cos,].(- x),x.[)) . (2 * r)) . 0) * ((g - 0) |^ (2 * r)) is V11() real ext-real Element of REAL
((((diff (cos,].(- x),x.[)) . (2 * r)) . 0) * ((g - 0) |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
((((- 1) |^ r) (#) (cos | ].(- x),x.[)) . 0) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
(((((- 1) |^ r) (#) (cos | ].(- x),x.[)) . 0) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
(((- 1) |^ r) * ((cos | ].(- x),x.[) . 0)) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * ((cos | ].(- x),x.[) . 0)) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
(((- 1) |^ r) * (cos . 0)) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * (cos . 0)) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
r + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (r + 1) is V11() real ext-real Element of REAL
((- 1) |^ (r + 1)) (#) (sin | ].(- x),x.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ (r + 1)) (#) (sin | ].(- x),x.[)) is set
(diff (cos,].(- x),x.[)) . ((2 * r) + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,].(- x),x.[)) . ((2 * r) + 1)) . 0 is V11() real ext-real Element of REAL
(((diff (cos,].(- x),x.[)) . ((2 * r) + 1)) . 0) * ((g - 0) |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((diff (cos,].(- x),x.[)) . ((2 * r) + 1)) . 0) * ((g - 0) |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(((- 1) |^ (r + 1)) (#) (sin | ].(- x),x.[)) . 0 is V11() real ext-real Element of REAL
((((- 1) |^ (r + 1)) (#) (sin | ].(- x),x.[)) . 0) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
(((((- 1) |^ (r + 1)) (#) (sin | ].(- x),x.[)) . 0) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(sin | ].(- x),x.[) . 0 is V11() real ext-real Element of REAL
((- 1) |^ (r + 1)) * ((sin | ].(- x),x.[) . 0) is V11() real ext-real Element of REAL
(((- 1) |^ (r + 1)) * ((sin | ].(- x),x.[) . 0)) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((- 1) |^ (r + 1)) * ((sin | ].(- x),x.[) . 0)) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
((- 1) |^ (r + 1)) * (sin . 0) is V11() real ext-real Element of REAL
(((- 1) |^ (r + 1)) * (sin . 0)) * (g |^ ((2 * r) + 1)) is V11() real ext-real Element of REAL
((((- 1) |^ (r + 1)) * (sin . 0)) * (g |^ ((2 * r) + 1))) / (((2 * r) + 1) !) is V11() real ext-real Element of REAL
(diff (sin,].(- x),x.[)) . (2 * r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,].(- x),x.[)) . (2 * r)) . 0 is V11() real ext-real Element of REAL
(((diff (sin,].(- x),x.[)) . (2 * r)) . 0) * ((g - 0) |^ (2 * r)) is V11() real ext-real Element of REAL
((((diff (sin,].(- x),x.[)) . (2 * r)) . 0) * ((g - 0) |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
(((- 1) |^ r) (#) (sin | ].(- x),x.[)) . 0 is V11() real ext-real Element of REAL
((((- 1) |^ r) (#) (sin | ].(- x),x.[)) . 0) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
(((((- 1) |^ r) (#) (sin | ].(- x),x.[)) . 0) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
((- 1) |^ r) * ((sin | ].(- x),x.[) . 0) is V11() real ext-real Element of REAL
(((- 1) |^ r) * ((sin | ].(- x),x.[) . 0)) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * ((sin | ].(- x),x.[) . 0)) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
((- 1) |^ r) * (sin . 0) is V11() real ext-real Element of REAL
(((- 1) |^ r) * (sin . 0)) * (g |^ (2 * r)) is V11() real ext-real Element of REAL
((((- 1) |^ r) * (sin . 0)) * (g |^ (2 * r))) / ((2 * r) !) is V11() real ext-real Element of REAL
r is open V75() V76() V77() Element of K6(REAL)
x is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
x - 1 is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
diff (sin,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (sin,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (sin,r)) . g) is set
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ g is V11() real ext-real Element of REAL
((- 1) |^ g) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ g) (#) (sin | r)) is set
dom (sin | r) is set
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
diff (sin,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (sin,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (sin,r)) . g) is set
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ g is V11() real ext-real Element of REAL
((- 1) |^ g) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ g) (#) (cos | r)) is set
dom (cos | r) is set
diff (sin,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (sin,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (sin,r)) . g) is set
diff (sin,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (sin,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (sin,r)) . g) is set
((diff (sin,r)) . g) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ p is V11() real ext-real Element of REAL
((- 1) |^ p) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * p) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ p is V11() real ext-real Element of REAL
((- 1) |^ p) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
diff (cos,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (cos,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (cos,r)) . g) is set
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ g is V11() real ext-real Element of REAL
((- 1) |^ g) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ g) (#) (cos | r)) is set
dom (cos | r) is set
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
diff (cos,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (cos,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (cos,r)) . g) is set
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (g + 1) is V11() real ext-real Element of REAL
((- 1) |^ (g + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ (g + 1)) (#) (sin | r)) is set
dom (sin | r) is set
diff (cos,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (cos,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (cos,r)) . g) is set
diff (cos,r) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
(diff (cos,r)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom ((diff (cos,r)) . g) is set
((diff (cos,r)) . g) | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
cos | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ p is V11() real ext-real Element of REAL
((- 1) |^ p) (#) (cos | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * p) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
sin | r is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (p + 1) is V11() real ext-real Element of REAL
((- 1) |^ (p + 1)) (#) (sin | r) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (sin,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
diff (cos,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
x is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
0 - r is V11() real ext-real Element of REAL
0 + r is V11() real ext-real Element of REAL
].(0 - r),(0 + r).[ is open V75() V76() V77() Element of K6(REAL)
p - 0 is V11() real ext-real Element of REAL
abs (p - 0) is V11() real ext-real Element of REAL
abs p is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(abs p) |^ g is V11() real ext-real Element of REAL
g ! is V11() real ext-real Element of REAL
((abs p) |^ g) / (g !) is V11() real ext-real Element of REAL
g |^ g is V11() real ext-real Element of REAL
(g |^ g) / (g !) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(abs p) |^ n1 is V11() real ext-real Element of REAL
n1 ! is V11() real ext-real Element of REAL
((abs p) |^ n1) / (n1 !) is V11() real ext-real Element of REAL
g |^ n1 is V11() real ext-real Element of REAL
(g |^ n1) / (n1 !) is V11() real ext-real Element of REAL
n1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(abs p) |^ (n1 + 1) is V11() real ext-real Element of REAL
(n1 + 1) ! is V11() real ext-real Element of REAL
((abs p) |^ (n1 + 1)) / ((n1 + 1) !) is V11() real ext-real Element of REAL
g |^ (n1 + 1) is V11() real ext-real Element of REAL
(g |^ (n1 + 1)) / ((n1 + 1) !) is V11() real ext-real Element of REAL
((abs p) |^ n1) * (abs p) is V11() real ext-real Element of REAL
(((abs p) |^ n1) * (abs p)) / ((n1 + 1) !) is V11() real ext-real Element of REAL
(n1 !) * (n1 + 1) is V11() real ext-real Element of REAL
(((abs p) |^ n1) * (abs p)) / ((n1 !) * (n1 + 1)) is V11() real ext-real Element of REAL
(abs p) / ((n1 !) * (n1 + 1)) is V11() real ext-real Element of REAL
((abs p) |^ n1) * ((abs p) / ((n1 !) * (n1 + 1))) is V11() real ext-real Element of REAL
(abs p) / (n1 !) is V11() real ext-real Element of REAL
((abs p) / (n1 !)) / (n1 + 1) is V11() real ext-real Element of REAL
((abs p) |^ n1) * (((abs p) / (n1 !)) / (n1 + 1)) is V11() real ext-real Element of REAL
(n1 !) / (abs p) is V11() real ext-real Element of REAL
1 / ((n1 !) / (abs p)) is V11() real ext-real Element of REAL
(1 / ((n1 !) / (abs p))) / (n1 + 1) is V11() real ext-real Element of REAL
((abs p) |^ n1) * ((1 / ((n1 !) / (abs p))) / (n1 + 1)) is V11() real ext-real Element of REAL
1 / (n1 !) is V11() real ext-real Element of REAL
(1 / (n1 !)) * (abs p) is V11() real ext-real Element of REAL
((1 / (n1 !)) * (abs p)) / (n1 + 1) is V11() real ext-real Element of REAL
((abs p) |^ n1) * (((1 / (n1 !)) * (abs p)) / (n1 + 1)) is V11() real ext-real Element of REAL
((abs p) |^ n1) * ((1 / (n1 !)) * (abs p)) is V11() real ext-real Element of REAL
(((abs p) |^ n1) * ((1 / (n1 !)) * (abs p))) / (n1 + 1) is V11() real ext-real Element of REAL
((abs p) |^ n1) * (1 / (n1 !)) is V11() real ext-real Element of REAL
(((abs p) |^ n1) * (1 / (n1 !))) * (abs p) is V11() real ext-real Element of REAL
((((abs p) |^ n1) * (1 / (n1 !))) * (abs p)) / (n1 + 1) is V11() real ext-real Element of REAL
((abs p) |^ n1) * 1 is V11() real ext-real Element of REAL
(((abs p) |^ n1) * 1) / (n1 !) is V11() real ext-real Element of REAL
((((abs p) |^ n1) * 1) / (n1 !)) * (abs p) is V11() real ext-real Element of REAL
(((((abs p) |^ n1) * 1) / (n1 !)) * (abs p)) / (n1 + 1) is V11() real ext-real Element of REAL
(((abs p) |^ n1) / (n1 !)) * (abs p) is V11() real ext-real Element of REAL
((((abs p) |^ n1) / (n1 !)) * (abs p)) / (n1 + 1) is V11() real ext-real Element of REAL
p |^ n1 is V11() real ext-real Element of REAL
abs (p |^ n1) is V11() real ext-real Element of REAL
(abs (p |^ n1)) / (n1 !) is V11() real ext-real Element of REAL
abs (n1 !) is V11() real ext-real Element of REAL
(abs (p |^ n1)) / (abs (n1 !)) is V11() real ext-real Element of REAL
(p |^ n1) / (n1 !) is V11() real ext-real Element of REAL
abs ((p |^ n1) / (n1 !)) is V11() real ext-real Element of REAL
(g |^ n1) * g is V11() real ext-real Element of REAL
((g |^ n1) * g) / ((n1 + 1) !) is V11() real ext-real Element of REAL
((g |^ n1) * g) / ((n1 !) * (n1 + 1)) is V11() real ext-real Element of REAL
g / ((n1 !) * (n1 + 1)) is V11() real ext-real Element of REAL
(g |^ n1) * (g / ((n1 !) * (n1 + 1))) is V11() real ext-real Element of REAL
g / (n1 !) is V11() real ext-real Element of REAL
(g / (n1 !)) / (n1 + 1) is V11() real ext-real Element of REAL
(g |^ n1) * ((g / (n1 !)) / (n1 + 1)) is V11() real ext-real Element of REAL
(n1 !) / g is V11() real ext-real Element of REAL
1 / ((n1 !) / g) is V11() real ext-real Element of REAL
(1 / ((n1 !) / g)) / (n1 + 1) is V11() real ext-real Element of REAL
(g |^ n1) * ((1 / ((n1 !) / g)) / (n1 + 1)) is V11() real ext-real Element of REAL
(1 / (n1 !)) * g is V11() real ext-real Element of REAL
((1 / (n1 !)) * g) / (n1 + 1) is V11() real ext-real Element of REAL
(g |^ n1) * (((1 / (n1 !)) * g) / (n1 + 1)) is V11() real ext-real Element of REAL
(g |^ n1) * ((1 / (n1 !)) * g) is V11() real ext-real Element of REAL
((g |^ n1) * ((1 / (n1 !)) * g)) / (n1 + 1) is V11() real ext-real Element of REAL
(g |^ n1) * (1 / (n1 !)) is V11() real ext-real Element of REAL
((g |^ n1) * (1 / (n1 !))) * g is V11() real ext-real Element of REAL
(((g |^ n1) * (1 / (n1 !))) * g) / (n1 + 1) is V11() real ext-real Element of REAL
(g |^ n1) * 1 is V11() real ext-real Element of REAL
((g |^ n1) * 1) / (n1 !) is V11() real ext-real Element of REAL
(((g |^ n1) * 1) / (n1 !)) * g is V11() real ext-real Element of REAL
((((g |^ n1) * 1) / (n1 !)) * g) / (n1 + 1) is V11() real ext-real Element of REAL
((g |^ n1) / (n1 !)) * g is V11() real ext-real Element of REAL
(((g |^ n1) / (n1 !)) * g) / (n1 + 1) is V11() real ext-real Element of REAL
(abs p) |^ 0 is V11() real ext-real Element of REAL
0 ! is V11() real ext-real Element of REAL
((abs p) |^ 0) / (0 !) is V11() real ext-real Element of REAL
1 / (0 !) is V11() real ext-real Element of REAL
g |^ 0 is V11() real ext-real Element of REAL
(g |^ 0) / (0 !) is V11() real ext-real Element of REAL
1 * r is V11() real ext-real Element of REAL
n * (abs p) is V11() real ext-real Element of REAL
abs n is V11() real ext-real Element of REAL
(abs n) * (abs p) is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
(n * p) - 0 is V11() real ext-real Element of REAL
abs ((n * p) - 0) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ n1 is V11() real ext-real Element of REAL
abs ((- 1) |^ n1) is V11() real ext-real Element of REAL
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (1 + 1) is V11() real ext-real Element of REAL
((- 1) |^ (1 + 1)) |^ m1 is V11() real ext-real Element of REAL
abs (((- 1) |^ (1 + 1)) |^ m1) is V11() real ext-real Element of REAL
(- 1) |^ 1 is V11() real ext-real Element of REAL
((- 1) |^ 1) * (- 1) is V11() real ext-real Element of REAL
(((- 1) |^ 1) * (- 1)) |^ m1 is V11() real ext-real Element of REAL
abs ((((- 1) |^ 1) * (- 1)) |^ m1) is V11() real ext-real Element of REAL
(- 1) * (- 1) is V11() real ext-real non negative Element of REAL
((- 1) * (- 1)) |^ m1 is V11() real ext-real Element of REAL
abs (((- 1) * (- 1)) |^ m1) is V11() real ext-real Element of REAL
abs 1 is V11() real ext-real V74() Element of REAL
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * m1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (2 * m1) is V11() real ext-real Element of REAL
((- 1) |^ (2 * m1)) * (- 1) is V11() real ext-real Element of REAL
abs (((- 1) |^ (2 * m1)) * (- 1)) is V11() real ext-real Element of REAL
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (1 + 1) is V11() real ext-real Element of REAL
((- 1) |^ (1 + 1)) |^ m1 is V11() real ext-real Element of REAL
(((- 1) |^ (1 + 1)) |^ m1) * (- 1) is V11() real ext-real Element of REAL
abs ((((- 1) |^ (1 + 1)) |^ m1) * (- 1)) is V11() real ext-real Element of REAL
(- 1) |^ 1 is V11() real ext-real Element of REAL
((- 1) |^ 1) * (- 1) is V11() real ext-real Element of REAL
(((- 1) |^ 1) * (- 1)) |^ m1 is V11() real ext-real Element of REAL
((((- 1) |^ 1) * (- 1)) |^ m1) * (- 1) is V11() real ext-real Element of REAL
abs (((((- 1) |^ 1) * (- 1)) |^ m1) * (- 1)) is V11() real ext-real Element of REAL
(- 1) * (- 1) is V11() real ext-real non negative Element of REAL
((- 1) * (- 1)) |^ m1 is V11() real ext-real Element of REAL
(((- 1) * (- 1)) |^ m1) * (- 1) is V11() real ext-real Element of REAL
abs ((((- 1) * (- 1)) |^ m1) * (- 1)) is V11() real ext-real Element of REAL
1 * (- 1) is V11() real ext-real non positive Element of REAL
abs (1 * (- 1)) is V11() real ext-real Element of REAL
abs 1 is V11() real ext-real V74() Element of REAL
(diff (sin,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (sin,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
abs (((diff (sin,].(- r),r.[)) . g) . (n * p)) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
sin | ].(- r),r.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ n1 is V11() real ext-real Element of REAL
((- 1) |^ n1) (#) (sin | ].(- r),r.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ n1) (#) (sin | ].(- r),r.[)) is set
dom (sin | ].(- r),r.[) is set
sin (n * p) is V11() real ext-real Element of REAL
abs (sin (n * p)) is V11() real ext-real Element of REAL
(((- 1) |^ n1) (#) (sin | ].(- r),r.[)) . (n * p) is V11() real ext-real Element of REAL
abs ((((- 1) |^ n1) (#) (sin | ].(- r),r.[)) . (n * p)) is V11() real ext-real Element of REAL
(sin | ].(- r),r.[) . (n * p) is V11() real ext-real Element of REAL
((- 1) |^ n1) * ((sin | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
abs (((- 1) |^ n1) * ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
abs ((- 1) |^ n1) is V11() real ext-real Element of REAL
abs ((sin | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
(abs ((- 1) |^ n1)) * (abs ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
1 * (abs ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
sin . (n * p) is V11() real ext-real Element of REAL
abs (sin . (n * p)) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * n1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
cos | ].(- r),r.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ n1 is V11() real ext-real Element of REAL
((- 1) |^ n1) (#) (cos | ].(- r),r.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ n1) (#) (cos | ].(- r),r.[)) is set
dom (cos | ].(- r),r.[) is set
cos (n * p) is V11() real ext-real Element of REAL
abs (cos (n * p)) is V11() real ext-real Element of REAL
(((- 1) |^ n1) (#) (cos | ].(- r),r.[)) . (n * p) is V11() real ext-real Element of REAL
abs ((((- 1) |^ n1) (#) (cos | ].(- r),r.[)) . (n * p)) is V11() real ext-real Element of REAL
(cos | ].(- r),r.[) . (n * p) is V11() real ext-real Element of REAL
((- 1) |^ n1) * ((cos | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
abs (((- 1) |^ n1) * ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
abs ((- 1) |^ n1) is V11() real ext-real Element of REAL
abs ((cos | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
(abs ((- 1) |^ n1)) * (abs ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
1 * (abs ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
cos . (n * p) is V11() real ext-real Element of REAL
abs (cos . (n * p)) is V11() real ext-real Element of REAL
(diff (cos,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
abs (((diff (cos,].(- r),r.[)) . g) . (n * p)) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
cos | ].(- r),r.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
(- 1) |^ n1 is V11() real ext-real Element of REAL
((- 1) |^ n1) (#) (cos | ].(- r),r.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ n1) (#) (cos | ].(- r),r.[)) is set
dom (cos | ].(- r),r.[) is set
cos (n * p) is V11() real ext-real Element of REAL
abs (cos (n * p)) is V11() real ext-real Element of REAL
(((- 1) |^ n1) (#) (cos | ].(- r),r.[)) . (n * p) is V11() real ext-real Element of REAL
abs ((((- 1) |^ n1) (#) (cos | ].(- r),r.[)) . (n * p)) is V11() real ext-real Element of REAL
(cos | ].(- r),r.[) . (n * p) is V11() real ext-real Element of REAL
((- 1) |^ n1) * ((cos | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
abs (((- 1) |^ n1) * ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
abs ((- 1) |^ n1) is V11() real ext-real Element of REAL
abs ((cos | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
(abs ((- 1) |^ n1)) * (abs ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
1 * (abs ((cos | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
cos . (n * p) is V11() real ext-real Element of REAL
abs (cos . (n * p)) is V11() real ext-real Element of REAL
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * n1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
sin | ].(- r),r.[ is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n1 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(- 1) |^ (n1 + 1) is V11() real ext-real Element of REAL
((- 1) |^ (n1 + 1)) (#) (sin | ].(- r),r.[) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
dom (((- 1) |^ (n1 + 1)) (#) (sin | ].(- r),r.[)) is set
dom (sin | ].(- r),r.[) is set
sin (n * p) is V11() real ext-real Element of REAL
abs (sin (n * p)) is V11() real ext-real Element of REAL
(((- 1) |^ (n1 + 1)) (#) (sin | ].(- r),r.[)) . (n * p) is V11() real ext-real Element of REAL
abs ((((- 1) |^ (n1 + 1)) (#) (sin | ].(- r),r.[)) . (n * p)) is V11() real ext-real Element of REAL
(sin | ].(- r),r.[) . (n * p) is V11() real ext-real Element of REAL
((- 1) |^ (n1 + 1)) * ((sin | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
abs (((- 1) |^ (n1 + 1)) * ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
abs ((- 1) |^ (n1 + 1)) is V11() real ext-real Element of REAL
abs ((sin | ].(- r),r.[) . (n * p)) is V11() real ext-real Element of REAL
(abs ((- 1) |^ (n1 + 1))) * (abs ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
1 * (abs ((sin | ].(- r),r.[) . (n * p))) is V11() real ext-real Element of REAL
sin . (n * p) is V11() real ext-real Element of REAL
abs (sin . (n * p)) is V11() real ext-real Element of REAL
p |^ g is V11() real ext-real Element of REAL
(p |^ g) / (g !) is V11() real ext-real Element of REAL
abs ((p |^ g) / (g !)) is V11() real ext-real Element of REAL
abs (p |^ g) is V11() real ext-real Element of REAL
abs (g !) is V11() real ext-real Element of REAL
(abs (p |^ g)) / (abs (g !)) is V11() real ext-real Element of REAL
(abs (p |^ g)) / (g !) is V11() real ext-real Element of REAL
(((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
(((diff (cos,].(- r),r.[)) . g) . (n * p)) * ((p |^ g) / (g !)) is V11() real ext-real Element of REAL
abs ((((diff (cos,].(- r),r.[)) . g) . (n * p)) * ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
(abs (((diff (cos,].(- r),r.[)) . g) . (n * p))) * (abs ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
(abs (((diff (cos,].(- r),r.[)) . g) . (n * p))) * ((abs p) |^ g) is V11() real ext-real Element of REAL
((abs (((diff (cos,].(- r),r.[)) . g) . (n * p))) * ((abs p) |^ g)) / (g !) is V11() real ext-real Element of REAL
(((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
(((diff (sin,].(- r),r.[)) . g) . (n * p)) * ((p |^ g) / (g !)) is V11() real ext-real Element of REAL
abs ((((diff (sin,].(- r),r.[)) . g) . (n * p)) * ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
(abs (((diff (sin,].(- r),r.[)) . g) . (n * p))) * (abs ((p |^ g) / (g !))) is V11() real ext-real Element of REAL
(abs (((diff (sin,].(- r),r.[)) . g) . (n * p))) * ((abs p) |^ g) is V11() real ext-real Element of REAL
((abs (((diff (sin,].(- r),r.[)) . g) . (n * p))) * ((abs p) |^ g)) / (g !) is V11() real ext-real Element of REAL
(abs (((diff (cos,].(- r),r.[)) . g) . (n * p))) * (((abs p) |^ g) / (g !)) is V11() real ext-real Element of REAL
x * ((g |^ g) / (g !)) is V11() real ext-real Element of REAL
(abs (((diff (sin,].(- r),r.[)) . g) . (n * p))) * (((abs p) |^ g) / (g !)) is V11() real ext-real Element of REAL
x * (g |^ g) is V11() real ext-real Element of REAL
(x * (g |^ g)) / (g !) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n * p is V11() real ext-real Element of REAL
((diff (sin,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
p |^ g is V11() real ext-real Element of REAL
(((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
g ! is V11() real ext-real Element of REAL
((((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (sin,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
g |^ g is V11() real ext-real Element of REAL
x * (g |^ g) is V11() real ext-real Element of REAL
(x * (g |^ g)) / (g !) is V11() real ext-real Element of REAL
(diff (cos,].(- r),r.[)) . g is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
((diff (cos,].(- r),r.[)) . g) . (n * p) is V11() real ext-real Element of REAL
(((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g) is V11() real ext-real Element of REAL
((((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !) is V11() real ext-real Element of REAL
abs (((((diff (cos,].(- r),r.[)) . g) . (n * p)) * (p |^ g)) / (g !)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (sin,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
diff (cos,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
g is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
n is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(diff (sin,].(- r),r.[)) . n is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n ! is V11() real ext-real Element of REAL
(diff (cos,].(- r),r.[)) . n is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
g |^ n is V11() real ext-real Element of REAL
g * (g |^ n) is V11() real ext-real Element of REAL
(g * (g |^ n)) / (n !) is V11() real ext-real Element of REAL
n1 is V11() real ext-real Element of REAL
m1 is V11() real ext-real Element of REAL
m1 * n1 is V11() real ext-real Element of REAL
((diff (sin,].(- r),r.[)) . n) . (m1 * n1) is V11() real ext-real Element of REAL
n1 |^ n is V11() real ext-real Element of REAL
(((diff (sin,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n) is V11() real ext-real Element of REAL
((((diff (sin,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !) is V11() real ext-real Element of REAL
abs (((((diff (sin,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !)) is V11() real ext-real Element of REAL
((diff (cos,].(- r),r.[)) . n) . (m1 * n1) is V11() real ext-real Element of REAL
(((diff (cos,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n) is V11() real ext-real Element of REAL
((((diff (cos,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !) is V11() real ext-real Element of REAL
abs (((((diff (cos,].(- r),r.[)) . n) . (m1 * n1)) * (n1 |^ n)) / (n !)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
diff (sin,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
diff (cos,].(- r),r.[) is Relation-like NAT -defined PFuncs (REAL,REAL) -valued V21() V30( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
dom cos is set
dom sin is set
p is V11() real ext-real Element of REAL
sin . p is V11() real ext-real Element of REAL
(sin,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (sin,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (sin,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(sin . p) - ((Partial_Sums (sin,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((sin . p) - ((Partial_Sums (sin,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
(diff (sin,].(- r),r.[)) . (g + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
p |^ (g + 1) is V11() real ext-real Element of REAL
(g + 1) ! is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
((diff (sin,].(- r),r.[)) . (g + 1)) . (n * p) is V11() real ext-real Element of REAL
(((diff (sin,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1)) is V11() real ext-real Element of REAL
((((diff (sin,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !) is V11() real ext-real Element of REAL
abs (((((diff (sin,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !)) is V11() real ext-real Element of REAL
cos . p is V11() real ext-real Element of REAL
(cos,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (cos,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(cos . p) - ((Partial_Sums (cos,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((cos . p) - ((Partial_Sums (cos,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
(diff (cos,].(- r),r.[)) . (g + 1) is Relation-like REAL -defined REAL -valued V21() V33() V34() V35() Element of K6(K7(REAL,REAL))
n is V11() real ext-real Element of REAL
n * p is V11() real ext-real Element of REAL
((diff (cos,].(- r),r.[)) . (g + 1)) . (n * p) is V11() real ext-real Element of REAL
(((diff (cos,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1)) is V11() real ext-real Element of REAL
((((diff (cos,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !) is V11() real ext-real Element of REAL
abs (((((diff (cos,].(- r),r.[)) . (g + 1)) . (n * p)) * (p |^ (g + 1))) / ((g + 1) !)) is V11() real ext-real Element of REAL
p is V11() real ext-real set
sin . p is V11() real ext-real Element of REAL
(sin,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (sin,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (sin,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(sin . p) - ((Partial_Sums (sin,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((sin . p) - ((Partial_Sums (sin,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
cos . p is V11() real ext-real Element of REAL
(cos,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,p) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(Partial_Sums (cos,].(- r),r.[,p)) . g is V11() real ext-real Element of REAL
(cos . p) - ((Partial_Sums (cos,].(- r),r.[,p)) . g) is V11() real ext-real Element of REAL
abs ((cos . p) - ((Partial_Sums (cos,].(- r),r.[,p)) . g)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x P_sin is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x P_sin) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x P_cos is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x P_cos) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_sin)) . g is V11() real ext-real Element of REAL
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . g is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_sin)) . g is V11() real ext-real Element of REAL
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * (g + 1) is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * (g + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * (g + 1)) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_sin)) . (g + 1) is V11() real ext-real Element of REAL
(2 * g) + 2 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 2) is V11() real ext-real Element of REAL
3 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 3 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(sin,].(- r),r.[,x) . ((2 * g) + 3) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 2)) + ((sin,].(- r),r.[,x) . ((2 * g) + 3)) is V11() real ext-real Element of REAL
(- 1) |^ (g + 1) is V11() real ext-real Element of REAL
x |^ ((2 * (g + 1)) + 1) is V11() real ext-real Element of REAL
((- 1) |^ (g + 1)) * (x |^ ((2 * (g + 1)) + 1)) is V11() real ext-real Element of REAL
((2 * (g + 1)) + 1) ! is V11() real ext-real Element of REAL
(((- 1) |^ (g + 1)) * (x |^ ((2 * (g + 1)) + 1))) / (((2 * (g + 1)) + 1) !) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 2)) + ((((- 1) |^ (g + 1)) * (x |^ ((2 * (g + 1)) + 1))) / (((2 * (g + 1)) + 1) !)) is V11() real ext-real Element of REAL
((2 * g) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . (((2 * g) + 1) + 1) is V11() real ext-real Element of REAL
(x P_sin) . (g + 1) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . (((2 * g) + 1) + 1)) + ((x P_sin) . (g + 1)) is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) . (2 * (g + 1)) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1)) + ((sin,].(- r),r.[,x) . (2 * (g + 1))) is V11() real ext-real Element of REAL
(((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1)) + ((sin,].(- r),r.[,x) . (2 * (g + 1)))) + ((x P_sin) . (g + 1)) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1)) + 0 is V11() real ext-real Element of REAL
(((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) + 1)) + 0) + ((x P_sin) . (g + 1)) is V11() real ext-real Element of REAL
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * 0) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * 0) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (sin,].(- r),r.[,x)) . (2 * 0) is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) . ((2 * 0) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . (2 * 0)) + ((sin,].(- r),r.[,x) . ((2 * 0) + 1)) is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) . (2 * 0) is V11() real ext-real Element of REAL
((sin,].(- r),r.[,x) . (2 * 0)) + ((sin,].(- r),r.[,x) . ((2 * 0) + 1)) is V11() real ext-real Element of REAL
0 + ((sin,].(- r),r.[,x) . ((2 * 0) + 1)) is V11() real ext-real Element of REAL
(- 1) |^ 0 is V11() real ext-real Element of REAL
x |^ ((2 * 0) + 1) is V11() real ext-real Element of REAL
((- 1) |^ 0) * (x |^ ((2 * 0) + 1)) is V11() real ext-real Element of REAL
((2 * 0) + 1) ! is V11() real ext-real Element of REAL
(((- 1) |^ 0) * (x |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !) is V11() real ext-real Element of REAL
(x P_sin) . 0 is V11() real ext-real Element of REAL
(Partial_Sums (x P_sin)) . 0 is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . g is V11() real ext-real Element of REAL
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * (g + 1) is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * (g + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * (g + 1)) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . (g + 1) is V11() real ext-real Element of REAL
(2 * g) + 2 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 2) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . ((2 * (g + 1)) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 2)) + ((cos,].(- r),r.[,x) . ((2 * (g + 1)) + 1)) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 2)) + 0 is V11() real ext-real Element of REAL
((2 * g) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . (((2 * g) + 1) + 1) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . ((2 * g) + 2) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1)) + ((cos,].(- r),r.[,x) . ((2 * g) + 2)) is V11() real ext-real Element of REAL
(- 1) |^ (g + 1) is V11() real ext-real Element of REAL
x |^ (2 * (g + 1)) is V11() real ext-real Element of REAL
((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1))) is V11() real ext-real Element of REAL
(2 * (g + 1)) ! is V11() real ext-real Element of REAL
(((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1)))) / ((2 * (g + 1)) !) is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . g) + ((((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1)))) / ((2 * (g + 1)) !)) is V11() real ext-real Element of REAL
(x P_cos) . (g + 1) is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . g) + ((x P_cos) . (g + 1)) is V11() real ext-real Element of REAL
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * 0) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * 0) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * 0) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . ((2 * 0) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . (2 * 0)) + ((cos,].(- r),r.[,x) . ((2 * 0) + 1)) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . (2 * 0) is V11() real ext-real Element of REAL
((cos,].(- r),r.[,x) . (2 * 0)) + ((cos,].(- r),r.[,x) . ((2 * 0) + 1)) is V11() real ext-real Element of REAL
((cos,].(- r),r.[,x) . (2 * 0)) + 0 is V11() real ext-real Element of REAL
(- 1) |^ 0 is V11() real ext-real Element of REAL
x |^ (2 * 0) is V11() real ext-real Element of REAL
((- 1) |^ 0) * (x |^ (2 * 0)) is V11() real ext-real Element of REAL
(2 * 0) ! is V11() real ext-real Element of REAL
(((- 1) |^ 0) * (x |^ (2 * 0))) / ((2 * 0) !) is V11() real ext-real Element of REAL
(x P_cos) . 0 is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . 0 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x P_sin is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x P_sin) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
(cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x P_cos is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x P_cos) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . (2 * g) is V11() real ext-real Element of REAL
g - 1 is V11() real ext-real Element of REAL
(Partial_Sums (x P_sin)) . (g - 1) is V11() real ext-real Element of REAL
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * g) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . g is V11() real ext-real Element of REAL
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * g) - 1 is V11() real ext-real Element of REAL
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) - 1) is V11() real ext-real Element of REAL
((2 * g) - 1) + 1 is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) . (((2 * g) - 1) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) - 1)) + ((sin,].(- r),r.[,x) . (((2 * g) - 1) + 1)) is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . ((2 * g) - 1)) + 0 is V11() real ext-real Element of REAL
2 * (g - 1) is V11() real ext-real Element of REAL
(2 * (g - 1)) + 1 is V11() real ext-real Element of REAL
(Partial_Sums (sin,].(- r),r.[,x)) . ((2 * (g - 1)) + 1) is V11() real ext-real Element of REAL
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) - 1) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . (((2 * g) - 1) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) - 1)) + ((cos,].(- r),r.[,x) . (((2 * g) - 1) + 1)) is V11() real ext-real Element of REAL
(- 1) |^ g is V11() real ext-real Element of REAL
x |^ (2 * g) is V11() real ext-real Element of REAL
((- 1) |^ g) * (x |^ (2 * g)) is V11() real ext-real Element of REAL
(2 * g) ! is V11() real ext-real Element of REAL
(((- 1) |^ g) * (x |^ (2 * g))) / ((2 * g) !) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) - 1)) + ((((- 1) |^ g) * (x |^ (2 * g))) / ((2 * g) !)) is V11() real ext-real Element of REAL
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * (g - 1)) + 1) is V11() real ext-real Element of REAL
(x P_cos) . g is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * (g - 1)) + 1)) + ((x P_cos) . g) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . (g - 1) is V11() real ext-real Element of REAL
(g - 1) + 1 is V11() real ext-real Element of REAL
(x P_cos) . ((g - 1) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . (g - 1)) + ((x P_cos) . ((g - 1) + 1)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
x P_cos is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (x P_cos) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * g) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . g is V11() real ext-real Element of REAL
g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * g is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * g) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . g is V11() real ext-real Element of REAL
g + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * (g + 1) is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * (g + 1)) is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . (g + 1) is V11() real ext-real Element of REAL
(2 * g) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1) is V11() real ext-real Element of REAL
((2 * g) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(cos,].(- r),r.[,x) . (((2 * g) + 1) + 1) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1)) + ((cos,].(- r),r.[,x) . (((2 * g) + 1) + 1)) is V11() real ext-real Element of REAL
(- 1) |^ (g + 1) is V11() real ext-real Element of REAL
x |^ (2 * (g + 1)) is V11() real ext-real Element of REAL
((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1))) is V11() real ext-real Element of REAL
(2 * (g + 1)) ! is V11() real ext-real Element of REAL
(((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1)))) / ((2 * (g + 1)) !) is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . ((2 * g) + 1)) + ((((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1)))) / ((2 * (g + 1)) !)) is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . g) + ((((- 1) |^ (g + 1)) * (x |^ (2 * (g + 1)))) / ((2 * (g + 1)) !)) is V11() real ext-real Element of REAL
(x P_cos) . (g + 1) is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . g) + ((x P_cos) . (g + 1)) is V11() real ext-real Element of REAL
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative V61() V74() V75() V76() V77() V78() V79() V80() V81() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . (2 * 0) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) . (2 * 0) is V11() real ext-real Element of REAL
(- 1) |^ 0 is V11() real ext-real Element of REAL
x |^ (2 * 0) is V11() real ext-real Element of REAL
((- 1) |^ 0) * (x |^ (2 * 0)) is V11() real ext-real Element of REAL
(2 * 0) ! is V11() real ext-real Element of REAL
(((- 1) |^ 0) * (x |^ (2 * 0))) / ((2 * 0) !) is V11() real ext-real Element of REAL
(x P_cos) . 0 is V11() real ext-real Element of REAL
(Partial_Sums (x P_cos)) . 0 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
- r is V11() real ext-real Element of REAL
].(- r),r.[ is open V75() V76() V77() Element of K6(REAL)
x is V11() real ext-real Element of REAL
(sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (sin,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (sin,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
sin . x is V11() real ext-real Element of REAL
Sum (sin,].(- r),r.[,x) is V11() real ext-real Element of REAL
(cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Taylor (cos,].(- r),r.[,0,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Partial_Sums (cos,].(- r),r.[,x) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
cos . x is V11() real ext-real Element of REAL
Sum (cos,].(- r),r.[,x) is V11() real ext-real Element of REAL
x P_sin is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (x P_sin) is V11() real ext-real Element of REAL
Partial_Sums (x P_sin) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
lim (Partial_Sums (x P_sin)) is V11() real ext-real Element of REAL
g is V11() real ext-real set
p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * p is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * p) + 2 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
n1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (sin,].(- r),r.[,x)) . n1 is V11() real ext-real Element of REAL
((Partial_Sums (sin,].(- r),r.[,x)) . n1) - (sin . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (sin,].(- r),r.[,x)) . n1) - (sin . x)) is V11() real ext-real Element of REAL
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(p + 1) * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
((p + 1) * 2) / 2 is V11() real ext-real non negative Element of REAL
m1 * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(m1 * 2) / 2 is V11() real ext-real non negative Element of REAL
(p + 1) - 1 is V11() real ext-real Element of REAL
m1 - 1 is V11() real ext-real Element of REAL
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (x P_sin)) . (m1 - 1) is V11() real ext-real Element of REAL
((Partial_Sums (x P_sin)) . (m1 - 1)) - (sin . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (x P_sin)) . (m1 - 1)) - (sin . x)) is V11() real ext-real Element of REAL
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * m1) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
p * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(p * 2) + 0 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(p * 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(p * 2) + 2 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
((p * 2) + 2) - 1 is V11() real ext-real Element of REAL
((2 * m1) + 1) - 1 is V11() real ext-real Element of REAL
m1 * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(p * 2) / 2 is V11() real ext-real non negative Element of REAL
(m1 * 2) / 2 is V11() real ext-real non negative Element of REAL
(Partial_Sums (x P_sin)) . m1 is V11() real ext-real Element of REAL
((Partial_Sums (x P_sin)) . m1) - (sin . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (x P_sin)) . m1) - (sin . x)) is V11() real ext-real Element of REAL
lim (Partial_Sums (sin,].(- r),r.[,x)) is V11() real ext-real Element of REAL
x P_cos is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
Sum (x P_cos) is V11() real ext-real Element of REAL
Partial_Sums (x P_cos) is Relation-like NAT -defined REAL -valued V21() total V30( NAT , REAL ) V33() V34() V35() Element of K6(K7(NAT,REAL))
lim (Partial_Sums (x P_cos)) is V11() real ext-real Element of REAL
p is V11() real ext-real set
n is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * n is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * n) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
m1 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(Partial_Sums (cos,].(- r),r.[,x)) . m1 is V11() real ext-real Element of REAL
((Partial_Sums (cos,].(- r),r.[,x)) . m1) - (cos . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (cos,].(- r),r.[,x)) . m1) - (cos . x)) is V11() real ext-real Element of REAL
j is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * j is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
n * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(n * 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
j * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(n * 2) / 2 is V11() real ext-real non negative Element of REAL
(j * 2) / 2 is V11() real ext-real non negative Element of REAL
(Partial_Sums (x P_cos)) . j is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . j) - (cos . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (x P_cos)) . j) - (cos . x)) is V11() real ext-real Element of REAL
j is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
2 * j is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(2 * j) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
n * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(n * 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
((n * 2) + 1) - 1 is V11() real ext-real Element of REAL
j * 2 is ordinal natural V11() real ext-real non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
(j * 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative V61() V74() V75() V76() V77() V78() V79() V80() Element of NAT
((j * 2) + 1) - 1 is V11() real ext-real Element of REAL
(n * 2) / 2 is V11() real ext-real non negative Element of REAL
(j * 2) / 2 is V11() real ext-real non negative Element of REAL
(Partial_Sums (x P_cos)) . j is V11() real ext-real Element of REAL
((Partial_Sums (x P_cos)) . j) - (cos . x) is V11() real ext-real Element of REAL
abs (((Partial_Sums (x P_cos)) . j) - (cos . x)) is V11() real ext-real Element of REAL
lim (Partial_Sums (cos,].(- r),r.[,x)) is V11() real ext-real Element of REAL