:: LIMFUNC1 semantic presentation

Lm1: (- 1) * (- 1) = 1
;

Lm2: for g, r, r1 being real number st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )

proof end;

Lm3: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL st rng seq c= dom (f1 + f2) holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )

proof end;

Lm4: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL , REAL st rng seq c= dom (f1 (#) f2) holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )

proof end;

definition

let n, m be Nat;
:: original: max
redefine func max n,m -> Nat;
coherence by FINSEQ_2:1;

end;

Lm5: for r1, r2, g1, g2 being real number st 0 <= r1 & r1 < r2 & 0 < g1 & g1 <= g2 holds
r1 * g1 < r2 * g2
by XREAL_1:99;

notation

let r be real number ;
synonym left_open_halfline r for halfline r;

end;

definition

let r be real number ;
func left_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 1
{ g where g is Real : g <= r } ;
coherence

proof end;

func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2
{ g where g is Real : r <= g } ;
coherence

proof end;

func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3
{ g where g is Real : r < g } ;
coherence

proof end;

end;

:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :

:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :

:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :

theorem :: LIMFUNC1:1

canceled;

theorem :: LIMFUNC1:2

canceled;

theorem :: LIMFUNC1:3

canceled;

theorem :: LIMFUNC1:4

canceled;

theorem :: LIMFUNC1:5

canceled;

theorem :: LIMFUNC1:6

canceled;

theorem :: LIMFUNC1:7

canceled;

theorem :: LIMFUNC1:8

for r1, r2 being real number st r1 <= r2 holds
right_open_halfline r2 c= right_open_halfline r1

proof end;

theorem :: LIMFUNC1:9

for r1, r2 being real number st r1 <= r2 holds
right_closed_halfline r2 c= right_closed_halfline r1

proof end;

theorem :: LIMFUNC1:10

for r being real number holds right_open_halfline r c= right_closed_halfline r

proof end;

theorem :: LIMFUNC1:11

for r, g being real number holds ].r,g.[ c= right_open_halfline r

proof end;

theorem :: LIMFUNC1:12

for r, g being real number holds [.r,g.] c= right_closed_halfline r

proof end;

theorem :: LIMFUNC1:13

for r1, r2 being real number st r1 <= r2 holds
left_open_halfline r1 c= left_open_halfline r2

proof end;

theorem :: LIMFUNC1:14

for r1, r2 being real number st r1 <= r2 holds
left_closed_halfline r1 c= left_closed_halfline r2

proof end;

theorem :: LIMFUNC1:15

for r being real number holds left_open_halfline r c= left_closed_halfline r

proof end;

theorem :: LIMFUNC1:16

for g, r being real number holds ].g,r.[ c= left_open_halfline r

proof end;

theorem :: LIMFUNC1:17

for g, r being real number holds [.g,r.] c= left_closed_halfline r

proof end;

theorem Th18: :: LIMFUNC1:18

for r, g being real number holds (left_open_halfline r) /\ (right_open_halfline g) = ].g,r.[

proof end;

theorem Th19: :: LIMFUNC1:19

for r, g being real number holds (left_closed_halfline r) /\ (right_closed_halfline g) = [.g,r.]

proof end;

theorem :: LIMFUNC1:20

for r, r1, r2 being real number st r <= r1 holds
( ].r1,r2.[ c= right_open_halfline r & [.r1,r2.] c= right_closed_halfline r )

proof end;

theorem :: LIMFUNC1:21

for r, r1, r2 being real number st r < r1 holds
[.r1,r2.] c= right_open_halfline r

proof end;

theorem :: LIMFUNC1:22

for r2, r, r1 being real number st r2 <= r holds
( ].r1,r2.[ c= left_open_halfline r & [.r1,r2.] c= left_closed_halfline r )

proof end;

theorem :: LIMFUNC1:23

for r2, r, r1 being real number st r2 < r holds
[.r1,r2.] c= left_open_halfline r

proof end;

theorem Th24: :: LIMFUNC1:24

for r being real number holds
( REAL \ (right_open_halfline r) = left_closed_halfline r & REAL \ (right_closed_halfline r) = left_open_halfline r & REAL \ (left_open_halfline r) = right_closed_halfline r & REAL \ (left_closed_halfline r) = right_open_halfline r )

proof end;

theorem :: LIMFUNC1:25

for r1, r2 being real number holds
( REAL \ ].r1,r2.[ = (left_closed_halfline r1) \/ (right_closed_halfline r2) & REAL \ [.r1,r2.] = (left_open_halfline r1) \/ (right_open_halfline r2) )

proof end;

theorem Th26: :: LIMFUNC1:26

for seq being Real_Sequence holds
( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) )

proof end;

theorem Th27: :: LIMFUNC1:27

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is non-decreasing holds
for n being Nat holds seq . n < 0

proof end;

theorem Th28: :: LIMFUNC1:28

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is non-increasing holds
for n being Nat holds 0 < seq . n

proof end;

theorem Th29: :: LIMFUNC1:29

for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Nat st
for m being Nat st n <= m holds
0 < seq . m

proof end;

theorem Th30: :: LIMFUNC1:30

for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Nat st
for m being Nat st n <= m holds
(lim seq) / 2 < seq . m

proof end;

definition

let seq be Real_Sequence;
attr seq is divergent_to+infty means :Def4: :: LIMFUNC1:def 4
for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < seq . m;
attr seq is divergent_to-infty means :Def5: :: LIMFUNC1:def 5
for r being Real ex n being Nat st
for m being Nat st n <= m holds
seq . m < r;

end;

:: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def 4 :

:: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def 5 :

theorem :: LIMFUNC1:31

canceled;

theorem :: LIMFUNC1:32

canceled;

theorem :: LIMFUNC1:33

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
ex n being Nat st
for m being Nat st n <= m holds
seq ^\ m is_not_0

proof end;

theorem Th34: :: LIMFUNC1:34

for k being Nat
for seq being Real_Sequence holds
( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) )

