let seq be Real_Sequence; :: thesis: ( seq is convergent implies abs seq is convergent )
assume seq is convergent ; :: thesis: abs seq is convergent
then consider g1 being real number such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by SEQ_2:def 6;
reconsider g1 = g1 as Real by XREAL_0:def 1;
take g = abs g1; :: 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 (((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 (((abs seq) . b₂) - g) ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs (((abs seq) . b₂) - g) )
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p by A1;
take n = n1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs (((abs seq) . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs (((abs seq) . m) - g) )
abs (g1 - (seq . m)) = abs (- ((seq . m) - g1))
.= abs ((seq . m) - g1) by COMPLEX1:138 ;
then g - (abs (seq . m)) <= abs ((seq . m) - g1) by COMPLEX1:145;
then ( (abs (seq . m)) - g <= abs ((seq . m) - g1) & - (abs ((seq . m) - g1)) <= - (g - (abs (seq . m))) ) by COMPLEX1:145, XREAL_1:26;
then abs ((abs (seq . m)) - g) <= abs ((seq . m) - g1) by ABSVALUE:12;
then A3: abs (((abs seq) . m) - g) <= abs ((seq . m) - g1) by SEQ_1:16;
assume n <= m ; :: thesis: not p <= abs (((abs seq) . m) - g)
then abs ((seq . m) - g1) < p by A2;
hence not p <= abs (((abs seq) . m) - g) by A3, XXREAL_0:2; :: thesis: verum