### The Mizar article:

### Series of Positive Real Numbers. Measure Theory

**by****Jozef Bialas**

- Received September 27, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: SUPINF_2
- [ MML identifier index ]

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;

Back to top