:: HOLDER_1 semantic presentation

REAL is non empty V67() V72() V73() V74() V78() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V67() V72() V78() set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
RAT is non empty V67() V72() V73() V74() V75() V78() set
INT is non empty V67() V72() V73() V74() V75() V76() V78() set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V66() V72() V73() V74() V75() V76() V77() V78() Element of NAT
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V72() V73() V74() V75() V76() V77() V78() set
right_open_halfline 0 is V50() V72() V73() V74() Element of K19(REAL)
+infty is non empty non real ext-real positive non negative set
K162(0,+infty) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
omega is non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() set
p is V22() real ext-real set
right_closed_halfline p is V49() V72() V73() V74() Element of K19(REAL)
K160(p,+infty) is set
a is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : a <= b₁ } is set
p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
p + a is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
b to_power p is V22() real ext-real Element of REAL
b to_power a is V22() real ext-real Element of REAL
(b to_power p) * (b to_power a) is V22() real ext-real Element of REAL
b to_power (p + a) is V22() real ext-real Element of REAL
0 to_power a is V22() real ext-real Element of REAL
0 * (0 to_power a) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
p * a is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
b to_power p is V22() real ext-real Element of REAL
(b to_power p) to_power a is V22() real ext-real Element of REAL
b to_power (p * a) is V22() real ext-real Element of REAL
0 to_power a is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
a to_power p is V22() real ext-real Element of REAL
b to_power p is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
1 / p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
1 / a is V22() real ext-real Element of REAL
(1 / p) + (1 / a) is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
b #R p is V22() real ext-real Element of REAL
(b #R p) / p is V22() real ext-real Element of REAL
ap is V22() real ext-real Element of REAL
b * ap is V22() real ext-real Element of REAL
ap #R a is V22() real ext-real Element of REAL
(ap #R a) / a is V22() real ext-real Element of REAL
((b #R p) / p) + ((ap #R a) / a) is V22() real ext-real Element of REAL
bp is V22() real ext-real Element of REAL
1 - bp is V22() real ext-real Element of REAL
a " is V22() real ext-real Element of REAL
(a ") " is V22() real ext-real Element of REAL
1 * a is V22() real ext-real Element of REAL
1 * p is V22() real ext-real Element of REAL
(1 * a) + (1 * p) is V22() real ext-real Element of REAL
p * a is V22() real ext-real Element of REAL
((1 * a) + (1 * p)) / (p * a) is V22() real ext-real Element of REAL
(((1 * a) + (1 * p)) / (p * a)) * (p * a) is V22() real ext-real Element of REAL
1 * (p * a) is V22() real ext-real Element of REAL
a + p is V22() real ext-real Element of REAL
a - 1 is V22() real ext-real Element of REAL
(a - 1) * p is V22() real ext-real Element of REAL
ap #R (a - 1) is V22() real ext-real Element of REAL
(ap #R (a - 1)) #R p is V22() real ext-real Element of REAL
b #R 1 is V22() real ext-real Element of REAL
p * (1 / p) is V22() real ext-real Element of REAL
b #R (p * (1 / p)) is V22() real ext-real Element of REAL
(b #R p) #R (1 / p) is V22() real ext-real Element of REAL
(ap #R (a - 1)) #R (p * (1 / p)) is V22() real ext-real Element of REAL
(ap #R (a - 1)) #R 1 is V22() real ext-real Element of REAL
b * 1 is V22() real ext-real Element of REAL
1 - a is V22() real ext-real Element of REAL
(1 - a) + (a - 1) is V22() real ext-real Element of REAL
ap #R ((1 - a) + (a - 1)) is V22() real ext-real Element of REAL
b * (ap #R ((1 - a) + (a - 1))) is V22() real ext-real Element of REAL
ap #R (1 - a) is V22() real ext-real Element of REAL
(ap #R (1 - a)) * (ap #R (a - 1)) is V22() real ext-real Element of REAL
b * ((ap #R (1 - a)) * (ap #R (a - 1))) is V22() real ext-real Element of REAL
1 * (ap #R (a - 1)) is V22() real ext-real Element of REAL
b * (ap #R (1 - a)) is V22() real ext-real Element of REAL
(b * (ap #R (1 - a))) * (ap #R (a - 1)) is V22() real ext-real Element of REAL
(ap #R a) * (1 / p) is V22() real ext-real Element of REAL
((ap #R a) * (1 / p)) + ((ap #R a) / a) is V22() real ext-real Element of REAL
(ap #R a) * (1 / a) is V22() real ext-real Element of REAL
((ap #R a) * (1 / p)) + ((ap #R a) * (1 / a)) is V22() real ext-real Element of REAL
(ap #R a) * ((1 / p) + (1 / a)) is V22() real ext-real Element of REAL
(ap #R a) * (b * (ap #R (1 - a))) is V22() real ext-real Element of REAL
(ap #R (1 - a)) * (ap #R a) is V22() real ext-real Element of REAL
b * ((ap #R (1 - a)) * (ap #R a)) is V22() real ext-real Element of REAL
(1 - a) + a is V22() real ext-real Element of REAL
ap #R ((1 - a) + a) is V22() real ext-real Element of REAL
b * (ap #R ((1 - a) + a)) is V22() real ext-real Element of REAL
0 * (ap #R (1 - a)) is V22() real ext-real Element of REAL
p - 1 is V22() real ext-real Element of REAL
#R p is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1 / p) (#) (#R p) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((1 / p) (#) (#R p)) is set
dom (#R p) is set
z is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 0 } is set
((1 / p) (#) (#R p)) . z is V22() real ext-real Element of REAL
(#R p) . z is V22() real ext-real Element of REAL
(1 / p) * ((#R p) . z) is V22() real ext-real Element of REAL
z #R p is V22() real ext-real Element of REAL
(1 / p) * (z #R p) is V22() real ext-real Element of REAL
(z #R p) / p is V22() real ext-real Element of REAL
diff (((1 / p) (#) (#R p)),z) is V22() real ext-real Element of REAL
diff ((#R p),z) is V22() real ext-real Element of REAL
(1 / p) * (diff ((#R p),z)) is V22() real ext-real Element of REAL
z #R (p - 1) is V22() real ext-real Element of REAL
p * (z #R (p - 1)) is V22() real ext-real Element of REAL
(1 / p) * (p * (z #R (p - 1))) is V22() real ext-real Element of REAL
(1 / p) * p is V22() real ext-real Element of REAL
((1 / p) * p) * (z #R (p - 1)) is V22() real ext-real Element of REAL
1 * (z #R (p - 1)) is V22() real ext-real Element of REAL
z is V22() real ext-real Element of REAL
((1 / p) (#) (#R p)) . z is V22() real ext-real Element of REAL
z #R p is V22() real ext-real Element of REAL
(z #R p) / p is V22() real ext-real Element of REAL
diff (((1 / p) (#) (#R p)),z) is V22() real ext-real Element of REAL
z #R (p - 1) is V22() real ext-real Element of REAL
ab is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ab is set
ab is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ab is set
- 1 is V22() real ext-real non positive Element of REAL
z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom z is set
x is set
[#] REAL is V49() V50() V72() V73() V74() Element of K19(REAL)
x is V22() real ext-real Element of REAL
z . x is V22() real ext-real Element of REAL
(1 / a) - x is V22() real ext-real Element of REAL
z /. x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
z . x is V22() real ext-real Element of REAL
(- 1) * x is V22() real ext-real Element of REAL
((- 1) * x) + (1 / a) is V22() real ext-real Element of REAL
(1 / a) - x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
diff (z,x) is V22() real ext-real Element of REAL
z `| (dom z) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(z `| (dom z)) . x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
z . x is V22() real ext-real Element of REAL
(1 / a) - x is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
diff (z,n) is V22() real ext-real Element of REAL
z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom z is set
z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom z is set
ab + z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (ab + z) is set
(right_open_halfline 0) /\ REAL is V72() V73() V74() Element of K19(REAL)
y is V22() real ext-real Element of REAL
(ab + z) . y is V22() real ext-real Element of REAL
y #R p is V22() real ext-real Element of REAL
(y #R p) / p is V22() real ext-real Element of REAL
((y #R p) / p) + (1 / a) is V22() real ext-real Element of REAL
(((y #R p) / p) + (1 / a)) - y is V22() real ext-real Element of REAL
diff ((ab + z),y) is V22() real ext-real Element of REAL
y #R (p - 1) is V22() real ext-real Element of REAL
(y #R (p - 1)) - 1 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 0 } is set
diff (ab,y) is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
ab . y is V22() real ext-real Element of REAL
z . y is V22() real ext-real Element of REAL
(ab . y) + (z . y) is V22() real ext-real Element of REAL
((y #R p) / p) + (z . y) is V22() real ext-real Element of REAL
(1 / a) - y is V22() real ext-real Element of REAL
((y #R p) / p) + ((1 / a) - y) is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
diff (z,y) is V22() real ext-real Element of REAL
(diff (ab,y)) + (diff (z,y)) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 0 } is set
(ab + z) . 1 is V22() real ext-real Element of REAL
1 #R p is V22() real ext-real Element of REAL
(1 #R p) / p is V22() real ext-real Element of REAL
((1 #R p) / p) + (1 / a) is V22() real ext-real Element of REAL
(((1 #R p) / p) + (1 / a)) - 1 is V22() real ext-real Element of REAL
((1 / p) + (1 / a)) - 1 is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
y #R p is V22() real ext-real Element of REAL
(y #R p) / p is V22() real ext-real Element of REAL
((y #R p) / p) + (1 / a) is V22() real ext-real Element of REAL
1 - y is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real Element of REAL
n is set
y + (1 - y) is V22() real ext-real Element of REAL
[.y,(y + (1 - y)).] is V49() V72() V73() V74() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( y <= b₁ & b₁ <= y + (1 - y) ) } is set
m is V22() real ext-real Element of REAL
(ab + z) | (right_open_halfline 0) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(ab + z) | [.y,(y + (1 - y)).] is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
].y,(y + (1 - y)).[ is V50() V72() V73() V74() Element of K19(REAL)
(ab + z) . (y + (1 - y)) is V22() real ext-real Element of REAL
(ab + z) . y is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
n * (1 - y) is V22() real ext-real Element of REAL
y + (n * (1 - y)) is V22() real ext-real Element of REAL
diff ((ab + z),(y + (n * (1 - y)))) is V22() real ext-real Element of REAL
(1 - y) * (diff ((ab + z),(y + (n * (1 - y))))) is V22() real ext-real Element of REAL
((ab + z) . y) + ((1 - y) * (diff ((ab + z),(y + (n * (1 - y)))))) is V22() real ext-real Element of REAL
1 * (1 - y) is V22() real ext-real Element of REAL
(y + (n * (1 - y))) to_power 0 is V22() real ext-real Element of REAL
(y + (n * (1 - y))) to_power (p - 1) is V22() real ext-real Element of REAL
(y + (n * (1 - y))) #R (p - 1) is V22() real ext-real Element of REAL
(y + (n * (1 - y))) #R 0 is V22() real ext-real Element of REAL
((y + (n * (1 - y))) #R (p - 1)) - 1 is V22() real ext-real Element of REAL
(1 - y) * 0 is V22() real ext-real Element of REAL
((ab + z) . y) + 0 is V22() real ext-real Element of REAL
(((y #R p) / p) + (1 / a)) - y is V22() real ext-real Element of REAL
((((y #R p) / p) + (1 / a)) - y) + y is V22() real ext-real Element of REAL
0 + y is V22() real ext-real Element of REAL
y - 1 is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real Element of REAL
n is set
1 + (y - 1) is V22() real ext-real Element of REAL
[.1,(1 + (y - 1)).] is V49() V72() V73() V74() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( 1 <= b₁ & b₁ <= 1 + (y - 1) ) } is set
m is V22() real ext-real Element of REAL
(ab + z) | (right_open_halfline 0) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(ab + z) | [.1,(1 + (y - 1)).] is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
].1,(1 + (y - 1)).[ is V50() V72() V73() V74() Element of K19(REAL)
(ab + z) . (1 + (y - 1)) is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
n * (y - 1) is V22() real ext-real Element of REAL
1 + (n * (y - 1)) is V22() real ext-real Element of REAL
diff ((ab + z),(1 + (n * (y - 1)))) is V22() real ext-real Element of REAL
(y - 1) * (diff ((ab + z),(1 + (n * (y - 1))))) is V22() real ext-real Element of REAL
((ab + z) . 1) + ((y - 1) * (diff ((ab + z),(1 + (n * (y - 1)))))) is V22() real ext-real Element of REAL
0 * (y - 1) is V22() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(1 + (n * (y - 1))) #R (p - 1) is V22() real ext-real Element of REAL
((1 + (n * (y - 1))) #R (p - 1)) - 1 is V22() real ext-real Element of REAL
(y - 1) * 0 is V22() real ext-real Element of REAL
(((y #R p) / p) + (1 / a)) - y is V22() real ext-real Element of REAL
((((y #R p) / p) + (1 / a)) - y) + y is V22() real ext-real Element of REAL
0 + y is V22() real ext-real Element of REAL
(1 - a) * p is V22() real ext-real Element of REAL
((1 - a) * p) + a is V22() real ext-real Element of REAL
(1 / a) * (ap #R a) is V22() real ext-real Element of REAL
((b #R p) / p) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
(b #R p) * (1 / p) is V22() real ext-real Element of REAL
((b #R p) * (1 / p)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
ap #R 0 is V22() real ext-real Element of REAL
(ap #R 0) / p is V22() real ext-real Element of REAL
(b #R p) * ((ap #R 0) / p) is V22() real ext-real Element of REAL
((b #R p) * ((ap #R 0) / p)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
ap #R ((1 - a) * p) is V22() real ext-real Element of REAL
(ap #R ((1 - a) * p)) * (ap #R a) is V22() real ext-real Element of REAL
((ap #R ((1 - a) * p)) * (ap #R a)) / p is V22() real ext-real Element of REAL
(b #R p) * (((ap #R ((1 - a) * p)) * (ap #R a)) / p) is V22() real ext-real Element of REAL
((b #R p) * (((ap #R ((1 - a) * p)) * (ap #R a)) / p)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
(ap #R ((1 - a) * p)) / p is V22() real ext-real Element of REAL
((ap #R ((1 - a) * p)) / p) * (ap #R a) is V22() real ext-real Element of REAL
(b #R p) * (((ap #R ((1 - a) * p)) / p) * (ap #R a)) is V22() real ext-real Element of REAL
((b #R p) * (((ap #R ((1 - a) * p)) / p) * (ap #R a))) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
(b #R p) * ((ap #R ((1 - a) * p)) / p) is V22() real ext-real Element of REAL
((b #R p) * ((ap #R ((1 - a) * p)) / p)) * (ap #R a) is V22() real ext-real Element of REAL
(((b #R p) * ((ap #R ((1 - a) * p)) / p)) * (ap #R a)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
(b #R p) * (ap #R ((1 - a) * p)) is V22() real ext-real Element of REAL
((b #R p) * (ap #R ((1 - a) * p))) / p is V22() real ext-real Element of REAL
(((b #R p) * (ap #R ((1 - a) * p))) / p) * (ap #R a) is V22() real ext-real Element of REAL
((((b #R p) * (ap #R ((1 - a) * p))) / p) * (ap #R a)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
(((b #R p) * (ap #R ((1 - a) * p))) / p) + (1 / a) is V22() real ext-real Element of REAL
((((b #R p) * (ap #R ((1 - a) * p))) / p) + (1 / a)) * (ap #R a) is V22() real ext-real Element of REAL
(ap #R (1 - a)) #R p is V22() real ext-real Element of REAL
(b #R p) * ((ap #R (1 - a)) #R p) is V22() real ext-real Element of REAL
((b #R p) * ((ap #R (1 - a)) #R p)) / p is V22() real ext-real Element of REAL
(((b #R p) * ((ap #R (1 - a)) #R p)) / p) + (1 / a) is V22() real ext-real Element of REAL
((((b #R p) * ((ap #R (1 - a)) #R p)) / p) + (1 / a)) * (ap #R a) is V22() real ext-real Element of REAL
(b * (ap #R (1 - a))) #R p is V22() real ext-real Element of REAL
((b * (ap #R (1 - a))) #R p) / p is V22() real ext-real Element of REAL
(((b * (ap #R (1 - a))) #R p) / p) + (1 / a) is V22() real ext-real Element of REAL
((((b * (ap #R (1 - a))) #R p) / p) + (1 / a)) * (ap #R a) is V22() real ext-real Element of REAL
(b * (ap #R (1 - a))) * (ap #R a) is V22() real ext-real Element of REAL
ap #R (((1 - a) * p) + a) is V22() real ext-real Element of REAL
(ap #R (((1 - a) * p) + a)) / p is V22() real ext-real Element of REAL
(b #R p) * ((ap #R (((1 - a) * p) + a)) / p) is V22() real ext-real Element of REAL
((b #R p) * ((ap #R (((1 - a) * p) + a)) / p)) + ((1 / a) * (ap #R a)) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
1 / p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
1 / a is V22() real ext-real Element of REAL
(1 / p) + (1 / a) is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
b to_power p is V22() real ext-real Element of REAL
(b to_power p) / p is V22() real ext-real Element of REAL
ap is V22() real ext-real Element of REAL
b * ap is V22() real ext-real Element of REAL
ap to_power a is V22() real ext-real Element of REAL
(ap to_power a) / a is V22() real ext-real Element of REAL
((b to_power p) / p) + ((ap to_power a) / a) is V22() real ext-real Element of REAL
bp is V22() real ext-real Element of REAL
1 - bp is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real Element of REAL
0 / p is V22() real ext-real Element of REAL
(0 / p) + ((ap to_power a) / a) is V22() real ext-real Element of REAL
0 * a is V22() real ext-real Element of REAL
((ap to_power a) / a) * a is V22() real ext-real Element of REAL
(ap to_power a) to_power (1 / a) is V22() real ext-real Element of REAL
a * (1 / a) is V22() real ext-real Element of REAL
ap to_power (a * (1 / a)) is V22() real ext-real Element of REAL
ap to_power 1 is V22() real ext-real Element of REAL
0 / a is V22() real ext-real Element of REAL
0 / a is V22() real ext-real Element of REAL
(0 / a) + ((b to_power p) / p) is V22() real ext-real Element of REAL
0 * p is V22() real ext-real Element of REAL
((b to_power p) / p) * p is V22() real ext-real Element of REAL
(b to_power p) to_power (1 / p) is V22() real ext-real Element of REAL
p * (1 / p) is V22() real ext-real Element of REAL
b to_power (p * (1 / p)) is V22() real ext-real Element of REAL
b to_power 1 is V22() real ext-real Element of REAL
0 / p is V22() real ext-real Element of REAL
b #R p is V22() real ext-real Element of REAL
(b #R p) / p is V22() real ext-real Element of REAL
ap #R a is V22() real ext-real Element of REAL
(ap #R a) / a is V22() real ext-real Element of REAL
((b #R p) / p) + ((ap #R a) / a) is V22() real ext-real Element of REAL
((b to_power p) / p) + ((ap #R a) / a) is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . a is V22() real ext-real Element of REAL
(Partial_Sums p) . a is V22() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . (a + 1) is V22() real ext-real Element of REAL
(Partial_Sums p) . (a + 1) is V22() real ext-real Element of REAL
((Partial_Sums p) . a) + (p . (a + 1)) is V22() real ext-real Element of REAL
(p . a) + (p . (a + 1)) is V22() real ext-real Element of REAL
0 + (p . (a + 1)) is V22() real ext-real Element of REAL
p . 0 is V22() real ext-real Element of REAL
(Partial_Sums p) . 0 is V22() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . a is V22() real ext-real Element of REAL
(Partial_Sums p) . a is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums p) . a is V22() real ext-real Element of REAL
p . a is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums p) . a is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums p) . b is V22() real ext-real Element of REAL
p . b is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . b is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums p is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums p) . a is V22() real ext-real Element of REAL
a + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums p) . (a + 1) is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . b is V22() real ext-real Element of REAL
p . (a + 1) is V22() real ext-real Element of REAL
((Partial_Sums p) . a) + (p . (a + 1)) is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . b is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . b is V22() real ext-real Element of REAL
(Partial_Sums p) . 0 is V22() real ext-real Element of REAL
p . 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
1 / p is V22() real ext-real Element of REAL
a is V22() real ext-real Element of REAL
1 / a is V22() real ext-real Element of REAL
(1 / p) + (1 / a) is V22() real ext-real Element of REAL
ab is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
z is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bp is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums x is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums ab is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums z is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums x) . y is V22() real ext-real Element of REAL
(Partial_Sums ab) . y is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums z) . y is V22() real ext-real Element of REAL
((Partial_Sums z) . y) to_power (1 / a) is V22() real ext-real Element of REAL
(((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)) is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
1 - b is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z . n is V22() real ext-real Element of REAL
bp . n is V22() real ext-real Element of REAL
abs (bp . n) is V22() real ext-real Element of REAL
(abs (bp . n)) to_power a is V22() real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab . m is V22() real ext-real Element of REAL
ap . m is V22() real ext-real Element of REAL
abs (ap . m) is V22() real ext-real Element of REAL
(abs (ap . m)) to_power p is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) * ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ap . D is V22() real ext-real Element of REAL
ab . D is V22() real ext-real Element of REAL
abs (ap . D) is V22() real ext-real Element of REAL
(abs (ap . D)) to_power p is V22() real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . D is V22() real ext-real Element of REAL
ap . D is V22() real ext-real Element of REAL
bp . D is V22() real ext-real Element of REAL
(ap . D) * (bp . D) is V22() real ext-real Element of REAL
abs ((ap . D) * (bp . D)) is V22() real ext-real Element of REAL
0 * (bp . D) is V22() real ext-real Element of REAL
abs (0 * (bp . D)) is V22() real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
bp . D is V22() real ext-real Element of REAL
z . D is V22() real ext-real Element of REAL
abs (bp . D) is V22() real ext-real Element of REAL
(abs (bp . D)) to_power a is V22() real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . D is V22() real ext-real Element of REAL
ap . D is V22() real ext-real Element of REAL
bp . D is V22() real ext-real Element of REAL
(ap . D) * (bp . D) is V22() real ext-real Element of REAL
abs ((ap . D) * (bp . D)) is V22() real ext-real Element of REAL
(ap . D) * 0 is V22() real ext-real Element of REAL
abs ((ap . D) * 0) is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) * ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
B is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
D . B is V22() real ext-real Element of REAL
bp . B is V22() real ext-real Element of REAL
abs (bp . B) is V22() real ext-real Element of REAL
(abs (bp . B)) / (((Partial_Sums z) . y) to_power (1 / a)) is V22() real ext-real Element of REAL
B is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a))) is V22() real ext-real Element of REAL
(1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) x is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
((1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) x) . n is V22() real ext-real Element of REAL
B . n is V22() real ext-real Element of REAL
D . n is V22() real ext-real Element of REAL
(B . n) * (D . n) is V22() real ext-real Element of REAL
ap . n is V22() real ext-real Element of REAL
abs (ap . n) is V22() real ext-real Element of REAL
(abs (ap . n)) / (((Partial_Sums ab) . y) to_power (1 / p)) is V22() real ext-real Element of REAL
bp . n is V22() real ext-real Element of REAL
abs (bp . n) is V22() real ext-real Element of REAL
(abs (bp . n)) / (((Partial_Sums z) . y) to_power (1 / a)) is V22() real ext-real Element of REAL
(abs (ap . n)) * (abs (bp . n)) is V22() real ext-real Element of REAL
((abs (ap . n)) * (abs (bp . n))) / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a))) is V22() real ext-real Element of REAL
(ap . n) * (bp . n) is V22() real ext-real Element of REAL
abs ((ap . n) * (bp . n)) is V22() real ext-real Element of REAL
(abs ((ap . n) * (bp . n))) / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a))) is V22() real ext-real Element of REAL
x . n is V22() real ext-real Element of REAL
(x . n) / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a))) is V22() real ext-real Element of REAL
(1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) * (x . n) is V22() real ext-real Element of REAL
Partial_Sums ((1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) x) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Partial_Sums ((1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) x)) . y is V22() real ext-real Element of REAL
(1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) (Partial_Sums x) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) (Partial_Sums x)) . y is V22() real ext-real Element of REAL
(1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) * ((Partial_Sums x) . y) is V22() real ext-real Element of REAL
1 / ((Partial_Sums ab) . y) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums ab) . y)) (#) ab is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 / ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums z) . y)) (#) z is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) + ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) + ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . n is V22() real ext-real Element of REAL
B . n is V22() real ext-real Element of REAL
(B . n) to_power p is V22() real ext-real Element of REAL
((B . n) to_power p) / p is V22() real ext-real Element of REAL
D . n is V22() real ext-real Element of REAL
(D . n) to_power a is V22() real ext-real Element of REAL
((D . n) to_power a) / a is V22() real ext-real Element of REAL
(((B . n) to_power p) / p) + (((D . n) to_power a) / a) is V22() real ext-real Element of REAL
ap . n is V22() real ext-real Element of REAL
abs (ap . n) is V22() real ext-real Element of REAL
(abs (ap . n)) / (((Partial_Sums ab) . y) to_power (1 / p)) is V22() real ext-real Element of REAL
((abs (ap . n)) / (((Partial_Sums ab) . y) to_power (1 / p))) to_power p is V22() real ext-real Element of REAL
(abs (ap . n)) to_power p is V22() real ext-real Element of REAL
(((Partial_Sums ab) . y) to_power (1 / p)) to_power p is V22() real ext-real Element of REAL
((abs (ap . n)) to_power p) / ((((Partial_Sums ab) . y) to_power (1 / p)) to_power p) is V22() real ext-real Element of REAL
0 / ((((Partial_Sums ab) . y) to_power (1 / p)) to_power p) is V22() real ext-real Element of REAL
bp . n is V22() real ext-real Element of REAL
abs (bp . n) is V22() real ext-real Element of REAL
(abs (bp . n)) / (((Partial_Sums z) . y) to_power (1 / a)) is V22() real ext-real Element of REAL
((abs (bp . n)) / (((Partial_Sums z) . y) to_power (1 / a))) to_power a is V22() real ext-real Element of REAL
(abs (bp . n)) to_power a is V22() real ext-real Element of REAL
(((Partial_Sums z) . y) to_power (1 / a)) to_power a is V22() real ext-real Element of REAL
((abs (bp . n)) to_power a) / ((((Partial_Sums z) . y) to_power (1 / a)) to_power a) is V22() real ext-real Element of REAL
0 / ((((Partial_Sums z) . y) to_power (1 / a)) to_power a) is V22() real ext-real Element of REAL
z . n is V22() real ext-real Element of REAL
(z . n) / ((((Partial_Sums z) . y) to_power (1 / a)) to_power a) is V22() real ext-real Element of REAL
((z . n) / ((((Partial_Sums z) . y) to_power (1 / a)) to_power a)) / a is V22() real ext-real Element of REAL
(1 / a) * a is V22() real ext-real Element of REAL
((Partial_Sums z) . y) to_power ((1 / a) * a) is V22() real ext-real Element of REAL
(z . n) / (((Partial_Sums z) . y) to_power ((1 / a) * a)) is V22() real ext-real Element of REAL
((z . n) / (((Partial_Sums z) . y) to_power ((1 / a) * a))) / a is V22() real ext-real Element of REAL
((Partial_Sums z) . y) to_power 1 is V22() real ext-real Element of REAL
(z . n) / (((Partial_Sums z) . y) to_power 1) is V22() real ext-real Element of REAL
((z . n) / (((Partial_Sums z) . y) to_power 1)) / a is V22() real ext-real Element of REAL
(z . n) / ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
((z . n) / ((Partial_Sums z) . y)) / a is V22() real ext-real Element of REAL
(1 / a) * ((z . n) / ((Partial_Sums z) . y)) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums z) . y)) * (z . n) is V22() real ext-real Element of REAL
(1 / a) * ((1 / ((Partial_Sums z) . y)) * (z . n)) is V22() real ext-real Element of REAL
((1 / ((Partial_Sums z) . y)) (#) z) . n is V22() real ext-real Element of REAL
(1 / a) * (((1 / ((Partial_Sums z) . y)) (#) z) . n) is V22() real ext-real Element of REAL
((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z)) . n is V22() real ext-real Element of REAL
ab . n is V22() real ext-real Element of REAL
(ab . n) / ((((Partial_Sums ab) . y) to_power (1 / p)) to_power p) is V22() real ext-real Element of REAL
((ab . n) / ((((Partial_Sums ab) . y) to_power (1 / p)) to_power p)) / p is V22() real ext-real Element of REAL
(1 / p) * p is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) to_power ((1 / p) * p) is V22() real ext-real Element of REAL
(ab . n) / (((Partial_Sums ab) . y) to_power ((1 / p) * p)) is V22() real ext-real Element of REAL
((ab . n) / (((Partial_Sums ab) . y) to_power ((1 / p) * p))) / p is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) to_power 1 is V22() real ext-real Element of REAL
(ab . n) / (((Partial_Sums ab) . y) to_power 1) is V22() real ext-real Element of REAL
((ab . n) / (((Partial_Sums ab) . y) to_power 1)) / p is V22() real ext-real Element of REAL
(ab . n) / ((Partial_Sums ab) . y) is V22() real ext-real Element of REAL
((ab . n) / ((Partial_Sums ab) . y)) / p is V22() real ext-real Element of REAL
(1 / p) * ((ab . n) / ((Partial_Sums ab) . y)) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums ab) . y)) * (ab . n) is V22() real ext-real Element of REAL
(1 / p) * ((1 / ((Partial_Sums ab) . y)) * (ab . n)) is V22() real ext-real Element of REAL
((1 / ((Partial_Sums ab) . y)) (#) ab) . n is V22() real ext-real Element of REAL
(1 / p) * (((1 / ((Partial_Sums ab) . y)) (#) ab) . n) is V22() real ext-real Element of REAL
((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) . n is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
B . n is V22() real ext-real Element of REAL
ap . n is V22() real ext-real Element of REAL
abs (ap . n) is V22() real ext-real Element of REAL
(abs (ap . n)) / (((Partial_Sums ab) . y) to_power (1 / p)) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
B . n is V22() real ext-real Element of REAL
D . n is V22() real ext-real Element of REAL
(B . n) * (D . n) is V22() real ext-real Element of REAL
(B . n) to_power p is V22() real ext-real Element of REAL
((B . n) to_power p) / p is V22() real ext-real Element of REAL
(D . n) to_power a is V22() real ext-real Element of REAL
((D . n) to_power a) / a is V22() real ext-real Element of REAL
(((B . n) to_power p) / p) + (((D . n) to_power a) / a) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
((1 / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a)))) (#) x) . n is V22() real ext-real Element of REAL
(((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) + ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . n is V22() real ext-real Element of REAL
B . n is V22() real ext-real Element of REAL
D . n is V22() real ext-real Element of REAL
(B . n) * (D . n) is V22() real ext-real Element of REAL
(B . n) to_power p is V22() real ext-real Element of REAL
((B . n) to_power p) / p is V22() real ext-real Element of REAL
(D . n) to_power a is V22() real ext-real Element of REAL
((D . n) to_power a) / a is V22() real ext-real Element of REAL
(((B . n) to_power p) / p) + (((D . n) to_power a) / a) is V22() real ext-real Element of REAL
Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) + ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) + ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z)))) . y is V22() real ext-real Element of REAL
Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab))) + (Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab))) + (Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z)))) . y is V22() real ext-real Element of REAL
(Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab))) . y is V22() real ext-real Element of REAL
(Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y is V22() real ext-real Element of REAL
((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ab) . y)) (#) ab))) . y) + ((Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(1 / p) (#) (Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / p) (#) (Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab))) . y is V22() real ext-real Element of REAL
(((1 / p) (#) (Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab))) . y) + ((Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
(Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab)) . y is V22() real ext-real Element of REAL
(1 / p) * ((Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab)) . y) is V22() real ext-real Element of REAL
((1 / p) * ((Partial_Sums ((1 / ((Partial_Sums ab) . y)) (#) ab)) . y)) + ((Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums ab) . y)) (#) (Partial_Sums ab) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / ((Partial_Sums ab) . y)) (#) (Partial_Sums ab)) . y is V22() real ext-real Element of REAL
(1 / p) * (((1 / ((Partial_Sums ab) . y)) (#) (Partial_Sums ab)) . y) is V22() real ext-real Element of REAL
((1 / p) * (((1 / ((Partial_Sums ab) . y)) (#) (Partial_Sums ab)) . y)) + ((Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y) is V22() real ext-real Element of REAL
(1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y)) is V22() real ext-real Element of REAL
((1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y))) + ((Partial_Sums ((1 / a) (#) ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(1 / a) (#) (Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / a) (#) (Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z))) . y is V22() real ext-real Element of REAL
((1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y))) + (((1 / a) (#) (Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z))) . y) is V22() real ext-real Element of REAL
(Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z)) . y is V22() real ext-real Element of REAL
(1 / a) * ((Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z)) . y) is V22() real ext-real Element of REAL
((1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y))) + ((1 / a) * ((Partial_Sums ((1 / ((Partial_Sums z) . y)) (#) z)) . y)) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums z) . y)) (#) (Partial_Sums z) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / ((Partial_Sums z) . y)) (#) (Partial_Sums z)) . y is V22() real ext-real Element of REAL
(1 / a) * (((1 / ((Partial_Sums z) . y)) (#) (Partial_Sums z)) . y) is V22() real ext-real Element of REAL
((1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y))) + ((1 / a) * (((1 / ((Partial_Sums z) . y)) (#) (Partial_Sums z)) . y)) is V22() real ext-real Element of REAL
(1 / ((Partial_Sums z) . y)) * ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
(1 / a) * ((1 / ((Partial_Sums z) . y)) * ((Partial_Sums z) . y)) is V22() real ext-real Element of REAL
((1 / p) * ((1 / ((Partial_Sums ab) . y)) * ((Partial_Sums ab) . y))) + ((1 / a) * ((1 / ((Partial_Sums z) . y)) * ((Partial_Sums z) . y))) is V22() real ext-real Element of REAL
(1 / p) * 1 is V22() real ext-real Element of REAL
((1 / p) * 1) + ((1 / a) * ((1 / ((Partial_Sums z) . y)) * ((Partial_Sums z) . y))) is V22() real ext-real Element of REAL
(1 / a) * 1 is V22() real ext-real Element of REAL
((1 / p) * 1) + ((1 / a) * 1) is V22() real ext-real Element of REAL
((Partial_Sums x) . y) / ((((Partial_Sums ab) . y) to_power (1 / p)) * (((Partial_Sums z) . y) to_power (1 / a))) is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) * ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
((Partial_Sums ab) . y) * ((Partial_Sums z) . y) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
1 / p is V22() real ext-real Element of REAL
ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
a is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bp is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
ab is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums ab is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums bp is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ap . z is V22() real ext-real Element of REAL
a . z is V22() real ext-real Element of REAL
abs (a . z) is V22() real ext-real Element of REAL
(abs (a . z)) to_power p is V22() real ext-real Element of REAL
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
bp . z is V22() real ext-real Element of REAL
b . z is V22() real ext-real Element of REAL
abs (b . z) is V22() real ext-real Element of REAL
(abs (b . z)) to_power p is V22() real ext-real Element of REAL
p - 1 is V22() real ext-real Element of REAL
z is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 - 1 is V22() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z . x is V22() real ext-real Element of REAL
a . x is V22() real ext-real Element of REAL
b . x is V22() real ext-real Element of REAL
(a . x) + (b . x) is V22() real ext-real Element of REAL
abs ((a . x) + (b . x)) is V22() real ext-real Element of REAL
(abs ((a . x) + (b . x))) to_power (p - 1) is V22() real ext-real Element of REAL
abs b is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
z (#) (abs b) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(z (#) (abs b)) . x is V22() real ext-real Element of REAL
b . x is V22() real ext-real Element of REAL
z . x is V22() real ext-real Element of REAL
(b . x) * (z . x) is V22() real ext-real Element of REAL
abs ((b . x) * (z . x)) is V22() real ext-real Element of REAL
abs (z . x) is V22() real ext-real Element of REAL
(abs b) . x is V22() real ext-real Element of REAL
(z . x) * ((abs b) . x) is V22() real ext-real Element of REAL
abs (b . x) is V22() real ext-real Element of REAL
(z . x) * (abs (b . x)) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
1 - x is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
1 / y is V22() real ext-real Element of REAL
n is V22() real ext-real Element of REAL
1 / n is V22() real ext-real Element of REAL
(1 / p) + (1 / n) is V22() real ext-real Element of REAL
1 * n is V22() real ext-real Element of REAL
1 * p is V22() real ext-real Element of REAL
(1 * n) + (1 * p) is V22() real ext-real Element of REAL
p * n is V22() real ext-real Element of REAL
((1 * n) + (1 * p)) / (p * n) is V22() real ext-real Element of REAL
(((1 * n) + (1 * p)) / (p * n)) * (p * n) is V22() real ext-real Element of REAL
1 * (p * n) is V22() real ext-real Element of REAL
n + p is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab . n is V22() real ext-real Element of REAL
z . n is V22() real ext-real Element of REAL
a . n is V22() real ext-real Element of REAL
b . n is V22() real ext-real Element of REAL
(a . n) + (b . n) is V22() real ext-real Element of REAL
abs ((a . n) + (b . n)) is V22() real ext-real Element of REAL
(z . n) * (abs ((a . n) + (b . n))) is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power p is V22() real ext-real Element of REAL
(p - 1) + 1 is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power ((p - 1) + 1) is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power (p - 1) is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power 1 is V22() real ext-real Element of REAL
((abs ((a . n) + (b . n))) to_power (p - 1)) * ((abs ((a . n) + (b . n))) to_power 1) is V22() real ext-real Element of REAL
((abs ((a . n) + (b . n))) to_power (p - 1)) * (abs ((a . n) + (b . n))) is V22() real ext-real Element of REAL
abs a is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
z (#) (abs a) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(z (#) (abs a)) + (z (#) (abs b)) is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of