proof end;

theorem Th35: :: LIMFUNC1:35

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 + seq2 is divergent_to+infty

proof end;

theorem Th36: :: LIMFUNC1:36

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is bounded_below holds
seq1 + seq2 is divergent_to+infty

proof end;

theorem Th37: :: LIMFUNC1:37

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th38: :: LIMFUNC1:38

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 + seq2 is divergent_to-infty

proof end;

theorem Th39: :: LIMFUNC1:39

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is bounded_above holds
seq1 + seq2 is divergent_to-infty

proof end;

theorem Th40: :: LIMFUNC1:40

for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to+infty & r > 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to+infty & r < 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to+infty & r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )

proof end;

theorem Th41: :: LIMFUNC1:41

for seq being Real_Sequence
for r being Real holds
( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to-infty & r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )

proof end;

theorem :: LIMFUNC1:42

for seq being Real_Sequence holds
( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) )

proof end;

theorem :: LIMFUNC1:43

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is divergent_to-infty holds
seq - seq1 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:44

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds
seq - seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:45

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is convergent holds
seq + seq1 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:46

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds
seq + seq1 is divergent_to-infty

proof end;

theorem Th47: :: LIMFUNC1:47

for seq being Real_Sequence st ( for n being Nat holds seq . n = n ) holds
seq is divergent_to+infty

proof end;

set s1 = incl NAT ;

Lm6: for n being Nat holds (incl NAT ) . n = n
by FUNCT_1:35;

theorem Th48: :: LIMFUNC1:48

for seq being Real_Sequence st ( for n being Nat holds seq . n = - n ) holds
seq is divergent_to-infty

proof end;

