let r be real number ; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) implies seq is convergent )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ; :: thesis: seq is convergent
take g = 0 ; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((seq . b₃) - g) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) ) )
assume A3: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) )
then A4: 0 < p " ;
consider k1 being Element of NAT such that
A5: p " < k1 by Th10;
take n = k1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((seq . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((seq . m) - g) )
assume A6: n <= m ; :: thesis: not p <= abs ((seq . m) - g)
( 0 <= n & 0 <= m ) by NAT_1:2;
then A7: n * n <= m * m by A6, XREAL_1:68;
A8: k1 > 0 by A3, A5;
then k1 >= 1 + 0 by NAT_1:13;
then k1 <= k1 * k1 by XREAL_1:153;
then A9: k1 + r <= (k1 * k1) + r by XREAL_1:8;
(p " ) + 0 < k1 + r by A1, A5, XREAL_1:10;
then (p " ) + 0 < (k1 * k1) + r by A9, XXREAL_0:2;
then 1 / ((k1 * k1) + r) < 1 / (p " ) by A4, XREAL_1:78;
then A10: 1 / ((k1 * k1) + r) < 1 * ((p " ) " ) by XCMPLX_0:def 9;
B11: 0 < n ^2 by A8, SQUARE_1:74;
(n * n) + r <= (m * m) + r by A7, XREAL_1:8;
then 1 / ((m * m) + r) <= 1 / ((n * n) + r) by A1, B11, XREAL_1:120;
then A12: 1 / ((m * m) + r) < p by A10, XXREAL_0:2;
A13: seq . m = 1 / ((m * m) + r) by A2;
0 <= m * m by NAT_1:2;
hence not p <= abs ((seq . m) - g) by A12, A13, A1, ABSVALUE:def 1; :: thesis: verum