let seq be convergent ExtREAL_sequence; :: thesis: ( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( - seq is convergent_to_finite_number implies seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( - seq is convergent_to_-infty implies seq is convergent_to_+infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )
now :: thesis: ( - seq is convergent_to_finite_number implies seq is convergent_to_finite_number )
assume - seq is convergent_to_finite_number ; :: thesis: seq is convergent_to_finite_number
then - (- seq) is convergent_to_finite_number by Lm6;
hence seq is convergent_to_finite_number by Th2; :: thesis: verum
end;
hence ( seq is convergent_to_finite_number iff - seq is convergent_to_finite_number ) by Lm6; :: thesis: ( ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( - seq is convergent_to_-infty implies seq is convergent_to_+infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )
now :: thesis: ( - seq is convergent_to_-infty implies seq is convergent_to_+infty )
assume - seq is convergent_to_-infty ; :: thesis: seq is convergent_to_+infty
then - (- seq) is convergent_to_+infty by Lm6;
hence seq is convergent_to_+infty by Th2; :: thesis: verum
end;
hence ( seq is convergent_to_+infty iff - seq is convergent_to_-infty ) by Lm6; :: thesis: ( ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )
now :: thesis: ( - seq is convergent_to_+infty implies seq is convergent_to_-infty )
assume - seq is convergent_to_+infty ; :: thesis: seq is convergent_to_-infty
then - (- seq) is convergent_to_-infty by Lm6;
hence seq is convergent_to_-infty by Th2; :: thesis: verum
end;
hence ( seq is convergent_to_-infty iff - seq is convergent_to_+infty ) by Lm6; :: thesis: ( - seq is convergent & lim (- seq) = - (lim seq) )
thus ( - seq is convergent & lim (- seq) = - (lim seq) ) by Lm6; :: thesis: verum