theorem Th49: :: LIMFUNC1:49

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( for n being Nat holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem :: LIMFUNC1:50

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & ex r being Real st
( 0 < r & ( for n being Nat holds seq2 . n >= r ) ) holds
seq1 (#) seq2 is divergent_to-infty

proof end;

theorem Th51: :: LIMFUNC1:51

for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th52: :: LIMFUNC1:52

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
abs seq is divergent_to+infty

proof end;

theorem Th53: :: LIMFUNC1:53

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is subsequence of seq holds
seq1 is divergent_to+infty

proof end;

theorem Th54: :: LIMFUNC1:54

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is subsequence of seq holds
seq1 is divergent_to-infty

proof end;

theorem :: LIMFUNC1:55

for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 holds
seq1 (#) seq2 is divergent_to+infty

proof end;

theorem Th56: :: LIMFUNC1:56

for seq being Real_Sequence st seq is non-decreasing & not seq is bounded_above holds
seq is divergent_to+infty

proof end;

theorem Th57: :: LIMFUNC1:57

for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds
seq is divergent_to-infty

proof end;

theorem :: LIMFUNC1:58

for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds
seq is divergent_to+infty

proof end;

theorem :: LIMFUNC1:59

for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds
seq is divergent_to-infty

proof end;

theorem :: LIMFUNC1:60

for seq being Real_Sequence holds
( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty )

proof end;

theorem Th61: :: LIMFUNC1:61

for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds
( seq " is convergent & lim (seq " ) = 0 )

proof end;

theorem Th62: :: LIMFUNC1:62

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & ex k being Nat st
for n being Nat st k <= n holds
0 < seq . n holds
seq " is divergent_to+infty

proof end;

theorem Th63: :: LIMFUNC1:63

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & ex k being Nat st
for n being Nat st k <= n holds
seq . n < 0 holds
seq " is divergent_to-infty

proof end;

theorem Th64: :: LIMFUNC1:64

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is non-decreasing holds
seq " is divergent_to-infty

proof end;

theorem Th65: :: LIMFUNC1:65

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is non-increasing holds
seq " is divergent_to+infty

proof end;

theorem :: LIMFUNC1:66

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is increasing holds
seq " is divergent_to-infty

proof end;

theorem :: LIMFUNC1:67

for seq being Real_Sequence st seq is_not_0 & seq is convergent & lim seq = 0 & seq is decreasing holds
seq " is divergent_to+infty

proof end;

theorem :: LIMFUNC1:68

for seq1, seq2 being Real_Sequence st seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) & seq2 is_not_0 holds
( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 )

proof end;

theorem Th69: :: LIMFUNC1:69

for seq, seq1 being Real_Sequence st seq is divergent_to+infty & ( for n being Nat holds seq . n <= seq1 . n ) holds
seq1 is divergent_to+infty

proof end;

theorem Th70: :: LIMFUNC1:70

for seq, seq1 being Real_Sequence st seq is divergent_to-infty & ( for n being Nat holds seq1 . n <= seq . n ) holds
seq1 is divergent_to-infty

proof end;

definition

let f be PartFunc of REAL , REAL ;
attr f is convergent_in+infty means :Def6: :: LIMFUNC1:def 6
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f * seq is convergent & lim (f * seq) = g ) );
attr f is divergent_in+infty_to+infty means :Def7: :: LIMFUNC1:def 7
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f * seq is divergent_to+infty ) );
attr f is divergent_in+infty_to-infty means :Def8: :: LIMFUNC1:def 8
( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f * seq is divergent_to-infty ) );
attr f is convergent_in-infty means :Def9: :: LIMFUNC1:def 9
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f * seq is convergent & lim (f * seq) = g ) );
attr f is divergent_in-infty_to+infty means :Def10: :: LIMFUNC1:def 10
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f * seq is divergent_to+infty ) );
attr f is divergent_in-infty_to-infty means :Def11: :: LIMFUNC1:def 11
( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
f * seq is divergent_to-infty ) );

end;

:: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def 6 :

:: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def 7 :

:: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def 8 :

:: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def 9 :

:: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def 10 :

:: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def 11 :

theorem :: LIMFUNC1:71

canceled;

theorem :: LIMFUNC1:72

canceled;

theorem :: LIMFUNC1:73

canceled;

theorem :: LIMFUNC1:74

canceled;

theorem :: LIMFUNC1:75

canceled;

theorem :: LIMFUNC1:76

canceled;

theorem :: LIMFUNC1:77

for f being PartFunc of REAL , REAL holds
( f is convergent_in+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )

proof end;

theorem :: LIMFUNC1:78

for f being PartFunc of REAL , REAL holds
( f is convergent_in-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 ) )

proof end;

theorem :: LIMFUNC1:79

for f being PartFunc of REAL , REAL holds
( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) ) )

proof end;

theorem :: LIMFUNC1:80

for f being PartFunc of REAL , REAL holds
( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
f . r1 < g ) ) )

proof end;

theorem :: LIMFUNC1:81

for f being PartFunc of REAL , REAL holds
( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
g < f . r1 ) ) )

proof end;

theorem :: LIMFUNC1:82

for f being PartFunc of REAL , REAL holds
( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) ) )

proof end;

