let seq1 be V183() ExtREAL_sequence; for seq2 being V184() ExtREAL_sequence holds
( ( seq1 is convergent_to_+infty & seq2 is convergent_to_-infty implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) ) )
let seq2 be V184() ExtREAL_sequence; ( ( seq1 is convergent_to_+infty & seq2 is convergent_to_-infty implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) ) )
reconsider f1 = - seq1 as V184() ExtREAL_sequence ;
reconsider f2 = - seq2 as V183() ExtREAL_sequence ;
hereby ( ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) ) )
assume A1:
(
seq1 is
convergent_to_+infty &
seq2 is
convergent_to_-infty )
;
( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty )then A2:
(
f1 is
convergent_to_-infty &
f2 is
convergent_to_+infty )
by Th17;
then reconsider F1 =
f1 + seq2,
F2 =
seq1 + f2 as
convergent ExtREAL_sequence by A1, Th24, Th18;
A3:
(
f1 + seq2 is
convergent_to_-infty &
f1 + seq2 is
convergent &
lim (f1 + seq2) = -infty &
seq1 + f2 is
convergent_to_+infty &
seq1 + f2 is
convergent &
lim (seq1 + f2) = +infty )
by A1, A2, Th24, Th18;
A4:
seq1 - seq2 =
seq1 + (- seq2)
by Th10
.=
- (seq2 - seq1)
by Th10
.=
- ((- seq1) + seq2)
by Th10
;
seq2 - seq1 =
seq2 + (- seq1)
by Th10
.=
- (seq1 - seq2)
by Th10
.=
- ((- seq2) + seq1)
by Th10
;
hence
(
seq1 - seq2 is
convergent_to_+infty &
seq1 - seq2 is
convergent &
seq2 - seq1 is
convergent_to_-infty &
seq2 - seq1 is
convergent &
lim (seq1 - seq2) = +infty &
lim (seq2 - seq1) = -infty )
by A3, A4, Th17, XXREAL_3:5, XXREAL_3:6;
verum
end;
hereby ( ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty ) ) & ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) ) )
assume A1:
(
seq1 is
convergent_to_+infty &
seq2 is
convergent_to_finite_number )
;
( seq1 - seq2 is convergent_to_+infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_-infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = +infty & lim (seq2 - seq1) = -infty )then A2:
(
f1 is
convergent_to_-infty &
f2 is
convergent_to_finite_number )
by Th17;
then reconsider F1 =
f1 + seq2,
F2 =
seq1 + f2 as
convergent ExtREAL_sequence by A1, Th24, Th19;
A3:
(
f1 + seq2 is
convergent_to_-infty &
f1 + seq2 is
convergent &
lim (f1 + seq2) = -infty &
seq1 + f2 is
convergent_to_+infty &
seq1 + f2 is
convergent &
lim (seq1 + f2) = +infty )
by A1, A2, Th24, Th19;
A4:
seq1 - seq2 =
seq1 + (- seq2)
by Th10
.=
- (seq2 - seq1)
by Th10
.=
- ((- seq1) + seq2)
by Th10
;
seq2 - seq1 =
seq2 + (- seq1)
by Th10
.=
- (seq1 - seq2)
by Th10
.=
- ((- seq2) + seq1)
by Th10
;
hence
(
seq1 - seq2 is
convergent_to_+infty &
seq1 - seq2 is
convergent &
seq2 - seq1 is
convergent_to_-infty &
seq2 - seq1 is
convergent &
lim (seq1 - seq2) = +infty &
lim (seq2 - seq1) = -infty )
by A3, A4, Th17, XXREAL_3:5, XXREAL_3:6;
verum
end;
hereby ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) ) )
assume A1:
(
seq1 is
convergent_to_-infty &
seq2 is
convergent_to_finite_number )
;
( seq1 - seq2 is convergent_to_-infty & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_+infty & seq2 - seq1 is convergent & lim (seq1 - seq2) = -infty & lim (seq2 - seq1) = +infty )then A2:
(
f1 is
convergent_to_+infty &
f2 is
convergent_to_finite_number )
by Th17;
then reconsider F1 =
f1 + seq2,
F2 =
seq1 + f2 as
convergent ExtREAL_sequence by A1, Th24, Th22;
A3:
(
f1 + seq2 is
convergent_to_+infty &
f1 + seq2 is
convergent &
lim (f1 + seq2) = +infty &
seq1 + f2 is
convergent_to_-infty &
seq1 + f2 is
convergent &
lim (seq1 + f2) = -infty )
by A1, A2, Th24, Th22;
A4:
seq1 - seq2 =
seq1 + (- seq2)
by Th10
.=
- (seq2 - seq1)
by Th10
.=
- ((- seq1) + seq2)
by Th10
;
seq2 - seq1 =
seq2 + (- seq1)
by Th10
.=
- (seq1 - seq2)
by Th10
.=
- ((- seq2) + seq1)
by Th10
;
hence
(
seq1 - seq2 is
convergent_to_-infty &
seq1 - seq2 is
convergent &
seq2 - seq1 is
convergent_to_+infty &
seq2 - seq1 is
convergent &
lim (seq1 - seq2) = -infty &
lim (seq2 - seq1) = +infty )
by A3, A4, Th17, XXREAL_3:5, XXREAL_3:6;
verum
end;
assume A1:
( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number )
; ( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) )
then A2:
( f1 is convergent_to_finite_number & f2 is convergent_to_finite_number )
by Th17;
then reconsider F1 = f1 + seq2, F2 = seq1 + f2 as convergent ExtREAL_sequence by A1, Th24, Th23;
A3:
( f1 + seq2 is convergent_to_finite_number & f1 + seq2 is convergent & seq1 + f2 is convergent_to_finite_number & seq1 + f2 is convergent & lim (f1 + seq2) = (lim f1) + (lim seq2) & lim (seq1 + f2) = (lim seq1) + (lim f2) )
by A1, A2, Th24, Th23;
A4: seq1 - seq2 =
seq1 + (- seq2)
by Th10
.=
- (seq2 - seq1)
by Th10
.=
- ((- seq1) + seq2)
by Th10
;
then A5:
lim (seq1 - seq2) = - ((lim f1) + (lim seq2))
by A3, Th17;
A6: seq2 - seq1 =
seq2 + (- seq1)
by Th10
.=
- (seq1 - seq2)
by Th10
.=
- ((- seq2) + seq1)
by Th10
;
then A7:
lim (seq2 - seq1) = - ((lim f2) + (lim seq1))
by A3, Th17;
( seq1 = - f1 & seq2 = - f2 )
by Th2;
then
( lim seq1 = - (lim f1) & lim seq2 = - (lim f2) )
by A2, Th17;
hence
( seq1 - seq2 is convergent_to_finite_number & seq1 - seq2 is convergent & seq2 - seq1 is convergent_to_finite_number & seq2 - seq1 is convergent & lim (seq1 - seq2) = (lim seq1) - (lim seq2) & lim (seq2 - seq1) = (lim seq2) - (lim seq1) )
by A3, A4, A5, A6, A7, Th17, XXREAL_3:9; verum