:: 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 NAT
ab . n is V22() real ext-real Element of REAL
((z (#) (abs a)) + (z (#) (abs b))) . 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
abs (a . n) is V22() real ext-real Element of REAL
b . n is V22() real ext-real Element of REAL
abs (b . n) is V22() real ext-real Element of REAL
(abs (a . n)) + (abs (b . n)) is V22() real ext-real Element of REAL
(z . n) * ((abs (a . n)) + (abs (b . n))) is V22() real ext-real Element of REAL
(z . n) * (abs (a . n)) is V22() real ext-real Element of REAL
(z . n) * (abs (b . n)) is V22() real ext-real Element of REAL
((z . n) * (abs (a . n))) + ((z . n) * (abs (b . n))) is V22() real ext-real Element of REAL
(abs a) . n is V22() real ext-real Element of REAL
(z . n) * ((abs a) . n) is V22() real ext-real Element of REAL
((z . n) * ((abs a) . n)) + ((z . n) * (abs (b . n))) is V22() real ext-real Element of REAL
(abs b) . n is V22() real ext-real Element of REAL
(z . n) * ((abs b) . n) is V22() real ext-real Element of REAL
((z . n) * ((abs a) . n)) + ((z . n) * ((abs b) . n)) is V22() real ext-real Element of REAL
(z (#) (abs a)) . n is V22() real ext-real Element of REAL
((z (#) (abs a)) . n) + ((z . n) * ((abs b) . n)) is V22() real ext-real Element of REAL
(z (#) (abs b)) . n is V22() real ext-real Element of REAL
((z (#) (abs a)) . n) + ((z (#) (abs 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
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
abs (z . n) is V22() real ext-real Element of REAL
(abs (z . n)) to_power n is V22() real ext-real Element of REAL
ab . 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
(abs ((a . n) + (b . n))) to_power (p - 1) is V22() real ext-real Element of REAL
((abs ((a . n) + (b . n))) to_power (p - 1)) to_power n is V22() real ext-real Element of REAL
0 to_power p is V22() real ext-real Element of REAL
0 to_power n is V22() real ext-real Element of REAL
(p - 1) * n is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power ((p - 1) * 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
(z (#) (abs a)) . n is V22() real ext-real Element of REAL
a . n is V22() real ext-real Element of REAL
z . n is V22() real ext-real Element of REAL
(a . n) * (z . n) is V22() real ext-real Element of REAL
abs ((a . n) * (z . n)) is V22() real ext-real Element of REAL
abs (z . n) is V22() real ext-real Element of REAL
(abs a) . n is V22() real ext-real Element of REAL
(z . n) * ((abs a) . n) is V22() real ext-real Element of REAL
abs (a . n) is V22() real ext-real Element of REAL
(z . n) * (abs (a . 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
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
(Partial_Sums ap) . n is V22() real ext-real Element of REAL
((Partial_Sums ap) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
((Partial_Sums bp) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / n) is V22() real ext-real Element of REAL
((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
Partial_Sums ((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))
(Partial_Sums ((z (#) (abs a)) + (z (#) (abs b)))) . n is V22() real ext-real Element of REAL
Partial_Sums (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))
Partial_Sums (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))
(Partial_Sums (z (#) (abs a))) + (Partial_Sums (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))
((Partial_Sums (z (#) (abs a))) + (Partial_Sums (z (#) (abs b)))) . n is V22() real ext-real Element of REAL
(Partial_Sums (z (#) (abs a))) . n is V22() real ext-real Element of REAL
(Partial_Sums (z (#) (abs b))) . n is V22() real ext-real Element of REAL
((Partial_Sums (z (#) (abs a))) . n) + ((Partial_Sums (z (#) (abs b))) . n) is V22() real ext-real Element of REAL
(((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
(((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / n))) + ((((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / 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
ab . 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
0 to_power p is V22() real ext-real Element of REAL
(abs ((a . n) + (b . n))) to_power 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
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
(Partial_Sums ap) . n is V22() real ext-real Element of REAL
((Partial_Sums ap) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
((Partial_Sums bp) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / n) is V22() real ext-real Element of REAL
0 to_power (1 / p) is V22() real ext-real Element of REAL
0 + 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
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
1 / (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
(((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / n))) * (1 / (((Partial_Sums ab) . n) to_power (1 / n))) is V22() real ext-real Element of REAL
(((Partial_Sums ab) . n) to_power (1 / n)) * (1 / (((Partial_Sums ab) . n) to_power (1 / n))) is V22() real ext-real Element of REAL
((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * ((((Partial_Sums ab) . n) to_power (1 / n)) * (1 / (((Partial_Sums ab) . n) to_power (1 / n)))) is V22() real ext-real Element of REAL
((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * 1 is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) * (1 / (((Partial_Sums ab) . n) to_power (1 / n))) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) / (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power 1 is V22() real ext-real Element of REAL
(((Partial_Sums ab) . n) to_power 1) / (((Partial_Sums ab) . n) to_power (1 / n)) is V22() real ext-real Element of REAL
1 - (1 / n) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 - (1 / n)) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) 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
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums ap) . n is V22() real ext-real Element of REAL
((Partial_Sums ap) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
((Partial_Sums bp) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) 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))
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))
lim p is V22() real ext-real Element of REAL
lim a is V22() real ext-real Element of REAL
b is V22() real ext-real set
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . ap is V22() real ext-real Element of REAL
a . ap is V22() real ext-real Element of REAL
b + 1 is V22() real ext-real Element of REAL
(p . ap) + 0 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))
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))
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))
lim p is V22() real ext-real Element of REAL
lim a is V22() real ext-real Element of REAL
lim b is V22() real ext-real Element of REAL
(lim a) + (lim b) is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
p . ap is V22() real ext-real Element of REAL
a . ap is V22() real ext-real Element of REAL
b . ap is V22() real ext-real Element of REAL
(a . ap) + (b . ap) is V22() real ext-real Element of REAL
a + 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))
(a + b) . ap is V22() real ext-real Element of REAL
lim (a + b) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of 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))
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))
lim b is V22() real ext-real Element of REAL
lim a is V22() real ext-real Element of REAL
(lim a) to_power p is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a ^\ ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of a
bp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(a ^\ ap) . bp is V22() real ext-real Element of REAL
bp + ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . (bp + ap) is V22() real ext-real Element of REAL
bp is V22() real ext-real set
ab 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
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
b ^\ ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of b
(b ^\ ap) . z is V22() real ext-real Element of REAL
z + ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
b . (z + ap) is V22() real ext-real Element of REAL
a . (z + ap) is V22() real ext-real Element of REAL
(a . (z + ap)) to_power p is V22() real ext-real Element of REAL
(a ^\ ap) . z is V22() real ext-real Element of REAL
((a ^\ ap) . z) to_power p is V22() real ext-real Element of REAL
0 to_power p is V22() real ext-real Element of REAL
((b ^\ ap) . z) - ((lim a) to_power p) is V22() real ext-real Element of REAL
abs (((b ^\ ap) . z) - ((lim a) to_power p)) is V22() real ext-real Element of REAL
lim (b ^\ ap) is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . ap is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real set
a . ap is V22() real ext-real Element of REAL
ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . z 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
a . x is V22() real ext-real Element of REAL
ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . x is V22() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real set
a . x is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . 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
a . n is V22() real ext-real Element of REAL
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(NAT,NAT)) is set
bp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab is Relation-like NAT -defined NAT -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
ab . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
rng ab is V72() V73() V74() V75() V76() V77() set
dom ab is V72() V73() V74() V75() V76() V77() set
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))
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
rng z is V72() V73() V74() set
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
x + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z . (x + 1) is V22() real ext-real Element of REAL
x is Relation-like NAT -defined NAT -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . y is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real set
a . y is V22() real ext-real Element of REAL
a . bp is V22() real ext-real Element of REAL
x . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real set
a . 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
x . n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real set
a . 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
a . n 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
x . m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . l is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . (n + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . (x . (n + 1)) 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
x . m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a * x is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of a
lim (a * x) is V22() real ext-real Element of REAL
y is V22() real ext-real set
1 / p is V22() real ext-real Element of REAL
y to_power (1 / p) is V22() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . m is V22() real ext-real Element of REAL
b . m is V22() real ext-real Element of REAL
0 to_power p is V22() real ext-real Element of REAL
(b . m) - ((lim a) to_power p) is V22() real ext-real Element of REAL
abs ((b . m) - ((lim a) to_power p)) is V22() real ext-real Element of REAL
a . m is V22() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
x . l is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(a * x) . l is V22() real ext-real Element of REAL
((a * x) . l) - 0 is V22() real ext-real Element of REAL
abs (((a * x) . l) - 0) is V22() real ext-real Element of REAL
a . (x . l) is V22() real ext-real Element of REAL
abs (a . (x . l)) is V22() real ext-real Element of REAL
(a . m) to_power p is V22() real ext-real Element of REAL
b . m is V22() real ext-real Element of REAL
abs (a . m) is V22() real ext-real Element of REAL
(y to_power (1 / p)) to_power p is V22() real ext-real set
(abs (a . m)) to_power p is V22() real ext-real Element of REAL
(1 / p) * p is V22() real ext-real Element of REAL
y to_power ((1 / p) * p) is V22() real ext-real set
y to_power 1 is V22() real ext-real set
(b . m) - ((lim a) to_power p) is V22() real ext-real Element of REAL
abs ((b . m) - ((lim a) to_power p)) is V22() real ext-real Element of REAL
a . m is V22() real ext-real Element of REAL
b . m is V22() real ext-real Element of REAL
(b . m) - ((lim a) to_power p) is V22() real ext-real Element of REAL
abs ((b . m) - ((lim a) to_power p)) is V22() real ext-real Element of REAL
a . m is V22() real ext-real Element of REAL
b . m is V22() real ext-real Element of REAL
(b . m) - ((lim a) to_power p) is V22() real ext-real Element of REAL
abs ((b . m) - ((lim a) to_power p)) is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
#R p is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (#R p) is set
(lim a) / 2 is V22() real ext-real Element of REAL
bp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a ^\ bp is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of a
rng (a ^\ bp) is V72() V73() V74() set
ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
bp + ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . (bp + ab) is V22() real ext-real Element of REAL
(a . (bp + ab)) - (lim a) is V22() real ext-real Element of REAL
abs ((a . (bp + ab)) - (lim a)) is V22() real ext-real Element of REAL
- ((lim a) / 2) is V22() real ext-real Element of REAL
(- ((lim a) / 2)) + (lim a) is V22() real ext-real Element of REAL
((a . (bp + ab)) - (lim a)) + (lim a) is V22() real ext-real Element of REAL
(a ^\ bp) . ab is V22() real ext-real Element of REAL
ab is set
z is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(a ^\ bp) . 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
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a ^\ ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of a
rng (a ^\ ap) is V72() V73() V74() set
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a ^\ ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of a
rng (a ^\ ap) is V72() V73() V74() set
bp is set
ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(a ^\ ap) . ab is V22() real ext-real Element of REAL
ap + ab is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
a . (ap + ab) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= 0 } is set
(#R p) /* (a ^\ 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))
((#R p) /* (a ^\ ap)) . bp is V22() real ext-real Element of REAL
(#R p) . ((a ^\ ap) . ab) is V22() real ext-real Element of REAL
((a ^\ ap) . ab) #R p is V22() real ext-real Element of REAL
(a . (ap + ab)) #R p is V22() real ext-real Element of REAL
(a . (ap + ab)) to_power p is V22() real ext-real Element of REAL
b . (ap + ab) is V22() real ext-real Element of REAL
b ^\ ap is Relation-like NAT -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of b
(b ^\ ap) . bp is V22() real ext-real Element of REAL
z is V22() real ext-real Element of REAL
lim (a ^\ ap) is V22() real ext-real Element of REAL
(#R p) . (lim (a ^\ ap)) is V22() real ext-real Element of REAL
lim ((#R p) /* (a ^\ ap)) is V22() real ext-real Element of REAL
(lim a) #R p is V22() real ext-real Element of REAL
p is V22() real ext-real Element of 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))
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))
Partial_Sums 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))
lim b is V22() real ext-real Element of REAL
Sum a is V22() real ext-real Element of REAL
(Sum a) to_power p is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums a) . ap is V22() real ext-real Element of REAL
lim (Partial_Sums a) is V22() real ext-real Element of REAL
(lim (Partial_Sums a)) to_power p is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
bp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums a) . ap is V22() real ext-real Element of REAL
(Partial_Sums a) . bp is V22() real ext-real Element of REAL
b . ap is V22() real ext-real Element of REAL
((Partial_Sums a) . ap) to_power p is V22() real ext-real Element of REAL
b . bp is V22() real ext-real Element of REAL
((Partial_Sums a) . bp) to_power p is V22() real ext-real Element of REAL
ap is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
b . ap 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
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))
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))
Sum z is V22() real ext-real Element of REAL
Sum bp is V22() real ext-real Element of REAL
(Sum bp) to_power (1 / p) is V22() real ext-real Element of REAL
Sum ab is V22() real ext-real Element of REAL
(Sum ab) to_power (1 / a) is V22() real ext-real Element of REAL
((Sum bp) to_power (1 / p)) * ((Sum ab) to_power (1 / a)) is V22() real ext-real Element of 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))
x is V22() real ext-real Element of REAL
1 - x is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab . y is V22() real ext-real Element of REAL
ap . y is V22() real ext-real Element of REAL
abs (ap . y) is V22() real ext-real Element of REAL
(abs (ap . y)) to_power a is V22() real ext-real Element of 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))
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 ab) . y is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
z . y is V22() real ext-real Element of REAL
b . y is V22() real ext-real Element of REAL
ap . y is V22() real ext-real Element of REAL
(b . y) * (ap . y) is V22() real ext-real Element of REAL
abs ((b . y) * (ap . y)) is V22() real ext-real Element of 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 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
bp . n is V22() real ext-real Element of REAL
b . n is V22() real ext-real Element of REAL
abs (b . n) is V22() real ext-real Element of REAL
(abs (b . n)) to_power 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
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
n 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 (#) y 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
(Partial_Sums z) . n is V22() real ext-real Element of REAL
(n (#) y) . n is V22() real ext-real Element of REAL
y . n is V22() real ext-real Element of REAL
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / a) is V22() real ext-real Element of REAL
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
((Partial_Sums bp) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / a)) is V22() real ext-real Element of REAL
n . n is V22() real ext-real Element of REAL
lim (Partial_Sums z) is V22() real ext-real Element of REAL
lim (n (#) y) is V22() real ext-real Element of REAL
lim (Partial_Sums bp) is V22() real ext-real Element of REAL
lim n is V22() real ext-real Element of REAL
lim (Partial_Sums ab) is V22() real ext-real Element of REAL
lim 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))
Sum ab is V22() real ext-real Element of REAL
(Sum ab) to_power (1 / p) is V22() real ext-real Element of REAL
Sum ap is V22() real ext-real Element of REAL
(Sum ap) to_power (1 / p) is V22() real ext-real Element of REAL
Sum bp is V22() real ext-real Element of REAL
(Sum bp) to_power (1 / p) is V22() real ext-real Element of REAL
((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) is V22() real ext-real Element of 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))
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))
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ab . 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 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
(Partial_Sums ab) . x is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) 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
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 ab) . x 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 ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) 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
y 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
(Partial_Sums ab) . x is V22() real ext-real Element of REAL
((Partial_Sums ab) . x) to_power (1 / p) is V22() real ext-real Element of REAL
z . 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
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
ap . x is V22() real ext-real Element of REAL
a . x is V22() real ext-real Element of REAL
abs (a . x) is V22() real ext-real Element of REAL
(abs (a . x)) to_power p is V22() real ext-real Element of 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))
x is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
(Partial_Sums ap) . x is V22() real ext-real Element of 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))
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() Element of NAT
bp . y is V22() real ext-real Element of REAL
b . y is V22() real ext-real Element of REAL
abs (b . y) is V22() real ext-real Element of REAL
(abs (b . y)) to_power p is V22() real ext-real Element of 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))
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 bp) . y is V22() real ext-real Element of REAL
y 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
z . n is V22() real ext-real Element of REAL
x . n is V22() real ext-real Element of REAL
y . n is V22() real ext-real Element of REAL
(x . n) + (y . n) is V22() real ext-real Element of REAL
(Partial_Sums bp) . n is V22() real ext-real Element of REAL
((Partial_Sums bp) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(Partial_Sums ap) . n is V22() real ext-real Element of REAL
((Partial_Sums ap) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) 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
z . n is V22() real ext-real Element of REAL
(z . n) to_power p is V22() real ext-real Element of REAL
(Partial_Sums ab) . n is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power (1 / p) is V22() real ext-real Element of REAL
(1 / p) * p is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power ((1 / p) * p) is V22() real ext-real Element of REAL
((Partial_Sums ab) . n) to_power 1 is V22() real ext-real Element of REAL
lim (Partial_Sums ab) is V22() real ext-real Element of REAL
lim z is V22() real ext-real Element of REAL
(lim z) to_power p is V22() real ext-real Element of REAL
0 to_power (1 / p) is V22() real ext-real Element of REAL
(1 / p) * p is V22() real ext-real Element of REAL
(lim z) to_power ((1 / p) * p) is V22() real ext-real Element of REAL
(lim z) to_power 1 is V22() real ext-real Element of REAL
lim (Partial_Sums bp) is V22() real ext-real Element of REAL
lim y is V22() real ext-real Element of REAL
lim (Partial_Sums ap) is V22() real ext-real Element of REAL
lim x is V22() real ext-real Element of REAL