theorem :: LIMFUNC1:83

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to+infty & f1 (#) f2 is divergent_in+infty_to+infty )

proof end;

theorem :: LIMFUNC1:84

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in+infty_to-infty & f1 (#) f2 is divergent_in+infty_to+infty )

proof end;

theorem :: LIMFUNC1:85

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to+infty & f1 (#) f2 is divergent_in-infty_to+infty )

proof end;

theorem :: LIMFUNC1:86

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is divergent_in-infty_to-infty & f1 (#) f2 is divergent_in-infty_to+infty )

proof end;

theorem :: LIMFUNC1:87

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 is_bounded_below_on right_open_halfline r holds
f1 + f2 is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:88

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (right_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:89

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 is_bounded_below_on left_open_halfline r holds
f1 + f2 is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:90

for f1, f2 being PartFunc of REAL , REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st
( 0 < r & ( for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds
r <= f2 . g ) ) holds
f1 (#) f2 is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:91

for f being PartFunc of REAL , REAL
for r being Real holds
( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) )

proof end;

theorem :: LIMFUNC1:92

for f being PartFunc of REAL , REAL
for r being Real holds
( ( f is divergent_in-infty_to+infty & r > 0 implies r (#) f is divergent_in-infty_to+infty ) & ( f is divergent_in-infty_to+infty & r < 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r > 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r < 0 implies r (#) f is divergent_in-infty_to+infty ) )

proof end;

theorem :: LIMFUNC1:93

for f being PartFunc of REAL , REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) holds
abs f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:94

for f being PartFunc of REAL , REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) holds
abs f is divergent_in-infty_to+infty

proof end;

theorem Th95: :: LIMFUNC1:95

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_non_decreasing_on right_open_halfline r & not f is_bounded_above_on right_open_halfline r ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:96

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_increasing_on right_open_halfline r & not f is_bounded_above_on right_open_halfline r ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem Th97: :: LIMFUNC1:97

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_non_increasing_on right_open_halfline r & not f is_bounded_below_on right_open_halfline r ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:98

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_decreasing_on right_open_halfline r & not f is_bounded_below_on right_open_halfline r ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem Th99: :: LIMFUNC1:99

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_non_increasing_on left_open_halfline r & not f is_bounded_above_on left_open_halfline r ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:100

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_decreasing_on left_open_halfline r & not f is_bounded_above_on left_open_halfline r ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem Th101: :: LIMFUNC1:101

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_non_decreasing_on left_open_halfline r & not f is_bounded_below_on left_open_halfline r ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:102

for f being PartFunc of REAL , REAL st ex r being Real st
( f is_increasing_on left_open_halfline r & not f is_bounded_below_on left_open_halfline r ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) holds
f is divergent_in-infty_to-infty

proof end;

theorem Th103: :: LIMFUNC1:103

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem Th104: :: LIMFUNC1:104

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem Th105: :: LIMFUNC1:105

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem Th106: :: LIMFUNC1:106

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex r being Real st
( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:107

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in+infty_to+infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:108

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in+infty_to-infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:109

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in-infty_to+infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f1 . g <= f . g ) ) holds
f is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:110

for f1, f being PartFunc of REAL , REAL st f1 is divergent_in-infty_to-infty & ex r being Real st
( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds
f . g <= f1 . g ) ) holds
f is divergent_in-infty_to-infty

proof end;

definition

let f be PartFunc of REAL , REAL ;
assume A1: f is convergent_in+infty ;
func lim_in+infty f -> Real means :Def12: :: LIMFUNC1:def 12
for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f * seq is convergent & lim (f * seq) = it );
existence by A1, Def6;
uniqueness

proof end;

end;

:: deftheorem Def12 defines lim_in+infty LIMFUNC1:def 12 :

definition

let f be PartFunc of REAL , REAL ;
assume A1: f is convergent_in-infty ;
func lim_in-infty f -> Real means :Def13: :: LIMFUNC1:def 13
for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f * seq is convergent & lim (f * seq) = it );
existence by A1, Def9;
uniqueness

proof end;

end;

:: deftheorem Def13 defines lim_in-infty LIMFUNC1:def 13 :

theorem :: LIMFUNC1:111

canceled;

theorem :: LIMFUNC1:112

canceled;

theorem :: LIMFUNC1:113

for f being PartFunc of REAL , REAL
for g being Real st f is convergent_in-infty holds
( lim_in-infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 )

proof end;

theorem :: LIMFUNC1:114

for f being PartFunc of REAL , REAL
for g being Real st f is convergent_in+infty holds
( lim_in+infty f = g iff for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
abs ((f . r1) - g) < g1 )

proof end;

theorem Th115: :: LIMFUNC1:115

for f being PartFunc of REAL , REAL
for r being Real st f is convergent_in+infty holds
( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )

proof end;

theorem Th116: :: LIMFUNC1:116

for f being PartFunc of REAL , REAL st f is convergent_in+infty holds
( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) )

proof end;

theorem Th117: :: LIMFUNC1:117

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) holds
( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:118

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 - f2) ) ) holds
( f1 - f2 is convergent_in+infty & lim_in+infty (f1 - f2) = (lim_in+infty f1) - (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:119

for f being PartFunc of REAL , REAL st f is convergent_in+infty & f " {0} = {} & lim_in+infty f <> 0 holds
( f ^ is convergent_in+infty & lim_in+infty (f ^ ) = (lim_in+infty f) " )

proof end;

theorem :: LIMFUNC1:120

for f being PartFunc of REAL , REAL st f is convergent_in+infty holds
( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) )

proof end;

theorem Th121: :: LIMFUNC1:121

for f being PartFunc of REAL , REAL st f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^ ) = (lim_in+infty f) " )

proof end;

theorem Th122: :: LIMFUNC1:122

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) )

