:: HOLDER_1 semantic presentation

begin

registration
let x be ( ( real ) ( V22() real ext-real ) number ) ;
cluster right_closed_halfline x : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V49() V72() V73() V74() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -> non empty ;
end;

theorem :: HOLDER_1:1
for p, q being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < q : ( ( ) ( V22() real ext-real ) Real) holds
for a being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( ) ( V22() real ext-real ) Real) holds
(a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) * (a : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = a : ( ( ) ( V22() real ext-real ) Real) to_power (p : ( ( ) ( V22() real ext-real ) Real) + q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ;

theorem :: HOLDER_1:2
for p, q being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < q : ( ( ) ( V22() real ext-real ) Real) holds
for a being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( ) ( V22() real ext-real ) Real) holds
(a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = a : ( ( ) ( V22() real ext-real ) Real) to_power (p : ( ( ) ( V22() real ext-real ) Real) * q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ;

theorem :: HOLDER_1:3
for p being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( ) ( V22() real ext-real ) Real) & a : ( ( ) ( V22() real ext-real ) Real) <= b : ( ( ) ( V22() real ext-real ) Real) holds
a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= b : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ;

theorem :: HOLDER_1:4
for p, q, a, b being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < a : ( ( ) ( V22() real ext-real ) Real) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < b : ( ( ) ( V22() real ext-real ) Real) holds
( a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= ((a : ( ( ) ( V22() real ext-real ) Real) #R p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) #R q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ( a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = ((a : ( ( ) ( V22() real ext-real ) Real) #R p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) #R q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) implies a : ( ( ) ( V22() real ext-real ) Real) #R p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = b : ( ( ) ( V22() real ext-real ) Real) #R q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & ( a : ( ( ) ( V22() real ext-real ) Real) #R p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = b : ( ( ) ( V22() real ext-real ) Real) #R q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) implies a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = ((a : ( ( ) ( V22() real ext-real ) Real) #R p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) #R q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) ;

theorem :: HOLDER_1:5
for p, q, a, b being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( ) ( V22() real ext-real ) Real) & 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= b : ( ( ) ( V22() real ext-real ) Real) holds
( a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= ((a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ( a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = ((a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) implies a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = b : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & ( a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = b : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) implies a : ( ( ) ( V22() real ext-real ) Real) * b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = ((a : ( ( ) ( V22() real ext-real ) Real) to_power p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((b : ( ( ) ( V22() real ext-real ) Real) to_power q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) ;

begin

theorem :: HOLDER_1:6
for p, q being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for a, b, ap, bq, ab being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & bq : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = abs ((a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) * (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) holds
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= (((Partial_Sums ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) * (((Partial_Sums bq : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ;

theorem :: HOLDER_1:7
for p being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) holds
for a, b, ap, bp, ab being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & bp : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs ((a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) holds
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds ((Partial_Sums ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= (((Partial_Sums ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (((Partial_Sums bp : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ;

theorem :: HOLDER_1:8
for a, b being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is V41() holds
( a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= lim b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ;

theorem :: HOLDER_1:9
for a, b, c being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (c : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & c : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is V41() holds
( a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= (lim b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (lim c : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ;

theorem :: HOLDER_1:10
for p being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) holds
for a, ap being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (lim a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ;

theorem :: HOLDER_1:11
for p being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) holds
for a, ap being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds 0 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = ((Partial_Sums a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (Sum a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is V41() & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= (Sum a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) ;

theorem :: HOLDER_1:12
for p, q being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) & (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
for a, b, ap, bq, ab being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & bq : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power q : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = abs ((a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) * (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) & ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable & bq : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable holds
( ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable & Sum ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= ((Sum ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) * ((Sum bq : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / q : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ;

theorem :: HOLDER_1:13
for p being ( ( ) ( V22() real ext-real ) Real) st 1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) < p : ( ( ) ( V22() real ext-real ) Real) holds
for a, b, ap, bp, ab being ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & bp : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) & ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) = (abs ((a : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + (b : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V33() V66() V72() V73() V74() V75() V76() V77() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ) & ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable & bp : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable holds
( ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is summable & (Sum ab : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) <= ((Sum ap : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) + ((Sum bp : ( ( V6() quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) to_power (1 : ( ( ) ( 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 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V72() V73() V74() V75() V76() V77() V78() ) Element of K19(REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( ) set ) ) ) / p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V67() V72() V73() V74() V78() ) set ) ) ) ;