Copyright (c) 1990 Association of Mizar Users
environ
vocabulary SUPINF_1, ARYTM_1, ARYTM_3, RLVECT_1, BOOLE, ORDINAL2, SEQ_2,
FUNCT_1, RELAT_1, LATTICES, CARD_4, FUNCT_4, FUNCOP_1, SUPINF_2;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SUPINF_1,
RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, NAT_1, CARD_4;
constructors REAL_1, SUPINF_1, NAT_1, CARD_4, FUNCOP_1, FUNCT_4, MEMBERED,
XBOOLE_0;
clusters SUPINF_1, RELSET_1, FUNCOP_1, FUNCT_1, ARYTM_3, FINSET_1, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SUPINF_1, XBOOLE_0;
theorems AXIOMS, TARSKI, REAL_1, SUPINF_1, FUNCT_1, FUNCT_2, NAT_1, RELSET_1,
CARD_4, SUBSET_1, FUNCT_4, FUNCOP_1, RELAT_1, ZFMISC_1, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes SUPINF_1, FUNCT_2, RECDEF_1, NAT_1;
begin :: operations " + "," - " in R_eal numbers
definition
func 0. -> R_eal equals
:Def1: 0;
correctness by SUPINF_1:10;
end;
definition
let x,y be R_eal;
func x + y -> R_eal means
:Def2:
ex a,b being Real st x = a & y = b & it = a + b if x in REAL & y in REAL,
it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty,
it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty
otherwise it = 0.;
existence
proof
thus x in REAL & y in REAL implies
ex IT being R_eal, a,b being Real st x = a & y = b & IT = a + b
proof assume x in REAL & y in REAL;
then reconsider a = x, b = y as Real;
a+b is R_eal by SUPINF_1:10;
hence thesis;
end;
thus thesis;
end;
uniqueness;
consistency by SUPINF_1:2,6;
commutativity;
end;
theorem Th1:
for x,y being R_eal holds
for a,b being Real holds
(x = a & y = b) implies (x + y = a + b)
proof let x,y be R_eal, a,b be Real;
assume
A1:x = a & y = b;
then ex a,b being Real st x = a & y = b & x + y = a + b by Def2;
hence thesis by A1;
end;
theorem Th2:
for x being R_eal holds
x in REAL or x = +infty or x = -infty
proof let x be R_eal;
x in REAL or x in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:def 2;
hence x in REAL or x = +infty or x = -infty by TARSKI:def 2;
end;
definition
let x be R_eal;
func - x -> R_eal means
:Def3: ex a being Real st x = a & it = - a if x in REAL,
it = -infty if x = +infty
otherwise it = +infty;
existence
proof
x in REAL implies ex Z being R_eal st
(ex a being Real st (x = a & Z = - a))
proof
assume x in REAL;
then reconsider x as Real;
reconsider Z = - x as R_eal by SUPINF_1:10;
take Z;
thus thesis;
end;
hence thesis;
end;
uniqueness;
consistency by SUPINF_1:2;
involutiveness
proof let y,x be R_eal such that
A1: x in REAL implies ex a being Real st x = a & y = - a and
A2: x = +infty implies y = -infty and
A3: not x in REAL & x <> +infty implies y = +infty;
thus y in REAL implies ex a being Real st y = a & x = - a
proof assume y in REAL;
then consider a being Real such that
A4: x = a and
A5: y = - a by A1,A2,A3,SUPINF_1:2,6;
take -a;
thus thesis by A4,A5;
end;
thus y = +infty implies x = -infty by A1,A2,Th2,SUPINF_1:2;
thus thesis by A1,A3;
end;
end;
definition
let x,y be R_eal;
func x - y -> R_eal equals
:Def4: x + -y;
coherence;
end;
theorem Th3:
for x being R_eal, a being Real st x = a holds - x = - a
proof
let x be R_eal, a be Real;
assume
A1: x = a;
then ex a being Real st x = a & - x = - a by Def3;
hence thesis by A1;
end;
theorem Th4:
- -infty = +infty
proof
thus thesis by Def3,SUPINF_1:6,14;
end;
theorem Th5:
for x,y being R_eal holds
for a,b being Real holds
(x = a & y = b) implies (x - y = a - b)
proof
let x,y be R_eal;
let a,b be Real;
assume
A1: x = a;
assume y = b;
then A2: -y = -b by Th3;
thus x - y = x + -y by Def4
.= a + -b by A1,A2,Th1
.= a - b by XCMPLX_0:def 8;
end;
theorem Th6:
for x being R_eal holds
x <> +infty implies +infty - x = +infty & x - +infty = -infty
proof
let x be R_eal;
assume
A1: x <> +infty;
then A2: -x <> -infty by Th4;
thus +infty - x = +infty + -x by Def4
.= +infty by A2,Def2;
- +infty = -infty by Def3;
hence x - +infty = x + -infty by Def4
.= -infty by A1,Def2;
end;
theorem Th7:
for x being R_eal holds
x <> -infty implies -infty - x = -infty & x - -infty = +infty
proof
let x be R_eal;
assume
A1: x <> -infty;
A2: now assume -x = +infty;
then --x = -infty by Def3;
hence contradiction by A1;
end;
thus -infty - x = -infty + -x by Def4
.= -infty by A2,Def2;
thus x - -infty = x + +infty by Def4,Th4
.= +infty by A1,Def2;
end;
theorem Th8:
for x,s being R_eal holds
x + s = +infty implies x = +infty or s = +infty
proof
let x,s be R_eal;
assume
A1:x + s = +infty;
assume
A2:not (x = +infty or s = +infty);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = -infty) or
(x = -infty & s in REAL) or (x = -infty & s = -infty) by A2,TARSKI:def 2;
not(x in REAL & s in REAL)
proof
assume x in REAL & s in REAL;
then reconsider a = x, b = s as Real;
x + s = a + b by Th1;
hence thesis by A1,SUPINF_1:2;
end;
hence thesis by A1,A2,A3,Def2;
end;
theorem Th9:
for x,s being R_eal holds
x + s = -infty implies (x = -infty or s = -infty)
proof
let x,s be R_eal;
assume
A1:x + s = -infty;
assume
A2:not (x = -infty or s = -infty);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = +infty) or
(x = +infty & s in REAL) or (x = +infty & s = +infty) by A2,TARSKI:def 2;
not(x in REAL & s in REAL)
proof
assume x in REAL & s in REAL;
then reconsider a = x, b = s as Real;
x + s = a + b by Th1;
hence thesis by A1,SUPINF_1:6;
end;
hence thesis by A1,A2,A3,Def2;
end;
theorem Th10:
for x,s being R_eal holds
x - s = +infty implies (x = +infty or s = -infty)
proof
let x,s be R_eal;
assume
A1:x - s = +infty;
assume
A2:not (x = +infty or s = -infty);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = +infty) or
(x = -infty & s in REAL) or (x = -infty & s = +infty) by A2,TARSKI:def 2;
not (x in REAL & s in REAL)
proof
assume x in REAL & s in REAL;
then consider a,b being Real such that
A4:a = x & b = s;
x - s = a - b by A4,Th5;
hence thesis by A1,SUPINF_1:2;
end;
hence thesis by A1,A2,A3,Th6,Th7;
end;
theorem Th11:
for x,s being R_eal holds
x - s = -infty implies (x = -infty or s = +infty)
proof
let x,s be R_eal;
assume
A1:x - s = -infty;
assume
A2:not (x = -infty or s = +infty);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(x in REAL & s in REAL) or (x in REAL & s = -infty) or
(x = +infty & s in REAL) or (x = +infty & s = -infty) by A2,TARSKI:def 2;
not(x in REAL & s in REAL)
proof
assume
x in REAL & s in REAL;
then consider a,b being Real such that
A4:a = x & b = s;
x - s = a - b by A4,Th5;
hence thesis by A1,SUPINF_1:6;
end;
hence thesis by A1,A2,A3,Th6,Th7;
end;
theorem Th12:
for x,s being R_eal holds
(not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
x + s in REAL) implies (x in REAL & s in REAL)
proof
let x,s be R_eal;
assume
A1:(not ((x = +infty & s = -infty) or (x = -infty & s = +infty
)) & x + s in REAL);
assume
A2:not (x in REAL & s in REAL);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then (x in REAL or x = -infty or x = +infty) &
(s in REAL or s = -infty or s = +infty) by TARSKI:def 2;
hence thesis by A1,A2,Def2;
end;
theorem Th13:
for x,s being R_eal holds
(not ((x = +infty & s = +infty) or (x = -infty & s = -infty)) &
x - s in REAL) implies (x in REAL & s in REAL)
proof
let x,s be R_eal;
assume
A1:(not ((x = +infty & s = +infty) or (x = -infty & s = -infty
)) & x - s in REAL);
assume
A2:not (x in REAL & s in REAL);
(x in REAL or x in {-infty,+infty}) & (s in REAL or s in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then (x in REAL or x = -infty or x = +infty) &
(s in REAL or s = -infty or s = +infty) by TARSKI:def 2;
hence thesis by A1,A2,Th6,Th7,SUPINF_1:2,6;
end;
theorem Th14:
for x,y,s,t being R_eal holds
not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
not ((y = +infty & t = -infty) or (y = -infty & t = +infty
)) & x <=' y & s <=' t implies
x + s <=' y + t
proof
let x,y,s,t be R_eal;
assume
A1:not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
not ((y = +infty & t = -infty) or (y = -infty & t = +infty
)) & x <=' y & s <=' t;
consider a,b being R_eal such that
A2:a = x + s & b = y + t;
(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(a in REAL & b in REAL) or (a in REAL & b = +infty) or
(a in REAL & b = -infty) or
(a = +infty & b in REAL) or (a = +infty & b = +infty) or (a = +infty & b =
-infty) or
(a = -infty & b in REAL) or (a = -infty & b = +infty) or (a = -infty & b =
-infty) by TARSKI:def 2;
A4:(a in REAL & b in REAL) implies a <=' b
proof
assume a in REAL & b in REAL;
then A5:x is Real & y is Real & s is Real & t is Real by A1,A2,Th12;
then A6:ex Ox,Oy being Real st (Ox = x & Oy = y & Ox <= Oy) by A1,SUPINF_1:
16;
ex Os,Ot being Real st (Os = s & Ot = t & Os <= Ot) by A1,A5,SUPINF_1:16;
then consider Ox,Oy,Os,Ot being Real such that
A7:Ox = x & Oy = y & Os = s & Ot = t & Ox <= Oy & Os <= Ot by A6;
A8:Ox + Os <= Os + Oy by A7,AXIOMS:24;
Os + Oy <= Ot + Oy by A7,AXIOMS:24;
then A9:Ox + Os <= Oy + Ot by A8,AXIOMS:22;
x + s = Ox + Os & y + t = Oy + Ot by A7,Th1;
hence thesis by A2,A9,SUPINF_1:16;
end;
A10:(a in REAL & b = -infty) implies a <=' b
proof
assume a in REAL & b = -infty;
then y = -infty or t = -infty by A2,Th9;
then x = -infty or s = -infty by A1,SUPINF_1:23;
then a = -infty by A1,A2,Def2;
hence thesis by SUPINF_1:21;
end;
A11:(a = +infty & b in REAL) implies a <=' b
proof
assume a = +infty & b in REAL;
then x = +infty or s = +infty by A2,Th8;
then y = +infty or t = +infty by A1,SUPINF_1:24;
then b = +infty by A1,A2,Def2;
hence thesis by SUPINF_1:20;
end;
not(a = +infty & b = -infty)
proof
assume
A12:a = +infty & b = -infty;
then A13:y = -infty or t = -infty by A2,Th9;
x = +infty or s = +infty by A2,A12,Th8;
hence thesis by A1,A13,SUPINF_1:14,24;
end;
hence thesis by A2,A3,A4,A10,A11,SUPINF_1:20,21;
end;
theorem
for x,y,s,t being R_eal holds
not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) &
not ((y = +infty & s = +infty) or (y = -infty & s = -infty
)) & x <=' y & s <=' t implies
x - t <=' y - s
proof
let x,y,s,t be R_eal;
assume
A1:not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) &
not ((y = +infty & s = +infty) or (y = -infty & s = -infty
)) & x <=' y & s <=' t;
consider a,b being R_eal such that
A2:a = x - t & b = y - s;
(a in REAL or a in {-infty,+infty}) & (b in REAL or b in {-infty,+infty
}) by SUPINF_1:def 6,XBOOLE_0:def 2;
then A3:(a in REAL & b in REAL) or (a in REAL & b = +infty) or
(a in REAL & b = -infty) or
(a = +infty & b in REAL) or (a = +infty & b = +infty) or (a = +infty & b =
-infty) or
(a = -infty & b in REAL) or (a = -infty & b = +infty) or (a = -infty & b =
-infty) by TARSKI:def 2;
A4:(a in REAL & b in REAL) implies a <=' b
proof
assume a in REAL & b in REAL;
then A5:x is Real & y is Real & s is Real & t is Real by A1,A2,Th13;
then A6:ex Ox,Oy being Real st (Ox = x & Oy = y & Ox <= Oy) by A1,SUPINF_1:
16;
ex Os,Ot being Real st (Os = s & Ot = t & Os <= Ot) by A1,A5,SUPINF_1:16;
then consider Ox,Oy,Os,Ot being Real such that
A7:Ox = x & Oy = y & Os = s & Ot = t & Ox <= Oy & Os <= Ot by A6;
A8: - Ot <= - Os by A7,REAL_1:50;
Ox + (- Ot) = Ox - Ot & Oy + (- Os) = Oy - Os by XCMPLX_0:def 8;
then A9:Ox - Ot <= Oy - Os by A7,A8,REAL_1:55;
x - t = Ox - Ot & y - s = Oy - Os by A7,Th5;
hence thesis by A2,A9,SUPINF_1:16;
end;
A10:(a in REAL & b = -infty) implies a <=' b
proof
assume
A11:a in REAL & b = -infty;
then A12:x in REAL & t in REAL by A1,A2,Th13;
y = -infty or s = +infty by A2,A11,Th11;
hence thesis by A1,A12,SUPINF_1:2,6,23,24;
end;
A13:(a = +infty & b in REAL) implies a <=' b
proof
assume
A14:a = +infty & b in REAL;
then A15:y in REAL & s in REAL by A1,A2,Th13;
x = +infty or t = -infty by A2,A14,Th10;
hence thesis by A1,A15,SUPINF_1:2,6,23,24;
end;
not(a = +infty & b = -infty)
proof
assume
A16:a = +infty & b = -infty;
then A17:y = -infty or s = +infty by A2,Th11;
x = +infty or t = -infty by A2,A16,Th10;
hence thesis by A1,A17,SUPINF_1:14,23,24;
end;
hence thesis by A2,A3,A4,A10,A13,SUPINF_1:20,21;
end;
Lm1:
for x being R_eal holds
-x in REAL iff x in REAL
proof let x be R_eal;
hereby assume -x in REAL;
then reconsider a = -x as Real;
-a in REAL;
then --x in REAL by Th3;
hence x in REAL;
end;
assume x in REAL;
then reconsider a = x as Real;
-x = -a by Th3;
hence thesis;
end;
Lm2:
for x,y being R_eal holds
x <=' y implies - y <=' - x
proof
let x,y be R_eal;
assume
A1: x <=' y;
per cases;
case that
A2: -y in REAL and
A3: -x in REAL;
A4: y in REAL by A2,Lm1;
then consider b being Real such that
A5: y = b and
A6: -y = - b by Def3;
A7: x in REAL by A3,Lm1;
then consider a being Real such that
A8: x = a and
A9: -x = - a by Def3;
take -b,-a;
thus -b = -y & -a = -x by A6,A9;
ex p,q being Real st p = x & q = y & p <= q by A1,A4,A7,SUPINF_1:def 7;
hence -b <= -a by A5,A8,REAL_1:50;
case not(-y in REAL & -x in REAL);
then not(y in REAL & x in REAL) by Lm1;
then x = -infty or y = +infty by A1,SUPINF_1:def 7;
hence -y = -infty or -x = +infty by Th4;
end;
theorem Th16:
for x,y being R_eal holds
x <=' y iff - y <=' - x
proof let x,y be R_eal;
thus x <=' y implies - y <=' - x by Lm2;
- y <=' - x implies --x <=' --y by Lm2;
hence thesis;
end;
theorem
for x,y being R_eal holds
x <' y iff - y <' - x by Th16;
theorem Th18:
for x being R_eal holds x + 0. = x & 0. + x = x
proof
let x be R_eal;
A1:x in REAL or x = -infty or x = +infty by Th2;
A2:x in REAL implies x + 0. =x & 0. + x = x
proof
assume x in REAL;
then reconsider a = x as Real;
x + 0. = a + 0 by Def1,Def2
.= x;
hence thesis;
end;
not 0. = -infty & not 0. = +infty by Def1,SUPINF_1:2,6;
hence thesis by A1,A2,Def2;
end;
theorem
-infty <'0. & 0. <'+infty
proof
A1:-infty <=' 0. & 0. <=' +infty by SUPINF_1:20,21;
not 0. = +infty & not 0. = -infty by Def1,SUPINF_1:2,6;
hence thesis by A1,SUPINF_1:22;
end;
theorem Th20:
for x,y,z being R_eal holds
0. <=' z & 0. <=' x & y = x + z implies x <=' y
proof
let x,y,z be R_eal;
assume
A1:0. <=' z & 0. <=' x & y = x + z;
not 0. = -infty & not 0. = +infty by Def1,SUPINF_1:2,6;
then A2:not z = -infty & not x = -infty by A1,SUPINF_1:23;
x in REAL \/ {-infty,+infty} & z in REAL \/
{-infty,+infty} by SUPINF_1:def 5;
then A3: (x in REAL or x in {-infty,+infty}) & (z in REAL or
z in {-infty,+infty}) by XBOOLE_0:def 2;
A4:z in REAL implies x <=' y
proof
assume
A5:z in REAL;
A6:x in REAL implies x <=' y
proof
assume
A7:x in REAL;
consider c,b being Real such that
A8:c = 0. & b = z & c <= b by A1,A5,Def1,SUPINF_1:16;
consider a being Real such that
A9:a = x by A7;
A10:y = a + b by A1,A8,A9,Th1;
then consider d being Real such that
A11:d = y;
-b <= 0 by A8,Def1,REAL_1:26,50;
then d + (-b) <= 0 + d by AXIOMS:24;
then a + (b + (-b)) <= d by A10,A11,XCMPLX_1:1;
then a + 0 <= d by XCMPLX_0:def 6;
hence thesis by A9,A11,SUPINF_1:16;
end;
x = +infty implies x <=' y by A1,A2,Def2;
hence thesis by A2,A3,A6,TARSKI:def 2;
end;
z = +infty implies x <=' y
proof
assume z = +infty;
then y = +infty by A1,A2,Def2;
hence thesis by SUPINF_1:20;
end;
hence thesis by A2,A3,A4,TARSKI:def 2;
end;
Lm3:
for x,y,s,t being R_eal holds
0. <=' x & 0. <=' s & x <=' y & s <=' t implies
x + s <=' y + t
proof
let x,y,s,t be R_eal;
assume
A1:0. <=' x & 0. <=' s & x <=' y & s <=' t;
not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
not ((y = +infty & t = -infty) or (y = -infty & t = +infty))
proof
0. <=' y & 0. <=' t by A1,SUPINF_1:29;
hence thesis by A1,Def1,SUPINF_1:17;
end;
hence thesis by A1,Th14;
end;
theorem Th21:
for x being R_eal holds x in NAT implies 0. <=' x
proof
let x be R_eal;
assume
x in NAT;
then reconsider x as Nat;
0 <= x by NAT_1:18;
hence thesis by Def1,SUPINF_1:16;
end;
::
:: operations " + "," - " in SUBDOMAIN of ExtREAL
::
definition
let X,Y be non empty Subset of ExtREAL;
func X + Y -> Subset of ExtREAL means
:Def5:for z being R_eal holds
z in it iff ex x,y being R_eal st (x in X & y in Y & z = x + y);
existence
proof
defpred P[R_eal] means
ex x,y being R_eal st x in X & y in Y & $1 = x + y;
consider Z being Subset of REAL \/ {-infty,+infty} such that
A1:for z being R_eal holds z in Z iff P[z] from SepR_eal;
reconsider Z as Subset of ExtREAL by SUPINF_1:def 6;
consider x being Element of X;
consider y being Element of Y;
reconsider x,y as R_eal;
x + y = x + y;
then reconsider Z as non empty set by A1;
reconsider Z as non empty Subset of ExtREAL;
take Z;
thus thesis by A1;
end;
uniqueness
proof
let Z1,Z2 be Subset of ExtREAL such that
A2:for z being R_eal holds
z in Z1 iff ex x,y being R_eal st (x in X & y in Y & z = x + y) and
A3:for z being R_eal holds
z in Z2 iff ex x,y being R_eal st (x in X & y in Y & z = x + y);
for z being set holds
z in Z1 iff z in Z2
proof
let z be set;
hereby assume
A4:z in Z1;
then reconsider z' = z as R_eal;
ex x,y being R_eal st (x in X & y in Y & z' = x + y) by A2,A4;
hence z in Z2 by A3;
end;
assume
A5:z in Z2;
then reconsider z as R_eal;
ex x,y being R_eal st (x in X & y in Y & z = x + y) by A3,A5;
hence thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X,Y be non empty Subset of ExtREAL;
cluster X + Y -> non empty;
coherence
proof
consider x being Element of X;
consider y being Element of Y;
reconsider x,y as R_eal;
x + y = x + y;
hence thesis by Def5;
end;
end;
definition
let X be non empty Subset of ExtREAL;
func - X -> Subset of ExtREAL means
:Def6:for z being R_eal holds
z in it iff ex x being R_eal st (x in X & z = - x);
existence
proof
defpred P[R_eal] means
ex x being R_eal st x in X & $1 = - x;
consider Z being Subset of REAL \/ {-infty,+infty} such that
A1:for z being R_eal holds z in Z iff P[z] from SepR_eal;
reconsider Z as Subset of ExtREAL by SUPINF_1:def 6;
consider x being Element of X;
reconsider x as R_eal;
-x = -x;
then reconsider Z as non empty set by A1;
reconsider Z as non empty Subset of ExtREAL;
take Z;
thus thesis by A1;
end;
uniqueness
proof
let Z1,Z2 be Subset of ExtREAL such that
A2:for z being R_eal holds z in Z1 iff
ex x being R_eal st (x in X & z = - x) and
A3:for z being R_eal holds z in Z2 iff
ex x being R_eal st (x in X & z = - x);
for z being set holds z in Z1 iff z in Z2
proof
let z be set;
A4:z in Z1 implies z in Z2
proof
assume
A5:z in Z1;
then reconsider z as R_eal;
ex x being R_eal st (x in X & z = - x) by A2,A5;
hence thesis by A3;
end;
z in Z2 implies z in Z1
proof
assume
A6:z in Z2;
then reconsider z as R_eal;
ex x being R_eal st (x in X & z = - x) by A3,A6;
hence thesis by A2;
end;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X be non empty Subset of ExtREAL;
cluster - X -> non empty;
coherence
proof
consider x being Element of X;
reconsider x as R_eal;
- x = - x;
hence thesis by Def6;
end;
end;
theorem Th22:
for X being non empty Subset of ExtREAL holds
- (- X) = X
proof
let X be non empty Subset of ExtREAL;
for z being R_eal holds
z in X iff ex x being R_eal st (x in - X & z = - x)
proof
let z be R_eal;
A1:z in X implies ex x being R_eal st (x in - X & z = - x)
proof
assume
A2:z in X;
set x = - z;
A3:z = - x;
x in - X by A2,Def6;
hence thesis by A3;
end;
(ex x being R_eal st (x in - X & z = - x)) implies z in X
proof
given x being R_eal such that
A4:x in - X & z = - x;
ex a being R_eal st a in X & x = - a by A4,Def6;
hence thesis by A4;
end;
hence thesis by A1;
end;
hence thesis by Def6;
end;
theorem Th23:
for X being non empty Subset of ExtREAL holds
for z being R_eal holds
z in X iff - z in - X
proof
let X be non empty Subset of ExtREAL;
let z be R_eal;
- z in - X implies z in X
proof
assume - z in - X;
then consider x being R_eal such that
A1:x in X & - z = - x by Def6;
- (- z) = z & - (- x) = x;
hence thesis by A1;
end;
hence thesis by Def6;
end;
theorem
for X,Y being non empty Subset of ExtREAL holds
X c= Y iff - X c= - Y
proof
let X,Y be non empty Subset of ExtREAL;
hereby assume
A1:X c= Y;
thus - X c= - Y
proof
let x be set;
assume
A2:x in - X;
then reconsider x as R_eal;
- x in - (- X) by A2,Th23;
then - x in X by Th22;
then - (- x) in - Y by A1,Th23;
hence thesis;
end;
end;
assume
A3:- X c= - Y;
let x be set;
assume
A4:x in X;
then reconsider x as R_eal;
- x in - X by A4,Th23;
hence thesis by A3,Th23;
end;
theorem
for z being R_eal holds
z in REAL iff - z in REAL
proof
let z be R_eal;
A1:for z being R_eal holds z in REAL implies - z in REAL
proof
let z be R_eal;
assume
A2:z in REAL;
- z in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
then - z in REAL or - z in {-infty,+infty} by XBOOLE_0:def 2;
then - z in REAL or - z = -infty or - z = +infty by TARSKI:def 2;
then - z in REAL or - (- z) = +infty or - (- z) = -infty by Th4;
hence - z in REAL by A2,SUPINF_1:2,6;
end;
- z in REAL implies z in REAL
proof
assume - z in REAL;
then - ( - z) in REAL by A1;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th26:
for X,Y being non empty Subset of ExtREAL holds
(not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty
)) implies
sup (X + Y) <=' sup X + sup Y
proof
let X,Y be non empty Subset of ExtREAL;
assume
A1:not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty);
for z being R_eal holds
z in X + Y implies z <=' sup X + sup Y
proof
let z be R_eal;
assume
z in X + Y;
then consider x,y being R_eal such that
A2:x in X & y in Y & z = x + y by Def5;
x <=' sup X & y <=' sup Y by A2,SUPINF_1:76;
hence thesis by A1,A2,Th14;
end;
then sup X + sup Y is majorant of X + Y by SUPINF_1:def 9;
hence thesis by SUPINF_1:def 16;
end;
theorem Th27:
for X,Y being non empty Subset of ExtREAL holds
(not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty
)) implies
inf X + inf Y <=' inf (X + Y)
proof
let X,Y be non empty Subset of ExtREAL;
assume
A1:not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty);
for z being R_eal holds
z in X + Y implies inf X + inf Y <=' z
proof
let z be R_eal;
assume z in X + Y;
then consider x,y being R_eal such that
A2:x in X & y in Y & z = x + y by Def5;
inf X <=' x & inf Y <=' y by A2,SUPINF_1:79;
hence thesis by A1,A2,Th14;
end;
then inf X + inf Y is minorant of X + Y by SUPINF_1:def 10;
hence thesis by SUPINF_1:def 17;
end;
theorem
for X,Y being non empty Subset of ExtREAL holds
X is bounded_above & Y is bounded_above implies
sup (X + Y) <=' sup X + sup Y
proof
let X,Y be non empty Subset of ExtREAL;
assume
A1:X is bounded_above & Y is bounded_above;
not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty)
proof
consider UBx being majorant of X such that
A2:UBx in REAL by A1,SUPINF_1:def 11;
consider UBy being majorant of Y such that
A3:UBy in REAL by A1,SUPINF_1:def 11;
A4:not +infty in X
proof
assume +infty in X;
then +infty <=' UBx by SUPINF_1:def 9;
hence contradiction by A2,SUPINF_1:2,24;
end;
A5:not +infty in Y
proof
assume +infty in Y;
then +infty <=' UBy by SUPINF_1:def 9;
hence contradiction by A3,SUPINF_1:2,24;
end;
A6:not sup X = +infty
proof
assume sup X = +infty;
then +infty <=' UBx by SUPINF_1:def 16;
hence contradiction by A2,SUPINF_1:2,24;
end;
not sup Y = +infty
proof
assume sup Y = +infty;
then +infty <=' UBy by SUPINF_1:def 16;
hence contradiction by A3,SUPINF_1:2,24;
end;
hence thesis by A4,A5,A6;
end;
hence thesis by Th26;
end;
theorem
for X,Y being non empty Subset of ExtREAL holds
X is bounded_below & Y is bounded_below implies
inf X + inf Y <=' inf (X + Y)
proof
let X,Y be non empty Subset of ExtREAL;
assume
A1:X is bounded_below & Y is bounded_below;
not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty)
proof
consider LBx being minorant of X such that
A2:LBx in REAL by A1,SUPINF_1:def 12;
consider LBy being minorant of Y such that
A3:LBy in REAL by A1,SUPINF_1:def 12;
A4:not -infty in X
proof
assume -infty in X;
then LBx <=' -infty by SUPINF_1:def 10;
hence contradiction by A2,SUPINF_1:6,23;
end;
A5:not -infty in Y
proof
assume -infty in Y;
then LBy <=' -infty by SUPINF_1:def 10;
hence contradiction by A3,SUPINF_1:6,23;
end;
A6:not inf X = -infty
proof
assume inf X = -infty;
then LBx <=' -infty by SUPINF_1:def 17;
hence contradiction by A2,SUPINF_1:6,23;
end;
not inf Y = -infty
proof
assume inf Y = -infty;
then LBy <=' -infty by SUPINF_1:def 17;
hence contradiction by A3,SUPINF_1:6,23;
end;
hence thesis by A4,A5,A6;
end;
hence thesis by Th27;
end;
theorem Th30:
for X being non empty Subset of ExtREAL holds
for a being R_eal holds
a is majorant of X iff - a is minorant of - X
proof
let X be non empty Subset of ExtREAL;
let a be R_eal;
hereby assume
A1:a is majorant of X;
- a is minorant of - X
proof
for x being R_eal holds (x in - X implies -a <=' x)
proof
let x be R_eal;
assume x in - X;
then - x in - (- X) by Th23;
then - x in X by Th22;
then - x <=' a by A1,SUPINF_1:def 9;
then - a <=' - (- x) by Th16;
hence thesis;
end;
hence thesis by SUPINF_1:def 10;
end;
hence - a is minorant of - X;
end;
assume
A2:- a is minorant of - X;
for x being R_eal holds (x in X implies x <='a)
proof
let x be R_eal;
assume x in X;
then - x in - X by Th23;
then - a <=' - x by A2,SUPINF_1:def 10;
hence thesis by Th16;
end;
hence thesis by SUPINF_1:def 9;
end;
theorem Th31:
for X being non empty Subset of ExtREAL holds
for a being R_eal holds
a is minorant of X iff - a is majorant of - X
proof
let X be non empty Subset of ExtREAL;
let a be R_eal;
hereby assume
A1:a is minorant of X;
- a is majorant of - X
proof
for x being R_eal holds (x in - X implies x <=' - a)
proof
let x be R_eal;
assume x in - X;
then - x in - (- X) by Th23;
then - x in X by Th22;
then a <=' - x by A1,SUPINF_1:def 10;
then - (- x) <=' - a by Th16;
hence thesis;
end;
hence thesis by SUPINF_1:def 9;
end;
hence - a is majorant of - X;
end;
assume
A2:- a is majorant of - X;
for x being R_eal holds (x in X implies a <=' x)
proof
let x be R_eal;
assume x in X;
then - x in - X by Th23;
then - x <=' - a by A2,SUPINF_1:def 9;
hence thesis by Th16;
end;
hence thesis by SUPINF_1:def 10;
end;
theorem Th32:
for X being non empty Subset of ExtREAL holds
inf(- X) = - sup X
proof
let X be non empty Subset of ExtREAL;
set a = inf(- X);
set b = sup X;
A1:a is minorant of - X &
for y being R_eal holds
(y is minorant of - X implies y <=' a) by SUPINF_1:def 17;
A2:b is majorant of X &
for y being R_eal holds
(y is majorant of X implies b <=' y) by SUPINF_1:def 16;
A3:a <=' - b
proof
- a is majorant of - (- X) by A1,Th31;
then - a is majorant of X by Th22;
then b <=' - a by SUPINF_1:def 16;
then - (- a) <=' - b by Th16;
hence thesis;
end;
- b <=' a
proof
- b is minorant of - X by A2,Th30;
hence thesis by SUPINF_1:def 17;
end;
hence thesis by A3,SUPINF_1:22;
end;
theorem Th33:
for X be non empty Subset of ExtREAL holds
sup(- X) = - inf X
proof
let X be non empty Subset of ExtREAL;
set a = sup(- X);
set b = inf X;
A1:a is majorant of - X &
for y being R_eal holds
(y is majorant of - X implies a <=' y) by SUPINF_1:def 16;
A2:b is minorant of X &
for y being R_eal holds
(y is minorant of X implies y <=' b) by SUPINF_1:def 17;
A3:a <=' - b
proof
- b is majorant of - X by A2,Th31;
hence thesis by SUPINF_1:def 16;
end;
- b <=' a
proof
- a is minorant of - (- X) by A1,Th30;
then - a is minorant of X by Th22;
then - a <=' b by SUPINF_1:def 17;
then - b <=' - (-a) by Th16;
hence thesis;
end;
hence thesis by A3,SUPINF_1:22;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
redefine func rng F -> non empty Subset of ExtREAL;
coherence
proof
consider x being Element of X;
A1:F.x in rng F by FUNCT_2:6;
rng F c= Y by RELSET_1:12;
hence thesis by A1,XBOOLE_1:1;
end;
end;
::
:: sup F and inf F for Function of X,ExtREAL
::
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
func sup F -> R_eal equals
:Def7: sup(rng F);
correctness;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
func inf F -> R_eal equals
:Def8: inf(rng F);
correctness;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
let x be Element of X;
redefine func F.x -> R_eal;
coherence
proof
F.x in ExtREAL by TARSKI:def 3;
hence thesis;
end;
end;
scheme FunctR_ealEx{X()->non empty set,Y()->set,F(set)->set}:
ex f being Function of X(),Y() st
for x being Element of X() holds f.x = F(x)
provided
A1:for x being Element of X() holds F(x) in Y()
proof defpred P[set,set] means $2 = F($1);
A2:for x being set st x in X() ex y being set st y in Y() & P[x,y]
proof
let x be set;
assume x in X();
then reconsider x as Element of X();
take F(x);
thus thesis by A1;
end;
ex f being Function of X(),Y() st
for x being set st x in X() holds P[x,f.x] from FuncEx1(A2);
then consider f being Function of X(),Y() such that
A3:for x being set st x in X() holds f.x = F(x);
for x being Element of X() holds f.x = F (x) by A3;
hence thesis;
end;
definition
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
let F be Function of X,Y;
let G be Function of X,Z;
func F + G -> Function of X,Y + Z means
:Def9: for x being Element of X holds it.x = F.x + G.x;
existence
proof
deffunc F(Element of X) = F.$1 + G.$1;
A1:for x being Element of X holds F(x) in Y + Z
proof
let x be Element of X;
F.x in Y & G.x in Z by FUNCT_2:7;
hence thesis by Def5;
end;
ex H being Function of X,Y + Z st
for x being Element of X holds H.x = F(x) from FunctR_ealEx(A1);
then consider H being Function of X,Y + Z such that
A2:for x being Element of X holds H.x = F.x + G.x;
take H;
thus thesis by A2;
end;
uniqueness
proof
let H1,H2 be Function of X,Y + Z such that
A3:for x being Element of X holds H1.x = F.x + G.x and
A4:for x being Element of X holds H2.x = F.x + G.x;
for x being set st x in X holds H1.x = H2.x
proof
let x be set;
assume x in X;
then reconsider x as Element of X;
H1.x = F.x + G.x by A3
.= H2.x by A4;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th34:
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL holds
for F being Function of X,Y for G being Function of X,Z holds
rng(F + G) c= rng F + rng G
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
let F be Function of X,Y;
let G be Function of X,Z;
F + G is Function of X,rng F + rng G
proof
A1:dom (F + G) = X by FUNCT_2:def 1;
for x being set st x in X holds
(F + G).x in rng F + rng G
proof
let x be set;
assume x in X;
then reconsider x as Element of X;
consider a,b being R_eal such that
A2:a = F.x & b = G.x;
A3:(F + G).x = a + b by A2,Def9;
A4:a in rng F by A2,FUNCT_2:6;
b in rng G by A2,FUNCT_2:6;
hence thesis by A3,A4,Def5;
end;
hence thesis by A1,FUNCT_2:5;
end;
hence thesis by RELSET_1:12;
end;
theorem Th35:
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL st
not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
for F being Function of X,Y for G being Function of X,Z st
not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty
) holds
sup(F + G) <=' sup F + sup G
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
assume
A1:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z);
let F be Function of X,Y;
let G be Function of X,Z;
assume
A2:not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty);
A3:sup(F + G) = sup(rng(F + G)) by Def7;
rng(F + G) c= rng F + rng G by Th34;
then A4:sup(F + G) <=' sup(rng F + rng G) by A3,SUPINF_1:91;
(not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G) &
not(sup(rng F) = +infty & sup(rng G) = -infty or
sup(rng F) = -infty & sup(rng G) = +infty))
proof
not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G)
proof
assume
A5:-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G;
A6:rng F c= Y by RELSET_1:12;
rng G c= Z by RELSET_1:12;
hence contradiction by A1,A5,A6;
end;
hence thesis by A2,Def7;
end;
then A7: sup(rng F + rng G) <=' sup(rng F) + sup(rng G) by Th26;
sup F = sup(rng F) & sup G = sup(rng G) by Def7;
hence thesis by A4,A7,SUPINF_1:29;
end;
theorem Th36:
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL st
not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
for F being Function of X,Y for G being Function of X,Z st
not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty
) holds
inf F + inf G <=' inf(F + G)
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
assume
A1:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z);
let F be Function of X,Y;
let G be Function of X,Z;
assume
A2:not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty);
A3:inf(F + G) = inf(rng(F + G)) by Def8;
rng(F + G) c= rng F + rng G by Th34;
then A4:inf(rng F + rng G) <=' inf(F + G) by A3,SUPINF_1:94;
(not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G) &
not(inf(rng F) = +infty & inf(rng G) = -infty or
inf(rng F) = -infty & inf(rng G) = +infty))
proof
not(-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G)
proof
assume
A5:-infty in rng F & +infty in rng G or +infty in rng F & -infty
in rng G;
A6:rng F c= Y by RELSET_1:12;
rng G c= Z by RELSET_1:12;
hence contradiction by A1,A5,A6;
end;
hence thesis by A2,Def8;
end;
then A7: inf(rng F) + inf(rng G) <=' inf(rng F + rng G) by Th27;
inf F = inf(rng F) & inf G = inf(rng G) by Def8;
hence thesis by A4,A7,SUPINF_1:29;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
func - F -> Function of X,- Y means
:Def10: for x being Element of X holds it.x = - F.x;
existence
proof
deffunc F(Element of X) = - F.$1;
A1:for x being Element of X holds F(x) in - Y
proof
let x be Element of X;
F.x in Y by FUNCT_2:7;
hence thesis by Th23;
end;
ex H being Function of X,- Y st
for x being Element of X holds H.x = F(x) from FunctR_ealEx(A1);
then consider H being Function of X,- Y such that
A2:for x being Element of X holds H.x = - F.x;
take H;
thus thesis by A2;
end;
uniqueness
proof
let H1,H2 be Function of X,- Y such that
A3:for x being Element of X holds H1.x = - F.x and
A4:for x being Element of X holds H2.x = - F.x;
for x being set st x in X holds H1.x = H2.x
proof
let x be set;
assume x in X;
then reconsider x as Element of X;
H1.x = - F.x by A3
.= H2.x by A4;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th37:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
rng(- F) = - rng F
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
thus rng(- F) c= - rng F
proof
let y be set;
assume
A1:y in rng(- F);
A2:dom F = X by FUNCT_2:def 1;
A3:dom(- F) = X & rng(- F) c= - Y by FUNCT_2:def 1,RELSET_1:12;
reconsider y as R_eal by A1;
consider a being set such that
A4:a in X & y = (- F).a by A1,A3,FUNCT_1:def 5;
reconsider a as Element of X by A4;
a in X & y = - F.a by A4,Def10;
then - y in rng F by A2,FUNCT_1:def 5;
then - (- y) in - rng F by Th23;
hence thesis;
end;
thus - rng F c= rng(- F)
proof
let y be set;
assume
A5:y in - rng F;
A6:dom (- F) = X by FUNCT_2:def 1;
A7:dom F = X & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
reconsider y as R_eal by A5;
- y in - (- rng F) by A5,Th23;
then - y in rng F by Th22;
then consider a being set such that
A8:a in X & - y = F.a by A7,FUNCT_1:def 5;
reconsider a as Element of X by A8;
y = - F.a by A8;
then y = (- F).a by Def10;
hence thesis by A6,FUNCT_1:def 5;
end;
end;
theorem Th38:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
inf(- F) = - sup F & sup(- F) = - inf F
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
thus inf(- F) = inf(rng(- F)) by Def8
.= inf(- rng F) by Th37
.= - sup(rng F) by Th32
.= - sup F by Def7;
thus sup(- F) = sup(rng(- F)) by Def7
.= sup(- rng F) by Th37
.= - inf(rng F) by Th33
.= - inf F by Def8;
end;
::
:: Bounded Function of X,ExtREAL
::
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
attr F is bounded_above means
:Def11:sup F <'+infty;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
attr F is bounded_below means
:Def12:-infty <'inf F;
end;
definition
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
attr F is bounded means
:Def13:F is bounded_above & F is bounded_below;
end;
definition let X be non empty set;
let Y be non empty Subset of ExtREAL;
cluster bounded -> bounded_above bounded_below Function of X, Y;
coherence by Def13;
cluster bounded_above bounded_below -> bounded Function of X, Y;
coherence by Def13;
end;
theorem
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
F is bounded iff sup F <'+infty & -infty <'inf F
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
hereby assume F is bounded;
then F is bounded_above & F is bounded_below by Def13;
hence sup F <'+infty & -infty <'inf F by Def11,Def12;
end;
assume sup F <'+infty & -infty <'inf F;
then F is bounded_above & F is bounded_below by Def11,Def12;
hence thesis by Def13;
end;
theorem Th40:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
F is bounded_above iff - F is bounded_below
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
hereby assume F is bounded_above;
then sup F <'+infty by Def11;
then A1:- (+infty) <'- sup F by Th16;
- (+infty) = -infty by Def3;
then -infty <'inf(- F) by A1,Th38;
hence - F is bounded_below by Def12;
end;
assume - F is bounded_below;
then -infty <'inf(- F) by Def12;
then - inf(- F) <'- (-infty) by Th16;
then - (- sup F) <'- (-infty) by Th38;
hence thesis by Def11,Th4;
end;
theorem Th41:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
F is bounded_below iff - F is bounded_above
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
hereby assume F is bounded_below;
then -infty <'inf F by Def12;
then - inf F <'- (-infty) by Th16;
then sup(- F) <'+infty by Th4,Th38;
hence - F is bounded_above by Def11;
end;
assume - F is bounded_above;
then sup(- F) <'+infty by Def11;
then - inf F <'+infty by Th38;
then A1:- (+infty) <'- (- inf F) by Th16;
- (+infty) = -infty & - (- inf F) = inf F by Def3;
hence thesis by A1,Def12;
end;
theorem
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
F is bounded iff - F is bounded
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
hereby assume F is bounded;
then F is bounded_above & F is bounded_below by Def13;
then - F is bounded_above & - F is bounded_below by Th40,Th41;
hence - F is bounded by Def13;
end;
assume - F is bounded;
then - F is bounded_above & - F is bounded_below by Def13;
then F is bounded_above & F is bounded_below by Th40,Th41;
hence thesis by Def13;
end;
theorem
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
for x being Element of X holds
-infty <=' F.x & F.x <=' +infty by SUPINF_1:20,21;
theorem
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
for x being Element of X holds
Y c= REAL implies -infty <'F.x & F.x <'+infty
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
let x be Element of X;
assume
A1:Y c= REAL;
A2:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
then F.x in rng F by FUNCT_1:def 5;
then F.x in Y by A2;
then A3:not F.x = -infty & not F.x = +infty by A1,SUPINF_1:2,6;
-infty <=' F.x & F.x <=' +infty by SUPINF_1:20,21;
hence thesis by A3,SUPINF_1:22;
end;
theorem Th45:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
for x being Element of X holds
inf F <=' F.x & F.x <=' sup F
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
let x be Element of X;
X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
then A1:F.x in rng F by FUNCT_1:def 5;
A2: inf F = inf(rng F) by Def8;
sup F = sup(rng F) by Def7;
hence thesis by A1,A2,SUPINF_1:76,79;
end;
theorem Th46:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
Y c= REAL implies (F is bounded_above iff sup F in REAL)
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
assume
A1:Y c= REAL;
hereby assume F is bounded_above;
then A2: sup F <'+infty by Def11;
consider x being Element of X;
A3:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
then F.x in rng F by FUNCT_1:def 5;
then A4: F.x in Y by A3;
F.x <=' sup F by Th45;
then A5:not sup F = -infty by A1,A4,SUPINF_1:17;
sup F in REAL or sup F in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:
def 2;
hence sup F in REAL by A2,A5,TARSKI:def 2;
end;
assume sup F in REAL;
then sup F <'+infty by SUPINF_1:31;
hence thesis by Def11;
end;
theorem Th47:
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
Y c= REAL implies (F is bounded_below iff inf F in REAL)
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
assume
A1:Y c= REAL;
A2:F is bounded_below implies inf F in REAL
proof
assume F is bounded_below;
then A3: -infty <'inf F by Def12;
consider x being Element of X;
A4:X = dom F & rng F c= Y by FUNCT_2:def 1,RELSET_1:12;
then F.x in rng F by FUNCT_1:def 5;
then A5:F.x in Y by A4;
inf F <=' F.x by Th45;
then A6:not inf F = +infty by A1,A5,SUPINF_1:18;
inf F in REAL or inf F in {-infty,+infty} by SUPINF_1:def 6,XBOOLE_0:
def 2;
hence thesis by A3,A6,TARSKI:def 2;
end;
inf F in REAL implies F is bounded_below
proof
assume inf F in REAL;
then -infty <'inf F by SUPINF_1:31;
hence thesis by Def12;
end;
hence thesis by A2;
end;
theorem
for X being non empty set holds
for Y being non empty Subset of ExtREAL holds
for F being Function of X,Y holds
Y c= REAL implies (F is bounded iff inf F in REAL & sup F in REAL)
proof
let X be non empty set;
let Y be non empty Subset of ExtREAL;
let F be Function of X,Y;
assume
A1:Y c= REAL;
A2:F is bounded implies inf F in REAL & sup F in REAL
proof
assume F is bounded;
then F is bounded_above & F is bounded_below by Def13;
hence thesis by A1,Th46,Th47;
end;
inf F in REAL & sup F in REAL implies F is bounded
proof
assume inf F in REAL & sup F in REAL;
then F is bounded_above & F is bounded_below by A1,Th46,Th47;
hence thesis by Def13;
end;
hence thesis by A2;
end;
theorem Th49:
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
for F1 being Function of X,Y holds
for F2 being Function of X,Z holds
F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
assume
A1:Y c= REAL & Z c= REAL;
let F1 be Function of X,Y;
let F2 be Function of X,Z;
assume
A2:F1 is bounded_above & F2 is bounded_above;
A3:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z)
by A1,SUPINF_1:2;
A4:not sup F1 = +infty & not sup F2 = +infty by A2,Def11;
A5:sup F1 in REAL & sup F2 in REAL implies sup F1 + sup F2 <'+infty
proof
assume
A6:sup F1 in REAL & sup F2 in REAL;
consider a,b being R_eal such that
A7:a = sup F1 & b = sup F2;
reconsider a,b as Real by A6,A7;
sup F1 + sup F2 = a + b by A7,Th1;
hence thesis by SUPINF_1:31;
end;
A8:sup F1 in REAL & sup F2 = -infty implies sup F1 + sup F2 <'+infty
proof
assume sup F1 in REAL & sup F2 = -infty;
hence thesis by Def2,SUPINF_1:2,19;
end;
A9:sup F1 = -infty & sup F2 in REAL implies sup F1 + sup F2 <'+infty
proof
assume
sup F1 = -infty & sup F2 in REAL;
hence thesis by Def2,SUPINF_1:2,19;
end;
A10:sup F1 = -infty & sup F2 = -infty implies sup F1 + sup F2 <'+infty
by Def2,SUPINF_1:19;
sup(F1 + F2) <'+infty
proof
assume not sup(F1 + F2) <'+infty;
then not(sup(F1 + F2) <=' +infty) or sup(F1 + F2) = +infty by SUPINF_1:22
;
hence thesis by A3,A4,A5,A8,A9,A10,Th35,SUPINF_1:24,def 7;
end;
hence thesis by Def11;
end;
theorem Th50:
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
for F1 being Function of X,Y holds
for F2 being Function of X,Z holds
F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
assume
A1:Y c= REAL & Z c= REAL;
let F1 be Function of X,Y;
let F2 be Function of X,Z;
assume
A2:F1 is bounded_below & F2 is bounded_below;
A3:not(-infty in Y & +infty in Z or +infty in Y & -infty in Z)
by A1,SUPINF_1:2;
A4:not inf F1 = -infty & not inf F2 = -infty by A2,Def12;
A5:inf F1 in REAL & inf F2 in REAL implies -infty <'inf F1 + inf F2
proof
assume
A6:inf F1 in REAL & inf F2 in REAL;
consider a,b being R_eal such that
A7:a = inf F1 & b = inf F2;
reconsider a,b as Real by A6,A7;
inf F1 + inf F2 = a + b by A7,Th1;
hence thesis by SUPINF_1:31;
end;
A8:inf F1 in REAL & inf F2 = +infty implies -infty <'inf F1 + inf F2
proof
assume
inf F1 in REAL & inf F2 = +infty;
hence thesis by Def2,SUPINF_1:6,19;
end;
A9:inf F1 = +infty & inf F2 in REAL implies -infty <'inf F1 + inf F2
proof
assume
inf F1 = +infty & inf F2 in REAL;
hence thesis by Def2,SUPINF_1:6,19;
end;
A10:inf F1 = +infty & inf F2 = +infty implies -infty <'inf F1 + inf F2
by Def2,SUPINF_1:19;
-infty <'inf(F1 + F2)
proof
assume not -infty <'inf(F1 + F2);
then not(-infty <=' inf(F1 + F2)) or inf(F1 + F2) = -infty by SUPINF_1:22
;
hence thesis by A3,A4,A5,A8,A9,A10,Th36,SUPINF_1:23,def 7;
end;
hence thesis by Def12;
end;
theorem
for X being non empty set holds
for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
for F1 being Function of X,Y holds
for F2 being Function of X,Z holds
F1 is bounded & F2 is bounded implies F1 + F2 is bounded
proof
let X be non empty set;
let Y,Z be non empty Subset of ExtREAL;
assume
A1:Y c= REAL & Z c= REAL;
let F1 be Function of X,Y;
let F2 be Function of X,Z;
assume
F1 is bounded & F2 is bounded;
then F1 is bounded_above & F1 is bounded_below &
F2 is bounded_above & F2 is bounded_below by Def13;
then F1 + F2 is bounded_above & F1 + F2 is bounded_below by A1,Th49,Th50;
hence thesis by Def13;
end;
theorem Th52:
ex F being Function of NAT,ExtREAL st (F is one-to-one & NAT = rng F &
rng F is non empty Subset of ExtREAL)
proof
deffunc F(set) = $1;
A1:now let x be set;
assume x in NAT;
then x is R_eal by SUPINF_1:10;
hence F(x) in ExtREAL;
end;
ex F being Function of NAT,ExtREAL st for n being set st n in NAT holds
F.n = F(n) from Lambda1(A1);
then consider F being Function of NAT,ExtREAL such that
A2:for n being set st n in NAT holds F.n = n;
A3:rng F is non empty Subset
of ExtREAL & dom F = NAT & F is one-to-one & rng F = NAT
proof
A4:dom F = NAT & rng F c= ExtREAL by FUNCT_2:def 1,RELSET_1:12;
A5: for x1,x2 being set st x1 in NAT & x2 in NAT & F.x1 = F.x2 holds x1 = x2
proof
let x1,x2 be set;
assume
A6:x1 in NAT & x2 in NAT & F.x1 = F.x2;
then F.x1 = x1 & F.x2 = x2 by A2;
hence thesis by A6;
end;
for y being set holds y in NAT iff ex x being set st x in dom F & y = F
.
x
proof
let y be set;
y in NAT implies ex x being set st (x in dom F & y = F.x)
proof
assume
A7:y in NAT;
take y;
thus thesis by A2,A7,FUNCT_2:def 1;
end;
hence thesis by A2,A4;
end;
hence thesis by A5,FUNCT_1:def 5,FUNCT_2:25,def 1,RELSET_1:12;
end;
take F;
thus thesis by A3;
end;
::
:: Series of Elements of ExtREAL numbers
::
definition let D be non empty set; let IT be Subset of D;
redefine attr IT is countable means
:Def14: IT is empty or ex F being Function of NAT,D st IT = rng F;
compatibility
proof
thus IT is countable implies
IT is empty or ex F being Function of NAT,D st IT = rng F
proof assume that
A1: IT is countable and
A2: IT is not empty;
consider f being Function such that
A3: dom f = NAT and
A4: IT c= rng f by A1,CARD_4:45;
consider x being Element of D such that
A5: x in IT by A2,SUBSET_1:10;
set F = f|(f"IT) +* (NAT \ f"IT --> x);
A6: rng F = IT & dom F = NAT
proof
A7: f"IT c= NAT by A3,RELAT_1:167;
A8: dom(f|(f"IT)) = NAT /\ (f"IT) by A3,RELAT_1:90;
per cases;
suppose
A9: NAT = f"IT;
then A10: NAT \ f"IT = {} by XBOOLE_1:37;
then dom(NAT \ f"IT --> x) = {} by FUNCOP_1:16;
then dom(f|(f"IT)) /\ dom(NAT \ f"IT --> x) = {};
then dom(f|(f"IT)) misses dom(NAT \ f"IT --> x) by XBOOLE_0:def 7;
then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by FUNCT_4:32;
hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:26
.= rng(f|(f"IT)) \/ {} by A10,FUNCOP_1:16
.= f.:(f"IT) by RELAT_1:148
.= IT by A4,FUNCT_1:147;
thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
.= dom(f|(f"IT)) \/ {} by A10,FUNCOP_1:16
.= NAT by A8,A9;
suppose
A11: NAT <> f"IT;
A12: now assume NAT \ f"IT is empty;
then NAT c= f"IT by XBOOLE_1:37;
hence contradiction by A7,A11,XBOOLE_0:def 10;
end;
dom(NAT \ f"IT --> x) = NAT \ f"IT by FUNCOP_1:19;
then dom(f|(f"IT)) misses dom(NAT \ f"IT --> x) by A8,XBOOLE_1:89;
then F = (f|(f"IT)) \/ (NAT \ f"IT --> x) by FUNCT_4:32;
hence rng F = rng(f|(f"IT)) \/ rng(NAT \ f"IT --> x) by RELAT_1:26
.= rng(f|(f"IT)) \/ {x} by A12,FUNCOP_1:14
.= f.:(f"IT) \/ {x} by RELAT_1:148
.= IT \/ {x} by A4,FUNCT_1:147
.= IT by A5,ZFMISC_1:46;
thus dom F = dom(f|(f"IT)) \/ dom(NAT \ f"IT --> x) by FUNCT_4:def 1
.= NAT /\ (f"IT) \/ (NAT \ f"IT) by A8,FUNCOP_1:19
.= NAT by XBOOLE_1:51;
end;
then reconsider F as Function of NAT, D by FUNCT_2:def 1,RELSET_1:11;
take F;
thus IT = rng F by A6;
end;
assume
A13: IT is empty or ex F being Function of NAT,D st IT = rng F;
per cases;
suppose IT is empty;
then IT = {};
hence thesis by CARD_4:43;
suppose IT is not empty;
then consider F being Function of NAT,D such that
A14: IT = rng F by A13;
dom F = NAT by FUNCT_2:def 1;
hence IT is countable by A14,CARD_4:45;
end;
synonym IT is denumerable;
end;
definition
cluster denumerable (non empty Subset of ExtREAL);
existence
proof
consider F being Function of NAT,ExtREAL such that
F is one-to-one & NAT = rng F and
A1: rng F is non empty Subset of ExtREAL by Th52;
reconsider A = rng F as non empty Subset of ExtREAL by A1;
take A;
assume A is non empty;
thus thesis;
end;
end;
definition
mode Denum_Set_of_R_EAL is denumerable non empty Subset of ExtREAL;
end;
definition let IT be set;
attr IT is nonnegative means
:Def15:for x being R_eal holds x in IT implies 0. <=' x;
end;
definition
cluster nonnegative Denum_Set_of_R_EAL;
existence
proof
reconsider N = NAT as Denum_Set_of_R_EAL by Def14,Th52;
take N;
thus for x being R_eal holds x in N implies 0. <=' x by Th21;
end;
end;
definition
mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;
end;
definition
let D be Denum_Set_of_R_EAL;
mode Num of D -> Function of NAT,ExtREAL means
:Def16:D = rng it;
existence by Def14;
end;
definition
let N be Function of NAT,ExtREAL;
let n be Nat;
redefine func N.n -> R_eal;
coherence
proof
N.n is R_eal;
hence thesis;
end;
end;
theorem Th53:
for D being Denum_Set_of_R_EAL holds
for N being Num of D holds
ex F being Function of NAT,ExtREAL st
F.0 = N.0 &
for n being Nat,
y being R_eal st y = F.n holds
F.(n + 1) = y + N.(n+1)
proof
let D be Denum_Set_of_R_EAL;
let N be Num of D;
defpred P[set,set,set] means
for a,b being R_eal,s being Nat holds (s = $1 & a = $2 & b = $3 implies
b = a + N.(s+1));
A1:for n being Nat for x being Element of ExtREAL
ex y being Element of ExtREAL st P[n,x,y]
proof
let n be Nat;
let x be Element of ExtREAL;
consider y being R_eal such that
A2:y = x + N.(n+1);
take y;
thus thesis by A2;
end;
consider A being R_eal such that
A3:A = N.0;
consider F being Function of NAT,ExtREAL such that
A4:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)])
from RecExD(A1);
take F;
thus thesis by A3,A4;
end;
definition
let D be Denum_Set_of_R_EAL;
let N be Num of D;
func Ser(D,N) -> Function of NAT,ExtREAL means
:Def17:it.0 = N.0 &
for n being Nat holds
for y being R_eal st y = it.n holds
it.(n + 1) = y + N.(n + 1);
existence by Th53;
uniqueness
proof
let S1,S2 be Function of NAT,ExtREAL such that
A1:S1.0 = N.0 &
for n being Nat holds
for y being R_eal st y = S1.n holds
S1.(n + 1) = y + N.(n + 1) and
A2:S2.0 = N.0 &
for n being Nat holds
for y being R_eal st y = S2.n holds
S2.(n + 1) = y + N.(n + 1);
defpred P[set] means S1.$1 = S2.$1;
for n being set holds n in NAT implies P[n]
proof
let n be set;
assume
A3:n in NAT;
then reconsider n as Element of REAL;
reconsider n as Nat by A3;
for n being Nat holds S1.n = S2.n
proof
A4: P[0] by A1,A2;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6:S1.k = S2.k;
consider y1,y2 being R_eal such that
A7:y1 = S1.k & y2 = S2.k;
thus S1.(k + 1) = y2 + N.(k + 1) by A1,A6,A7
.= S2.(k + 1) by A2,A7;
end;
thus for k being Nat holds P[k] from Ind(A4,A5);
end;
then S1.n = S2.n;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th54:
for D being Pos_Denum_Set_of_R_EAL holds
for N being Num of D holds
for n being Nat holds 0. <=' N.n
proof
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
let n be Nat;
D = rng N by Def16;
then N.n in D by FUNCT_2:6;
hence thesis by Def15;
end;
theorem Th55:
for D being Pos_Denum_Set_of_R_EAL holds
for N being Num of D holds
for n being Nat holds
Ser(D,N).n <=' Ser(D,N).(n + 1) & 0. <=' Ser(D,N).n
proof
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
let n be Nat;
set F = Ser(D,N);
A1:F.0 = N.0 &
for n being Nat holds
for y being R_eal st y = F.n holds
F.(n + 1) = y + N.(n + 1) by Def17;
defpred P[Nat] means F.$1 <=' F.($1 + 1) & 0. <=' F.$1;
A2: P[0]
proof
A3:F.(0 + 1) = F.0 + N.(1) by Def17;
A4:0. <=' F.0 by A1,Th54;
0. <=' N.(1) by Th54;
hence thesis by A3,A4,Th20;
end;
A5: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A6:F.k <=' F.(k + 1) & 0. <=' F.k;
A7:F.((k+1) + 1) = F.(k + 1) + N.((k+1) + 1) by Def17;
A8:0. <=' N.((k+1) + 1) by Th54;
0. <=' F.(k+1) by A6,SUPINF_1:29;
hence thesis by A7,A8,Th20;
end;
for n being Nat holds P[n] from Ind(A2,A5);
hence thesis;
end;
theorem Th56:
for D being Pos_Denum_Set_of_R_EAL holds
for N being Num of D holds
for n,m being Nat holds
Ser(D,N).n <=' Ser(D,N).(n + m)
proof
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
let n,m be Nat;
defpred P[Nat] means Ser(D,N).n <=' Ser(D,N).(n + $1);
A1: P[0];
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3:Ser(D,N).n <=' Ser(D,N).(n + k);
Ser(D,N).(n + (k+1)) = Ser(D,N).((n + k) + 1) by XCMPLX_1:1;
then Ser(D,N).(n + k) <=' Ser(D,N).(n + (k+1)) by Th55;
hence thesis by A3,SUPINF_1:29;
end;
for n being Nat holds P[n] from Ind(A1,A2);
hence thesis;
end;
definition
let D be Denum_Set_of_R_EAL;
mode Set_of_Series of D -> non empty Subset of ExtREAL means
ex N being Num of D st it = rng Ser(D,N);
existence
proof
consider N being Num of D;
set S = Ser(D,N);
0 in NAT;
then rng S is non empty Subset of ExtREAL by FUNCT_2:6,RELSET_1:12;
then consider SER being non empty Subset of ExtREAL such that
A1:SER = rng S;
take SER;
thus thesis by A1;
end;
end;
Lm4:
for F being Function of NAT,ExtREAL holds
rng F is non empty Subset of ExtREAL
proof
let F be Function of NAT,ExtREAL;
consider n being Element of NAT;
n in NAT;
hence thesis by FUNCT_2:6,RELSET_1:12;
end;
definition
let F be Function of NAT,ExtREAL;
redefine func rng F -> non empty Subset of ExtREAL;
coherence by Lm4;
end;
definition
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
func SUM(D,N) -> R_eal equals
sup(rng Ser(D,N));
coherence;
end;
definition
let D be Pos_Denum_Set_of_R_EAL;
let N be Num of D;
pred D is_sumable N means
SUM(D,N) in REAL;
end;
theorem Th57:
for F being Function of NAT,ExtREAL holds
rng F is Denum_Set_of_R_EAL by Def14;
definition
let F be Function of NAT,ExtREAL;
redefine func rng F -> Denum_Set_of_R_EAL;
coherence by Th57;
end;
definition
let F be Function of NAT,ExtREAL;
func Ser(F) -> Function of NAT,ExtREAL means
:Def21: for N being Num of rng F st N = F holds it = Ser(rng F,N);
existence
proof
F is Num of rng F by Def16;
then consider N being Num of rng F such that
A1:N = F;
take Ser(rng F,N);
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be Function of NAT,ExtREAL such that
A2:for N being Num of rng F st N = F holds S1 = Ser(rng F,N) and
A3:for N being Num of rng F st N = F holds S2 = Ser(rng F,N);
F is Num of rng F by Def16;
then consider N being Num of rng F such that
A4:N = F;
thus S1 = Ser(rng F,N) by A2,A4
.= S2 by A3,A4;
end;
end;
definition let X be set;
let F be Function of X,ExtREAL;
attr F is nonnegative means
:Def22:rng F is nonnegative;
end;
definition
let F be Function of NAT,ExtREAL;
func SUM(F) -> R_eal equals
:Def23: sup(rng Ser(F));
coherence;
end;
theorem Th58:
for X being non empty set
for F being Function of X,ExtREAL holds
F is nonnegative iff for n being Element of X holds 0. <=' F.n
proof let X be non empty set;
let F be Function of X,ExtREAL;
hereby assume F is nonnegative;
then A1:rng F is nonnegative by Def22;
let n be Element of X;
F.n in rng F by FUNCT_2:6;
hence 0. <=' F.n by A1,Def15;
end;
assume
A2:for n being Element of X holds 0. <=' F.n;
for y being R_eal holds y in rng F implies 0. <=' y
proof
let y be R_eal;
assume y in rng F;
then consider x being set such that
A3:x in dom F & y = F.x by FUNCT_1:def 5;
reconsider x as Element of X by A3,FUNCT_2:def 1;
0. <=' F.x by A2;
hence thesis by A3;
end;
then rng F is nonnegative by Def15;
hence thesis by Def22;
end;
theorem Th59:
for F being Function of NAT,ExtREAL holds
for n being Nat holds
F is nonnegative implies (Ser(F)).n <=' (Ser(F)).(n + 1) & 0. <=' (Ser(F)).n
proof
let F be Function of NAT,ExtREAL;
let n be Nat;
assume
A1:F is nonnegative;
F is Num of rng F by Def16;
then consider N being Num of rng F such that
A2:N = F;
A3:Ser(F) = Ser(rng F,N) by A2,Def21;
rng F is Pos_Denum_Set_of_R_EAL by A1,Def22;
hence thesis by A3,Th55;
end;
theorem Th60:
for F being Function of NAT,ExtREAL holds
F is nonnegative implies
for n,m being Nat holds Ser(F).n <=' Ser(F).(n + m)
proof
let F be Function of NAT,ExtREAL;
assume
A1:F is nonnegative;
let n,m be Nat;
F is Num of rng F by Def16;
then consider N being Num of rng F such that
A2:N = F;
A3:Ser(F) = Ser(rng F,N) by A2,Def21;
rng F is Pos_Denum_Set_of_R_EAL by A1,Def22;
hence thesis by A3,Th56;
end;
theorem Th61:
for F1,F2 being Function of NAT,ExtREAL st
F1 is nonnegative holds
((for n being Nat holds F1.n <=' F2.n) implies
(for n being Nat holds Ser(F1).n <=' Ser(F2).n))
proof
let F1,F2 be Function of NAT,ExtREAL;
assume
A1:F1 is nonnegative;
assume
A2:for n being Nat holds F1.n <=' F2.n;
F1 is Num of rng F1 by Def16;
then consider N1 being Num of rng F1 such that
A3:N1 = F1;
A4:Ser(F1) = Ser(rng F1,N1) by A3,Def21;
F2 is Num of rng F2 by Def16;
then consider N2 being Num of rng F2 such that
A5:N2 = F2;
A6:Ser(F2) = Ser(rng F2,N2) by A5,Def21;
let n be Nat;
defpred P[Nat] means Ser(F1).$1 <=' Ser(F2).$1;
A7: P[0]
proof
A8:Ser(F1).0 = F1.0 by A3,A4,Def17;
Ser(F2).0 = F2.0 by A5,A6,Def17;
hence thesis by A2,A8;
end;
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A10:Ser(F1).k <=' Ser(F2).k;
A11:Ser(F1).(k+1) = Ser(F1).k + F1.(k+1) by A3,A4,Def17;
A12:Ser(F2).(k+1) = Ser(F2).k + F2.(k+1) by A5,A6,Def17;
A13:F1.(k+1) <=' F2.(k+1) by A2;
A14:0. <=' Ser(F1).k by A1,Th59;
0. <=' F1.(k+1) by A1,Th58;
hence thesis by A10,A11,A12,A13,A14,Lm3;
end;
for n being Nat holds P[n] from Ind(A7,A9);
hence thesis;
end;
theorem Th62:
for F1,F2 being Function of NAT,ExtREAL st
F1 is nonnegative holds
((for n being Nat holds F1.n <=' F2.n) implies (SUM(F1) <=' SUM(F2)))
proof
let F1,F2 be Function of NAT,ExtREAL;
assume
A1:F1 is nonnegative;
assume
A2:for n being Nat holds F1.n <=' F2.n;
A3:SUM(F1) = sup(rng Ser(F1)) by Def23;
A4:SUM(F2) = sup(rng Ser(F2)) by Def23;
for x being R_eal st x in rng Ser(F1) holds
(ex y being R_eal st y in rng Ser(F2) & x <=' y)
proof
let x be R_eal;
assume
A5:x in rng Ser(F1);
A6:dom Ser(F1) = NAT & dom Ser(F2) = NAT & rng Ser(F2) c= ExtREAL
by FUNCT_2:def 1;
then consider n being set such that
A7:n in NAT & x = Ser(F1).n by A5,FUNCT_1:def 5;
reconsider n as Nat by A7;
consider y being set such that
A8:y = Ser(F2).n;
reconsider y as R_eal by A8;
take y;
thus thesis by A1,A2,A6,A7,A8,Th61,FUNCT_1:def 5;
end;
hence thesis by A3,A4,SUPINF_1:99;
end;
theorem Th63:
for F being Function of NAT,ExtREAL holds
Ser(F).0 = F.0 &
for n being Nat holds
for y being R_eal st y = Ser(F).n holds
Ser(F).(n + 1) = y + F.(n + 1)
proof
let F be Function of NAT,ExtREAL;
F is Num of rng F by Def16;
then consider N being Num of rng F such that
A1:N = F;
Ser(F) = Ser(rng F,N) by A1,Def21;
hence thesis by A1,Def17;
end;
theorem Th64:
for F being Function of NAT,ExtREAL st F is nonnegative holds
(ex n being Nat st F.n = +infty) implies SUM(F) = +infty
proof
let F be Function of NAT,ExtREAL;
assume
A1:F is nonnegative;
given n being Nat such that
A2:F.n = +infty;
A3:n = 0 implies SUM(F) = +infty
proof
assume n = 0;
then A4:Ser(F).0 = +infty by A2,Th63;
consider x being R_eal such that
A5:x = Ser(F).0;
A6:x in rng Ser(F) by A5,FUNCT_2:6;
x is majorant of rng Ser(F) by A4,A5,SUPINF_1:33;
then sup(rng Ser(F)) = +infty by A4,A5,A6,SUPINF_1:80;
hence thesis by Def23;
end;
(ex k being Nat st n = k + 1) implies SUM(F) = +infty
proof
given k being Nat such that
A7:n = k + 1;
A8:not Ser(F).k = -infty
proof
A9:0. <=' Ser(F).k by A1,Th59;
not 0. = -infty by Def1,SUPINF_1:6;
hence thesis by A9,SUPINF_1:23;
end;
consider y being R_eal such that
A10:y = Ser(F).k;
A11: Ser(F).(k + 1) = y + F.(k + 1) by A10,Th63;
consider x being R_eal such that
A12:x = Ser(F).(k + 1);
A13:x = +infty by A2,A7,A8,A10,A11,A12,Def2;
A14:x in rng Ser(F) by A12,FUNCT_2:6;
x is majorant of rng Ser(F) by A13,SUPINF_1:33;
then sup(rng Ser(F)) = +infty by A13,A14,SUPINF_1:80;
hence thesis by Def23;
end;
hence thesis by A3,NAT_1:22;
end;
definition
let F be Function of NAT,ExtREAL;
attr F is summable means
:Def24:SUM(F) in REAL;
end;
theorem
for F being Function of NAT,ExtREAL st F is nonnegative holds
((ex n being Nat st F.n = +infty) implies F is not summable)
proof
let F be Function of NAT,ExtREAL;
assume
A1:F is nonnegative;
assume ex n being Nat st F.n = +infty;
then not SUM(F) in REAL by A1,Th64,SUPINF_1:2;
hence thesis by Def24;
end;
theorem
for F1,F2 being Function of NAT,ExtREAL st
F1 is nonnegative holds
((for n being Nat holds F1.n <=' F2.n) implies
(F2 is summable implies F1 is summable))
proof
let F1,F2 be Function of NAT,ExtREAL;
assume
A1:F1 is nonnegative;
assume
A2:for n being Nat holds F1.n <=' F2.n;
assume F2 is summable;
then A3:SUM(F2) in REAL by Def24;
SUM(F1) <=' SUM(F2) by A1,A2,Th62;
then A4:not SUM(F1) = +infty by A3,SUPINF_1:18;
A5:SUM(F1) = sup(rng Ser(F1)) by Def23;
A6:0. <=' Ser(F1).0 by A1,Th59;
Ser(F1).0 in rng Ser(F1) by FUNCT_2:6;
then Ser(F1).0 <=' sup(rng Ser(F1)) by SUPINF_1:76;
then A7:0. <=' SUM(F1) by A5,A6,SUPINF_1:29;
A8:not SUM(F1) = -infty
proof
not 0. = -infty by Def1,SUPINF_1:6;
hence thesis by A7,SUPINF_1:23;
end;
SUM(F1) in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
then SUM(F1) in REAL or SUM(F1) in {-infty,+infty} by XBOOLE_0:def 2;
hence thesis by A4,A8,Def24,TARSKI:def 2;
end;
theorem Th67:
for F being Function of NAT,ExtREAL st F is nonnegative holds
for n being Nat st (for r being Nat holds (n <= r implies F.r = 0.))
holds SUM(F) = Ser(F).n
proof
let F be Function of NAT,ExtREAL;
assume
A1:F is nonnegative;
let n be Nat;
assume
A2:for r being Nat holds (n <= r implies F.r = 0.);
A3:for r being Nat holds (n <= r implies Ser(F).r <=' Ser(F).n)
proof
let r be Nat;
assume n <= r;
then A4: ex m being Nat st r = n + m by NAT_1:28;
defpred P[Nat] means Ser(F).(n + $1) <=' Ser(F).n;
for m being Nat holds P[m]
proof
A5: P[0];
A6: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat;
assume
A7:Ser(F).(n + s) <=' Ser(F).n;
A8:n + (s + 1) = (n + s) + 1 by XCMPLX_1:1;
consider y being R_eal such that
A9:y = Ser(F).(n + s);
A10:Ser(F).(n + (s + 1)) = y + F.(n + (s + 1)) by A8,A9,Th63;
0 <= s+1 by NAT_1:18;
then n + 0 <= n + (s+1) by REAL_1:55;
then F.(n + (s+1)) = 0. by A2;
hence thesis by A7,A9,A10,Th18;
end;
thus for m being Nat holds P[m] from Ind(A5,A6);
end;
hence thesis by A4;
end;
A11:for r being Nat holds (r <= n implies Ser(F).r <=' Ser(F).n)
proof
let r be Nat;
assume r <= n;
then ex m being Nat st n = r + m by NAT_1:28;
hence thesis by A1,Th60;
end;
for y being R_eal holds y in rng Ser(F) implies y <=' Ser(F).n
proof
let y be R_eal;
assume
A12:y in rng Ser(F);
dom Ser(F) = NAT & rng Ser(F) c= ExtREAL by FUNCT_2:def 1;
then consider m being set such that
A13:m in NAT & y = Ser(F).m by A12,FUNCT_1:def 5;
reconsider m as Nat by A13;
m <= n or n <= m;
hence thesis by A3,A11,A13;
end;
then A14:Ser(F).n is majorant of rng Ser(F) by SUPINF_1:def 9;
Ser(F).n in rng Ser(F) by FUNCT_2:6;
then sup(rng Ser(F)) = Ser(F).n by A14,SUPINF_1:80;
hence thesis by Def23;
end;
theorem Th68:
for F being Function of NAT,ExtREAL st
(for n being Nat holds F.n in REAL ) holds
(for n being Nat holds Ser(F).n in REAL)
proof
let F be Function of NAT,ExtREAL;
assume
A1:for n being Nat holds F.n in REAL;
defpred P[Element of NAT] means Ser(F).$1 in REAL;
Ser(F).0 = F.0 by Th63;
then A2: P[0] by A1;
A3: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat;
assume
A4:Ser(F).s in REAL;
consider y being R_eal such that
A5:y = Ser(F).s;
A6:Ser(F).(s+1) = y + F.(s+1) by A5,Th63;
consider b being set such that
A7:b = F.(s+1);
reconsider b as Real by A1,A7;
consider a being set such that
A8:a = y;
reconsider a as Real by A4,A5,A8;
y + F.(s+1) = a + b by A7,A8,Th1;
hence thesis by A6;
end;
thus for s being Nat holds P[s] from Ind(A2,A3);
end;
theorem
for F being Function of NAT,ExtREAL st F is nonnegative holds
(ex n being Nat st (for k being Nat holds (n <= k implies F.k = 0.)) &
(for k being Nat holds (k <= n implies not F.k = +infty)))
implies F is summable
proof
let F be Function of NAT,ExtREAL;
assume
A1:F is nonnegative;
given n being Nat such that
A2:for k being Nat holds (n <= k implies F.k = 0.) and
A3:for k being Nat holds (k <= n implies not F.k = +infty);
A4:SUM(F) = Ser(F).n by A1,A2,Th67;
for s being Nat holds F.s in REAL
proof
let s be Nat;
A5:s <= n implies F.s in REAL
proof
assume s <= n;
then A6:not F.s = +infty by A3;
A7:0. <=' F.s by A1,Th58;
A8:not F.s = -infty
proof
not 0. = -infty by Def1,SUPINF_1:6;
hence thesis by A7,SUPINF_1:23;
end;
F.s in REAL \/ {-infty,+infty} by SUPINF_1:def 5;
then F.s in REAL or F.s in {-infty,+infty} by XBOOLE_0:def 2;
hence thesis by A6,A8,TARSKI:def 2;
end;
n <= s implies F.s in REAL
proof
assume n <= s;
then F.s = 0. by A2;
hence thesis by Def1;
end;
hence thesis by A5;
end;
then Ser(F).n in REAL by Th68;
hence thesis by A4,Def24;
end;