proof end;

theorem :: LIMFUNC1:123

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2 <> 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in+infty & lim_in+infty (f1 / f2) = (lim_in+infty f1) / (lim_in+infty f2) )

proof end;

theorem Th124: :: LIMFUNC1:124

for f being PartFunc of REAL , REAL
for r being Real st f is convergent_in-infty holds
( r (#) f is convergent_in-infty & lim_in-infty (r (#) f) = r * (lim_in-infty f) )

proof end;

theorem Th125: :: LIMFUNC1:125

for f being PartFunc of REAL , REAL st f is convergent_in-infty holds
( - f is convergent_in-infty & lim_in-infty (- f) = - (lim_in-infty f) )

proof end;

theorem Th126: :: LIMFUNC1:126

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) holds
( f1 + f2 is convergent_in-infty & lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:127

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 - f2) ) ) holds
( f1 - f2 is convergent_in-infty & lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:128

for f being PartFunc of REAL , REAL st f is convergent_in-infty & f " {0} = {} & lim_in-infty f <> 0 holds
( f ^ is convergent_in-infty & lim_in-infty (f ^ ) = (lim_in-infty f) " )

proof end;

theorem :: LIMFUNC1:129

for f being PartFunc of REAL , REAL st f is convergent_in-infty holds
( abs f is convergent_in-infty & lim_in-infty (abs f) = abs (lim_in-infty f) )

proof end;

theorem Th130: :: LIMFUNC1:130

for f being PartFunc of REAL , REAL st f is convergent_in-infty & lim_in-infty f <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^ ) = (lim_in-infty f) " )

proof end;

theorem Th131: :: LIMFUNC1:131

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) holds
( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = (lim_in-infty f1) * (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:132

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2 <> 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 / f2) ) ) holds
( f1 / f2 is convergent_in-infty & lim_in-infty (f1 / f2) = (lim_in-infty f1) / (lim_in-infty f2) )

proof end;

theorem :: LIMFUNC1:133

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & lim_in+infty f1 = 0 & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 is_bounded_on right_open_halfline r holds
( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = 0 )

proof end;

theorem :: LIMFUNC1:134

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st
( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 is_bounded_on left_open_halfline r holds
( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 )

proof end;

theorem Th135: :: LIMFUNC1:135

for f1, f2, f being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )

proof end;

theorem :: LIMFUNC1:136

for f1, f2, f being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ex r being Real st
( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )

proof end;

theorem Th137: :: LIMFUNC1:137

proof end;

theorem :: LIMFUNC1:138

for f1, f2, f being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ex r being Real st
( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )

proof end;

theorem :: LIMFUNC1:139

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ex r being Real st
( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in+infty f1 <= lim_in+infty f2

proof end;

theorem :: LIMFUNC1:140

for f1, f2 being PartFunc of REAL , REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) holds
lim_in-infty f1 <= lim_in-infty f2

proof end;

theorem :: LIMFUNC1:141

for f being PartFunc of REAL , REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in+infty & lim_in+infty (f ^ ) = 0 )

proof end;

theorem :: LIMFUNC1:142

for f being PartFunc of REAL , REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) holds
( f ^ is convergent_in-infty & lim_in-infty (f ^ ) = 0 )

proof end;

theorem :: LIMFUNC1:143

for f being PartFunc of REAL , REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:144

for f being PartFunc of REAL , REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st
( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:145

for f being PartFunc of REAL , REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 <= f . g holds
f ^ is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:146

for f being PartFunc of REAL , REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st
( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g <= 0 holds
f ^ is divergent_in-infty_to-infty

proof end;

theorem :: LIMFUNC1:147

for f being PartFunc of REAL , REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in+infty_to+infty

proof end;

theorem :: LIMFUNC1:148

for f being PartFunc of REAL , REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (right_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in+infty_to-infty

proof end;

theorem :: LIMFUNC1:149

for f being PartFunc of REAL , REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
0 < f . g holds
f ^ is divergent_in-infty_to+infty

proof end;

theorem :: LIMFUNC1:150

for f being PartFunc of REAL , REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st
for g being Real st g in (dom f) /\ (left_open_halfline r) holds
f . g < 0 holds
f ^ is divergent_in-infty_to-infty

proof end;