defpred S1[ R_eal] means ( ex g being real number st
( $1 = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - $1).| < p ) & seq is convergent_to_finite_number ) or ( $1 = +infty & seq is convergent_to_+infty ) or ( $1 = -infty & seq is convergent_to_-infty ) );
given g1, g2 being R_eal such that A3:
S1[g1]
and
A4:
S1[g2]
and
A5:
g1 <> g2
; contradiction
per cases
( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty )
by A1, Def11;
suppose A6:
seq is
convergent_to_finite_number
;
contradictionthen consider g being
real number such that A7:
g1 = g
and A8:
for
p being
real number st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - g1).| < p
and
seq is
convergent_to_finite_number
by A3, Th56, Th57;
consider h being
real number such that A9:
g2 = h
and A10:
for
p being
real number st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - g2).| < p
and
seq is
convergent_to_finite_number
by A4, A6, Th56, Th57;
reconsider g =
g,
h =
h as
complex number ;
g - h <> 0
by A5, A7, A9;
then A11:
|.(g - h).| > 0
;
then consider n1 being
Nat such that A12:
for
m being
Nat st
n1 <= m holds
|.((seq . m) - g1).| < R_EAL (|.(g - h).| / 2)
by A8;
consider n2 being
Nat such that A13:
for
m being
Nat st
n2 <= m holds
|.((seq . m) - g2).| < R_EAL (|.(g - h).| / 2)
by A10, A11;
reconsider n1 =
n1,
n2 =
n2 as
Element of
NAT by ORDINAL1:def 13;
set m =
max (
n1,
n2);
A14:
|.((seq . (max (n1,n2))) - g1).| < R_EAL (|.(g - h).| / 2)
by A12, XXREAL_0:25;
A15:
|.((seq . (max (n1,n2))) - g2).| < R_EAL (|.(g - h).| / 2)
by A13, XXREAL_0:25;
reconsider g =
g,
h =
h as
Real by XREAL_0:def 1;
A16:
(seq . (max (n1,n2))) - g2 < R_EAL (|.(g - h).| / 2)
by A15, EXTREAL2:58;
A17:
- (R_EAL (|.(g - h).| / 2)) < (seq . (max (n1,n2))) - g2
by A15, EXTREAL2:58;
then reconsider w =
(seq . (max (n1,n2))) - g2 as
Real by A16, XXREAL_0:48;
A18:
(seq . (max (n1,n2))) - g2 in REAL
by A17, A16, XXREAL_0:48;
then A19:
seq . (max (n1,n2)) <> +infty
by A9;
A20:
(- (seq . (max (n1,n2)))) + g1 = - ((seq . (max (n1,n2))) - g1)
by XXREAL_3:27;
then A21:
|.((- (seq . (max (n1,n2)))) + g1).| < R_EAL (|.(g - h).| / 2)
by A14, EXTREAL2:66;
then A22:
(- (seq . (max (n1,n2)))) + g1 < R_EAL (|.(g - h).| / 2)
by EXTREAL2:58;
- (R_EAL (|.(g - h).| / 2)) < (- (seq . (max (n1,n2)))) + g1
by A21, EXTREAL2:58;
then A23:
(- (seq . (max (n1,n2)))) + g1 in REAL
by A22, XXREAL_0:48;
A24:
seq . (max (n1,n2)) <> -infty
by A9, A18;
|.(g1 - g2).| =
|.((g1 + 0.) - g2).|
by XXREAL_3:4
.=
|.((g1 + ((seq . (max (n1,n2))) + (- (seq . (max (n1,n2)))))) - g2).|
by XXREAL_3:7
.=
|.((((- (seq . (max (n1,n2)))) + g1) + (seq . (max (n1,n2)))) - g2).|
by A7, A19, A24, XXREAL_3:30
.=
|.(((- (seq . (max (n1,n2)))) + g1) + ((seq . (max (n1,n2))) - g2)).|
by A9, A23, XXREAL_3:31
;
then
|.(g1 - g2).| <= |.((- (seq . (max (n1,n2)))) + g1).| + |.((seq . (max (n1,n2))) - g2).|
by EXTREAL2:61;
then A25:
|.(g1 - g2).| <= |.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).|
by A20, EXTREAL2:66;
A26:
(R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2)) = (|.(g - h).| / 2) + (|.(g - h).| / 2)
by SUPINF_2:1;
|.w.| in REAL
;
then
|.((seq . (max (n1,n2))) - g2).| in REAL
by EXTREAL2:49;
then A27:
|.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| < (R_EAL (|.(g - h).| / 2)) + |.((seq . (max (n1,n2))) - g2).|
by A14, XXREAL_3:47;
(R_EAL (|.(g - h).| / 2)) + |.((seq . (max (n1,n2))) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2))
by A15, XXREAL_3:47;
then A28:
|.((seq . (max (n1,n2))) - g1).| + |.((seq . (max (n1,n2))) - g2).| < (R_EAL (|.(g - h).| / 2)) + (R_EAL (|.(g - h).| / 2))
by A27, XXREAL_0:2;
g - h = g1 - g2
by A7, A9, SUPINF_2:5;
hence
contradiction
by A28, A25, A26, EXTREAL2:49;
verum end;