:: ASYMPT_0 semantic presentation

scheme :: ASYMPT_0:sch 1
s1{ F1() -> Nat, F2() -> Nat, F3() -> non empty set , F4( set ) -> Element of F3() } :
{ F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() ) } is non empty finite Subset of F3()
provided
E1: F1() <= F2()
proof
defpred S1[ Nat] means verum;
set c1 = { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } ;
set c2 = { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() ) } ;
E2: now
let c3 be set ;
hereby
assume c3 in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } ;
then ex b1 being Nat st
( c3 = F4(b1) & F1() <= b1 & b1 <= F2() & S1[b1] ) ;
hence c3 in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() ) } ;
end;
assume c3 in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() ) } ;
then ex b1 being Nat st
( c3 = F4(b1) & F1() <= b1 & b1 <= F2() ) ;
hence c3 in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } ;
end;
E3: F4(F1()) in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } by E1;
E4: { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } is finite from FINSEQ_1:sch 6();
 { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } c= F3()
proof
let c3 be set ; :: according to TARSKI:def 3
assume c3 in { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } ;
then consider c4 being Nat such that
E5: c3 = F4(c4) and
( c4 >= F1() & c4 <= F2() ) ;
thus c3 in F3() by E5;
end;
hence { F4(b1) where B is Nat : ( F1() <= b1 & b1 <= F2() ) } is non empty finite Subset of F3() by E2, E3, E4, TARSKI:2;
end;

