:: SERIES_5 semantic presentation

begin

theorem :: SERIES_5:1
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:2
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) >= ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:3
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) < b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) < (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:4
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) < b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) < sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:5
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) < b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) < (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:6
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) < b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) < (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:7
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:8
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:9
for x, y being ( ( real ) ( V11() real ext-real ) number ) holds x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) <= sqrt (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:10
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:11
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( real ) ( V11() real ext-real ) set ) <= sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:12
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:13
for x, y being ( ( real ) ( V11() real ext-real ) number ) st abs x : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) & abs y : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
abs ((x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) / (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) <= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:14
for x, y being ( ( real ) ( V11() real ext-real ) number ) holds (abs (x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) / (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (abs (x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= ((abs x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) / (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (abs x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + ((abs y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) / (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (abs y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:15
for a, b, d, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:16
for a, b, d, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) < 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:17
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) > c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) & b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) > a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) & a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) > b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) >= 9 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:18
for a, b, c, d being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds sqrt ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( real ) ( V11() real ext-real ) set ) >= (sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) + (sqrt (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:19
for a, b, c, d being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= (((4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ;

theorem :: SERIES_5:20
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) >= 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:21
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= sqrt 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SERIES_5:22
for b, c, a being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds ((((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) - c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) >= 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:23
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= ((sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (sqrt (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:24
for b, c, a being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) >= (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ;

theorem :: SERIES_5:25
for x, y, z being ( ( real ) ( V11() real ext-real ) number ) st x : ( ( real ) ( V11() real ext-real ) number ) > y : ( ( real ) ( V11() real ext-real ) number ) & y : ( ( real ) ( V11() real ext-real ) number ) > z : ( ( real ) ( V11() real ext-real ) number ) holds
(((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + ((y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) * z : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + ((z : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) > ((x : ( ( real ) ( V11() real ext-real ) number ) * (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) * (z : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) * (x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:26
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) & b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) - b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) > c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) - c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:27
for b, a, c, d being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) & c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) > d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) / (d : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:28
for m, x, z, y being ( ( real ) ( V11() real ext-real ) number ) holds (m : ( ( real ) ( V11() real ext-real ) number ) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) <= (sqrt ((m : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) * (sqrt ((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:29
for m, x, u, y, w, z being ( ( real ) ( V11() real ext-real ) number ) holds (((m : ( ( real ) ( V11() real ext-real ) number ) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (u : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (w : ( ( real ) ( V11() real ext-real ) number ) * z : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ^2 : ( ( ) ( V11() real ext-real ) set ) <= (((m : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (u : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (w : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:30
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (((9 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) <= (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ;

theorem :: SERIES_5:31
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) <= ((sqrt ((((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) + (sqrt ((((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (sqrt ((((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:32
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds ((sqrt ((((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) + (sqrt ((((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (sqrt ((((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) <= ((sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) + (sqrt (((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (sqrt (((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:33
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds ((sqrt (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) + (sqrt (((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (sqrt (((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) <= sqrt (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:34
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds sqrt (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) set ) <= (((b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + ((c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:35
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) * ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) >= 9 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:36
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= 17 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:37
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) >= 9 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:38
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) * ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) >= 8 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:39
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) >= 64 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:40
for x, y, z being ( ( real ) ( V11() real ext-real ) number ) st (x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + z : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((x : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:41
for x, y, z being ( ( real ) ( V11() real ext-real ) number ) st (x : ( ( real ) ( V11() real ext-real ) number ) + y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + z : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((x : ( ( real ) ( V11() real ext-real ) number ) * y : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (y : ( ( real ) ( V11() real ext-real ) number ) * z : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) + (z : ( ( real ) ( V11() real ext-real ) number ) * x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) <= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;

theorem :: SERIES_5:42
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) & b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) > c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) holds
((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) * (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) > ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) * (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * (c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) to_power (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) + b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:43
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) >= ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) * b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) + (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) * (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:44
for a, b, c being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st (a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) = c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) < c : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:45
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) < (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:46
for a, b being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number )
for n, k being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) & k : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ k : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ k : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) * ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) <= 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * ((a : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (k : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) + (b : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) |^ (k : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:47
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (sqrt (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (sqrt (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:48
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) <= 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) - (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:49
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) )
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ^2) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) holds
(Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:50
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:51
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) & s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Product s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) >= ((Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) - n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:52
for s, s1 being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) & s1 : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds (Partial_Sums s1 : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SERIES_5:53
for s, s1 being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) & s1 : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / (s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds ((Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) * ((Partial_Sums s1 : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) >= (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ^2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SERIES_5:54
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = sqrt n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) & s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) < ((1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 6 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) * ((4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) * (sqrt n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:55
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = sqrt n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) set ) & s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > ((2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) * n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative ) set ) * (sqrt n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:56
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / ((2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) set ) & s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Partial_Product s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) * (sqrt ((2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: SERIES_5:57
for s being ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = sqrt (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) & s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) . 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V57() V58() V59() V60() V61() V62() V63() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) holds
for n being ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(Partial_Sums s : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( V21() V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) ) ( V16() V19( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V21() V26( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) V30( NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) V35() V36() V37() ) Element of K6(K7(NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( V35() V36() V37() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) > (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (n : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K6(REAL : ( ( ) ( V1() V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non negative ) Element of COMPLEX : ( ( ) ( V1() V46() V57() V63() ) set ) ) ;