scheme :: ASYMPT_0:sch 2
s2{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
{ F3(b1) where B is Nat : b1 <= F1() } is non empty finite Subset of F2()
provided
proof
set c1 = { F3(b1) where B is Nat : b1 <= F1() } ;
set c2 = { F3(b1) where B is Nat : ( 0 <= b1 & b1 <= F1() ) } ;
E1: 0 <= F1() ;
E2: { F3(b1) where B is Nat : ( 0 <= b1 & b1 <= F1() ) } is non empty finite Subset of F2() from ASYMPT_0:sch 1(E1);
now
let c3 be set ;
hereby
assume c3 in { F3(b1) where B is Nat : b1 <= F1() } ;
then consider c4 being Nat such that
E3: ( c3 = F3(c4) & c4 <= F1() ) ;
thus c3 in { F3(b1) where B is Nat : ( 0 <= b1 & b1 <= F1() ) } by E3;
end;
assume c3 in { F3(b1) where B is Nat : ( 0 <= b1 & b1 <= F1() ) } ;
then consider c4 being Nat such that
E3: ( c3 = F3(c4) & 0 <= c4 & c4 <= F1() ) ;
thus c3 in { F3(b1) where B is Nat : b1 <= F1() } by E3;
end;
hence { F3(b1) where B is Nat : b1 <= F1() } is non empty finite Subset of F2() by E2, TARSKI:2;
end;

scheme :: ASYMPT_0:sch 3
s3{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
{ F3(b1) where B is Nat : b1 < F1() } is non empty finite Subset of F2()
provided
E1: F1() > 0
proof
set c1 = { F3(b1) where B is Nat : b1 < F1() } ;
consider c2 being Nat such that
E2: F1() = c2 + 1 by E1, NAT_1:22;
set c3 = { F3(b1) where B is Nat : b1 <= c2 } ;
E3: { F3(b1) where B is Nat : b1 <= c2 } is non empty finite Subset of F2() from ASYMPT_0:sch 2();
now
let c4 be set ;
hereby
assume c4 in { F3(b1) where B is Nat : b1 < F1() } ;
then consider c5 being Nat such that
E4: ( c4 = F3(c5) & c5 < F1() ) ;
c5 <= c2 by E2, E4, NAT_1:38;
hence c4 in { F3(b1) where B is Nat : b1 <= c2 } by E4;
end;
assume c4 in { F3(b1) where B is Nat : b1 <= c2 } ;
then consider c5 being Nat such that
E4: ( c4 = F3(c5) & c5 <= c2 ) ;
c5 < c2 + 1 by E4, NAT_1:38;
hence c4 in { F3(b1) where B is Nat : b1 < F1() } by E2, E4;
end;
hence { F3(b1) where B is Nat : b1 < F1() } is non empty finite Subset of F2() by E3, TARSKI:2;
end;

definition
let c1 be real number ;
canceled;
canceled;
attr a1 is logbase means :E1: :: ASYMPT_0:def 3
( a1 > 0 & a1 <> 1 );
end;

:: deftheorem ASYMPT_0:def 1 :
canceled;

:: deftheorem ASYMPT_0:def 2 :
canceled;

:: deftheorem E1 defines logbase ASYMPT_0:def 3 :
for b1 being real number holds
( b1 is logbase iff ( b1 > 0 & b1 <> 1 ) );

registration
cluster positive Element of REAL ;
existence
ex b1 being Real st b1 is positive
proof
take 1 ;
thus 1 is positive ;
end;
cluster negative Element of REAL ;
existence
ex b1 being Real st b1 is negative
proof
take - 1 ;
thus - 1 is negative by XREAL_0:def 4;
end;
cluster logbase Element of REAL ;
existence
ex b1 being Real st b1 is logbase
proof
take 2 ;
thus 2 is logbase by E1;
end;
cluster non negative Element of REAL ;
existence
not for b1 being Real holds b1 is negative by XREAL_0:def 4;
cluster non positive Element of REAL ;
existence
not for b1 being Real holds b1 is positive by XREAL_0:def 3;
cluster non logbase Element of REAL ;
existence
not for b1 being Real holds b1 is logbase
proof
take 1 ;
thus not 1 is logbase by E1;
end;
end;

definition
let c1 be Real_Sequence;
attr a1 is eventually-nonnegative means :E2: :: ASYMPT_0:def 4
ex b1 being Nat st
for b2 being Nat holds
( b2 >= b1 implies a1 . b2 >= 0 );
attr a1 is positive means :E3: :: ASYMPT_0:def 5
for b1 being Nat holds
a1 . b1 > 0;
attr a1 is eventually-positive means :E4: :: ASYMPT_0:def 6
ex b1 being Nat st
for b2 being Nat holds
not ( b2 >= b1 & not a1 . b2 > 0 );
attr a1 is eventually-nonzero means :E5: :: ASYMPT_0:def 7
ex b1 being Nat st
for b2 being Nat holds
not ( b2 >= b1 & not a1 . b2 <> 0 );
attr a1 is eventually-nondecreasing means :E6: :: ASYMPT_0:def 8
ex b1 being Nat st
for b2 being Nat holds
( b2 >= b1 implies a1 . b2 <= a1 . (b2 + 1) );
end;

:: deftheorem E2 defines eventually-nonnegative ASYMPT_0:def 4 :
for b1 being Real_Sequence holds
( b1 is eventually-nonnegative iff ex b2 being Nat st
for b3 being Nat holds
( b3 >= b2 implies b1 . b3 >= 0 ) );

:: deftheorem E3 defines positive ASYMPT_0:def 5 :
for b1 being Real_Sequence holds
( b1 is positive iff for b2 being Nat holds
b1 . b2 > 0 );

:: deftheorem E4 defines eventually-positive ASYMPT_0:def 6 :
for b1 being Real_Sequence holds
( b1 is eventually-positive iff ex b2 being Nat st
for b3 being Nat holds
not ( b3 >= b2 & not b1 . b3 > 0 ) );

:: deftheorem E5 defines eventually-nonzero ASYMPT_0:def 7 :
for b1 being Real_Sequence holds
( b1 is eventually-nonzero iff ex b2 being Nat st
for b3 being Nat holds
not ( b3 >= b2 & not b1 . b3 <> 0 ) );

:: deftheorem E6 defines eventually-nondecreasing ASYMPT_0:def 8 :
for b1 being Real_Sequence holds
( b1 is eventually-nondecreasing iff ex b2 being Nat st
for b3 being Nat holds
( b3 >= b2 implies b1 . b3 <= b1 . (b3 + 1) ) );

registration
cluster eventually-nonnegative positive eventually-positive eventually-nonzero eventually-nondecreasing M5( NAT , REAL );
existence
ex b1 being Real_Sequence st
( b1 is eventually-nonnegative & b1 is eventually-nonzero & b1 is positive & b1 is eventually-positive & b1 is eventually-nondecreasing )
proof
reconsider c1 = NAT --> 1 as Function of NAT , REAL by FUNCOP_1:57;
E7: for b1 being Nat holds c1 . b1 = 1 by FUNCOP_1:13;
take c1 ;
thus c1 is eventually-nonnegative
proof
take 0 ; :: according to ASYMPT_0:def 4
let c2 be Nat;
assume c2 >= 0 ;
c1 . c2 = 1 by E7;
hence c1 . c2 >= 0 ;
end;
thus c1 is eventually-nonzero
proof
take 0 ; :: according to ASYMPT_0:def 7
let c2 be Nat;
thus not ( c2 >= 0 & not c1 . c2 <> 0 ) by E7;
end;
thus c1 is positive
proof
let c2 be Nat; :: according to ASYMPT_0:def 5
c1 . c2 = 1 by E7;
hence c1 . c2 > 0 ;
end;
thus c1 is eventually-positive
proof
take 0 ; :: according to ASYMPT_0:def 6
let c2 be Nat;
assume c2 >= 0 ;
c1 . c2 = 1 by E7;
hence c1 . c2 > 0 ;
end;
thus c1 is eventually-nondecreasing
proof
take 0 ; :: according to ASYMPT_0:def 8
let c2 be Nat;
assume c2 >= 0 ;
( c1 . c2 = 1 & c1 . (c2 + 1) = 1 ) by E7;
hence c1 . c2 <= c1 . (c2 + 1) ;
end;
end;
end;

registration
cluster positive -> eventually-positive M5( NAT , REAL );
coherence
for b1 being Real_Sequence holds
( b1 is positive implies b1 is eventually-positive )
proof
let c1 be Real_Sequence;
assume E7: c1 is positive ;
take 0 ; :: according to ASYMPT_0:def 6
let c2 be Nat;
assume c2 >= 0 ;
thus c1 . c2 > 0 by E7, E3;
end;
cluster eventually-positive -> eventually-nonnegative eventually-nonzero M5( NAT , REAL );
coherence
for b1 being Real_Sequence holds
( b1 is eventually-positive implies ( b1 is eventually-nonnegative & b1 is eventually-nonzero ) )
proof
let c1 be Real_Sequence;
assume c1 is eventually-positive ;
then consider c2 being Nat such that
E7: for b1 being Nat holds
not ( b1 >= c2 & not c1 . b1 > 0 ) by E4;
thus c1 is eventually-nonnegative
proof
take c2 ; :: according to ASYMPT_0:def 4
let c3 be Nat;
assume c3 >= c2 ;
hence c1 . c3 >= 0 by E7;
end;
thus c1 is eventually-nonzero
proof
take c2 ; :: according to ASYMPT_0:def 7
let c3 be Nat;
assume c3 >= c2 ;
hence c1 . c3 <> 0 by E7;
end;
end;
cluster eventually-nonnegative eventually-nonzero -> eventually-positive M5( NAT , REAL );
coherence
for b1 being Real_Sequence holds
( ( b1 is eventually-nonnegative & b1 is eventually-nonzero ) implies ( b1 is eventually-positive ) )
proof
let c1 be Real_Sequence;
assume E7: ( c1 is eventually-nonnegative & c1 is eventually-nonzero ) ;
then consider c2 being Nat such that
E8: for b1 being Nat holds
( b1 >= c2 implies c1 . b1 >= 0 ) by E2;
consider c3 being Nat such that
E9: for b1 being Nat holds
not ( b1 >= c3 & not c1 . b1 <> 0 ) by E7, E5;
take c4 = max c2,c3; :: according to ASYMPT_0:def 6
let c5 be Nat;
assume E10: c5 >= c4 ;
( c4 >= c2 & c4 >= c3 ) by SQUARE_1:46;
then E11: ( c5 >= c2 & c5 >= c3 ) by E10, XREAL_1:2;
then c1 . c5 <> 0 by E9;
hence c1 . c5 > 0 by E8, E11;
end;
end;

definition
let c1, c2 be eventually-nonnegative Real_Sequence;
redefine func + as c1 + c2 -> eventually-nonnegative Real_Sequence;
coherence
c1 + c2 is eventually-nonnegative Real_Sequence
proof
consider c3 being Nat such that
E7: for b1 being Nat holds
( b1 >= c3 implies c1 . b1 >= 0 ) by E2;
consider c4 being Nat such that
E8: for b1 being Nat holds
( b1 >= c4 implies c2 . b1 >= 0 ) by E2;
set c5 = max c3,c4;
c1 + c2 is eventually-nonnegative
proof
take max c3,c4 ; :: according to ASYMPT_0:def 4
let c6 be Nat;
assume E9: c6 >= max c3,c4 ;
max c3,c4 >= c3 by SQUARE_1:46;
then c6 >= c3 by E9, XREAL_1:2;
then E10: c1 . c6 >= 0 by E7;
max c3,c4 >= c4 by SQUARE_1:46;
then c6 >= c4 by E9, XREAL_1:2;
then c2 . c6 >= 0 by E8;
then 0 + 0 <= (c1 . c6) + (c2 . c6) by E10, XREAL_1:9;
hence (c1 + c2) . c6 >= 0 by SEQ_1:11;
end;
hence c1 + c2 is eventually-nonnegative Real_Sequence ;
end;
end;

definition
let c1 be Real_Sequence;
let c2 be real number ;
func c2 + c1 -> Real_Sequence means :E7: :: ASYMPT_0:def 9
for b1 being Nat holds a3 . b1 = a2 + (a1 . b1);
existence
ex b1 being Real_Sequence st
for b2 being Nat holds b1 . b2 = c2 + (c1 . b2)
proof
reconsider c3 = c2 as Real by XREAL_0:def 1;
deffunc H1( Nat) -> Element of REAL = c3 + (c1 . a1);
consider c4 being Function of NAT , REAL such that
E7: for b1 being Nat holds c4 . b1 = H1(b1) from FUNCT_2:sch 4();
 take c4 ;
let c5 be Nat;
thus c4 . c5 = c2 + (c1 . c5) by E7;
end;
uniqueness
for b1, b2 being Real_Sequence holds
( ( ( for b3 being Nat holds b1 . b3 = c2 + (c1 . b3) ) & ( for b3 being Nat holds b2 . b3 = c2 + (c1 . b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Real_Sequence;
assume that
E7: for b1 being Nat holds c3 . b1 = c2 + (c1 . b1) and
E8: for b1 being Nat holds c4 . b1 = c2 + (c1 . b1) ;
now
let c5 be Nat;
thus c3 . c5 = c2 + (c1 . c5) by E7
.= c4 . c5 by E8 ;
end;
hence c3 = c4 by FUNCT_2:113;
end;
end;

:: deftheorem E7 defines + ASYMPT_0:def 9 :
for b1 being Real_Sequence
for b2 being real number
for b3 being Real_Sequence holds
( b3 = b2 + b1 iff for b4 being Nat holds b3 . b4 = b2 + (b1 . b4) );

notation
let c1 be Real_Sequence;
let c2 be real number ;
synonym c1 + c2 for c2 + c1;
end;

definition
let c1 be eventually-nonnegative Real_Sequence;
let c2 be positive Real;
redefine func (#) as c2 (#) c1 -> eventually-nonnegative Real_Sequence;
coherence
c2 (#) c1 is eventually-nonnegative Real_Sequence
proof
consider c3 being Nat such that
E8: for b1 being Nat holds
( b1 >= c3 implies c1 . b1 >= 0 ) by E2;
c2 (#) c1 is eventually-nonnegative
proof
take c3 ; :: according to ASYMPT_0:def 4
let c4 be Nat;
assume c4 >= c3 ;
then c1 . c4 >= 0 by E8;
then c2 * (c1 . c4) >= c2 * 0 by XREAL_1:66;
hence (c2 (#) c1) . c4 >= 0 by SEQ_1:13;
end;
hence c2 (#) c1 is eventually-nonnegative Real_Sequence ;
end;
end;

registration
let c1 be eventually-nonnegative Real_Sequence;
let c2 be non negative Real;
cluster a2 + a1 -> eventually-nonnegative ;
coherence
c2 + c1 is eventually-nonnegative
proof
consider c3 being Nat such that
E8: for b1 being Nat holds
( b1 >= c3 implies c1 . b1 >= 0 ) by E2;
take c3 ; :: according to ASYMPT_0:def 4
let c4 be Nat;
assume c4 >= c3 ;
then c1 . c4 >= 0 by E8;
then c2 + (c1 . c4) >= 0 + 0 by XREAL_1:9;
hence (c2 + c1) . c4 >= 0 by E7;
end;
end;

registration
let c1 be eventually-nonnegative Real_Sequence;
let c2 be positive Real;
cluster a2 + a1 -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence
c2 + c1 is eventually-positive
proof
consider c3 being Nat such that
E8: for b1 being Nat holds
( b1 >= c3 implies c1 . b1 >= 0 ) by E2;
take c3 ; :: according to ASYMPT_0:def 6
let c4 be Nat;
assume c4 >= c3 ;
then c1 . c4 >= 0 by E8;
then c2 + (c1 . c4) > 0 + 0 by XREAL_1:10;
hence (c2 + c1) . c4 > 0 by E7;
end;
end;

definition
let c1, c2 be Real_Sequence;
func max c1,c2 -> Real_Sequence means :E8: :: ASYMPT_0:def 10
for b1 being Nat holds a3 . b1 = max (a1 . b1),(a2 . b1);
existence
ex b1 being Real_Sequence st
for b2 being Nat holds b1 . b2 = max (c1 . b2),(c2 . b2)
proof
deffunc H1( Nat) -> Element of REAL = max (c1 . a1),(c2 . a1);
consider c3 being Function of NAT , REAL such that
E8: for b1 being Nat holds c3 . b1 = H1(b1) from FUNCT_2:sch 4();
 take c3 ;
let c4 be Nat;
thus c3 . c4 = max (c1 . c4),(c2 . c4) by E8;
end;
uniqueness
for b1, b2 being Real_Sequence holds
( ( ( for b3 being Nat holds b1 . b3 = max (c1 . b3),(c2 . b3) ) & ( for b3 being Nat holds b2 . b3 = max (c1 . b3),(c2 . b3) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Real_Sequence;
assume that
E8: for b1 being Nat holds c3 . b1 = max (c1 . b1),(c2 . b1) and
E9: for b1 being Nat holds c4 . b1 = max (c1 . b1),(c2 . b1) ;
now
let c5 be Nat;
thus c3 . c5 = max (c1 . c5),(c2 . c5) by E8
.= c4 . c5 by E9 ;
end;
hence c3 = c4 by FUNCT_2:113;
end;
commutativity
for b1, b2, b3 being Real_Sequence holds
( ( for b4 being Nat holds b1 . b4 = max (b2 . b4),(b3 . b4) ) implies for b4 being Nat holds b1 . b4 = max (b3 . b4),(b2 . b4) ) ;
end;

:: deftheorem E8 defines max ASYMPT_0:def 10 :
for b1, b2, b3 being Real_Sequence holds
( b3 = max b1,b2 iff for b4 being Nat holds b3 . b4 = max (b1 . b4),(b2 . b4) );

registration
let c1 be Real_Sequence;
let c2 be eventually-nonnegative Real_Sequence;
cluster max a1,a2 -> eventually-nonnegative ;
coherence
max c1,c2 is eventually-nonnegative
proof
consider c3 being Nat such that
E9: for b1 being Nat holds
( b1 >= c3 implies c2 . b1 >= 0 ) by E2;
take c3 ; :: according to ASYMPT_0:def 4
let c4 be Nat;
assume c4 >= c3 ;
then E10: c2 . c4 >= 0 by E9;
max (c1 . c4),(c2 . c4) >= c2 . c4 by SQUARE_1:46;
hence (max c1,c2) . c4 >= 0 by E10, E8;
end;
end;

registration
let c1 be Real_Sequence;
let c2 be eventually-positive Real_Sequence;
cluster max a1,a2 -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence
max c1,c2 is eventually-positive
proof
consider c3 being Nat such that
E9: for b1 being Nat holds
not ( b1 >= c3 & not c2 . b1 > 0 ) by E4;
take c3 ; :: according to ASYMPT_0:def 6
let c4 be Nat;
assume c4 >= c3 ;
then c2 . c4 > 0 by E9;
then max (c1 . c4),(c2 . c4) > 0 by SQUARE_1:46;
hence (max c1,c2) . c4 > 0 by E8;
end;
end;

definition
let c1, c2 be Real_Sequence;
pred c2 majorizes c1 means :E9: :: ASYMPT_0:def 11
ex b1 being Nat st
for b2 being Nat holds
( b2 >= b1 implies a1 . b2 <= a2 . b2 );
end;

:: deftheorem E9 defines majorizes ASYMPT_0:def 11 :
for b1, b2 being Real_Sequence holds
( b2 majorizes b1 iff ex b3 being Nat st
for b4 being Nat holds
( b4 >= b3 implies b1 . b4 <= b2 . b4 ) );

E10: for b1, b2 being Real_Sequence
for b3 being Nat holds (b1 /" b2) . b3 = (b1 . b3) / (b2 . b3)
proof
let c1, c2 be Real_Sequence;
let c3 be Nat;
thus (c1 /" c2) . c3 = (c1 (#) (c2 " )) . c3 by SEQ_1:def 9
.= (c1 . c3) * ((c2 " ) . c3) by SEQ_1:12
.= (c1 . c3) * ((c2 . c3) " ) by SEQ_1:def 8
.= (c1 . c3) / (c2 . c3) by XCMPLX_0:def 9 ;
end;

theorem E11: :: ASYMPT_0:1
for b1 being Real_Sequence
for b2 being Nat holds
( ( for b3 being Nat holds
( b3 >= b2 implies b1 . b3 <= b1 . (b3 + 1) ) ) implies for b3, b4 being Nat holds
( ( b2 <= b3 & b3 <= b4 ) implies ( b1 . b3 <= b1 . b4 ) ) )
proof
let c1 be Real_Sequence;
let c2 be Nat;
assume E12: for b1 being Nat holds
( b1 >= c2 implies c1 . b1 <= c1 . (b1 + 1) ) ;
let c3, c4 be Nat;
assume E13: c3 >= c2 ;
defpred S1[ Nat] means c1 . c3 <= c1 . a1;
E14: S1[c3] ;
E15: for b1 being Nat holds
( ( b1 >= c3 & S1[b1] ) implies ( S1[b1 + 1] ) )
proof
let c5 be Nat;
assume E16: ( c5 >= c3 & c1 . c3 <= c1 . c5 ) ;
then c5 >= c2 by E13, XREAL_1:2;
then c1 . c5 <= c1 . (c5 + 1) by E12;
hence c1 . c3 <= c1 . (c5 + 1) by E16, XREAL_1:2;
end;
for b1 being Nat holds
( b1 >= c3 implies S1[b1] ) from INT_2:sch 1(E14, E15);
 hence not ( c3 <= c4 & not c1 . c3 <= c1 . c4 ) ;
end;

theorem E12: :: ASYMPT_0:2
for b1, b2 being eventually-positive Real_Sequence holds
( ( b1 /" b2 is convergent ) implies ( not lim (b1 /" b2) <> 0 or ( b2 /" b1 is convergent & lim (b2 /" b1) = (lim (b1 /" b2)) " ) ) )
proof
let c1, c2 be eventually-positive Real_Sequence;
set c3 = c1 /" c2;
set c4 = abs (lim (c1 /" c2));
set c5 = lim (c1 /" c2);
assume that
E13: c1 /" c2 is convergent and
E14: lim (c1 /" c2) <> 0 ;
consider c6 being Nat such that
E15: for b1 being Nat holds
not ( b1 >= c6 & not c1 . b1 > 0 ) by E4;
consider c7 being Nat such that
E16: for b1 being Nat holds
not ( b1 >= c7 & not c2 . b1 > 0 ) by E4;
E17: 0 < abs (lim (c1 /" c2)) by E14, COMPLEX1:133;
E18: 0 <> abs (lim (c1 /" c2)) by E14, COMPLEX1:133;
consider c8 being Nat such that
E19: for b1 being Nat holds
not ( c8 <= b1 & not (abs (lim (c1 /" c2))) / 2 < abs ((c1 /" c2) . b1) ) by E13, E14, SEQ_2:30;
0 * 0 < (abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2))) by E17, XREAL_1:98;
then E20: 0 < ((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2 by SEQ_2:3;
E21: now
let c9 be real number ;
assume E22: 0 < c9 ;
then 0 * 0 < c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2) by E20, XREAL_1:98;
then consider c10 being Nat such that
E23: for b1 being Nat holds
not ( c10 <= b1 & not abs (((c1 /" c2) . b1) - (lim (c1 /" c2))) < c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2) ) by E13, SEQ_2:def 7;
set c11 = c6 + c7;
E24: ( c6 <= c6 + c7 & c7 <= c6 + c7 ) by NAT_1:37;
set c12 = (c6 + c7) + c8;
E25: ( c6 <= (c6 + c7) + c8 & c7 <= (c6 + c7) + c8 & c6 + c7 <= (c6 + c7) + c8 & c8 <= (c6 + c7) + c8 ) by E24, NAT_1:37;
take c13 = ((c6 + c7) + c8) + c10;
E26: ( c6 <= c13 & c7 <= c13 & c6 + c7 <= c13 & (c6 + c7) + c8 <= c13 & c8 <= c13 & c10 <= c13 ) by E25, NAT_1:37;
let c14 be Nat;
assume E27: c13 <= c14 ;
set c15 = abs ((c1 /" c2) . c14);
E28: ( c6 <= c14 & c7 <= c14 & c6 + c7 <= c14 & (c6 + c7) + c8 <= c14 & c8 <= c14 & c10 <= c14 ) by E26, E27, XREAL_1:2;
then E29: abs (((c1 /" c2) . c14) - (lim (c1 /" c2))) < c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2) by E23;
E30: (abs (lim (c1 /" c2))) / 2 < abs ((c1 /" c2) . c14) by E19, E28;
( c1 . c14 <> 0 & c2 . c14 <> 0 ) by E15, E16, E28;
then (c1 . c14) / (c2 . c14) <> 0 by XCMPLX_1:50;
then E31: (c1 /" c2) . c14 <> 0 by E10;
then ((c1 /" c2) . c14) * (lim (c1 /" c2)) <> 0 by E14, XCMPLX_1:6;
then 0 < abs (((c1 /" c2) . c14) * (lim (c1 /" c2))) by COMPLEX1:133;
then 0 < (abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2))) by COMPLEX1:151;
then E32: (abs (((c1 /" c2) . c14) - (lim (c1 /" c2)))) / ((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) < (c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2)) / ((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) by E29, REAL_1:73;
E33: (c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2)) / ((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) = (c9 * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) / 2)) * (((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) " ) by XCMPLX_0:def 9
.= (c9 * ((2 " ) * ((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))))) * (((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) " ) by XCMPLX_0:def 9
.= ((c9 * (2 " )) * ((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2))))) * (((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) " )
.= (c9 * (2 " )) * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) * (((abs (lim (c1 /" c2))) * (abs ((c1 /" c2) . c14))) " )) by XCMPLX_1:4
.= (c9 * (2 " )) * (((abs (lim (c1 /" c2))) * (abs (lim (c1 /" c2)))) * (((abs (lim (c1 /" c2))) " ) * ((abs ((c1 /" c2) . c14)) " ))) by XCMPLX_1:205
.= (c9 * (2 " )) * (((abs (lim (c1 /" c2))) * ((abs (lim (c1 /" c2))) * ((abs (lim (c1 /" c2))) " ))) * ((abs ((c1 /" c2) . c14)) " ))
.= (c9 * (2 " )) * (((abs (lim (c1 /" c2))) * 1) * ((abs ((c1 /" c2) . c14)) " )) by E18, XCMPLX_0:def 7
.= (c9 * ((2 " ) * (abs (lim (c1 /" c2))))) * ((abs ((c1 /" c2) . c14)) " )
.= (c9 * ((abs (lim (c1 /" c2))) / 2)) * ((abs ((c1 /" c2) . c14)) " ) by XCMPLX_0:def 9
.= (c9 * ((abs (lim (c1 /" c2))) / 2)) / (abs ((c1 /" c2) . c14)) by XCMPLX_0:def 9 ;
E34: abs (((c2 /" c1) . c14) - ((lim (c1 /" c2)) " )) = abs (((c2 . c14) / (c1 . c14)) - ((lim (c1 /" c2)) " )) by E10
.= abs ((((c1 . c14) / (c2 . c14)) " ) - ((lim (c1 /" c2)) " )) by XCMPLX_1:215
.= abs ((((c1 /" c2) . c14) " ) - ((lim (c1 /" c2)) " )) by E10
.= (abs (((c1 /" c2) . c14) - (lim (c1 /" c2)))) / ((abs ((c1 /" c2) . c14)) * (abs (lim (c1 /" c2)))) by E14, E31, SEQ_2:11 ;
E35: 0 < (abs (lim (c1 /" c2))) / 2 by E17, SEQ_2:3;
E36: 0 <> (abs (lim (c1 /" c2))) / 2 by E17;
0 * 0 < c9 * ((abs (lim (c1 /" c2))) / 2) by E22, E35, XREAL_1:98;
then E37: (c9 * ((abs (lim (c1 /" c2))) / 2)) / (abs ((c1 /" c2) . c14)) < (c9 * ((abs (lim (c1 /" c2))) / 2)) / ((abs (lim (c1 /" c2))) / 2) by E30, E35, XREAL_1:78;
(c9 * ((abs (lim (c1 /"