:: Some Properties of Dyadic Numbers and Intervals
:: by J\'ozef Bia{\l}as and Yatsuka Nakamura
::
:: Received February 16, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, CARD_1, RELAT_1, MEMBER_1, TARSKI,
ARYTM_3, XBOOLE_0, SUPINF_1, XXREAL_0, MEASURE5, XXREAL_1, ORDINAL2,
XXREAL_2, MEMBERED, SEQ_4, ARYTM_1, NEWTON, INT_1, URYSOHN1, CARD_3,
PROB_1, LIMFUNC1, NAT_1, COMPLEX1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0,
XXREAL_3, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NUMBERS, MEMBERED, MEMBER_1, NEWTON, INT_1, NAT_1,
XXREAL_1, XXREAL_2, SUPINF_1, MEASURE5, PROB_1, URYSOHN1, INTEGRA2,
LIMFUNC1, SEQ_4, SUPINF_2, EXTREAL1;
constructors DOMAIN_1, REAL_1, NAT_1, PROB_1, LIMFUNC1, NEWTON, SUPINF_2,
URYSOHN1, INTEGRA2, SUPINF_1, EXTREAL1, SEQ_4, PSCOMP_1, MEASURE5,
BINOP_2;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, XXREAL_1, SEQ_4, XXREAL_2, XXREAL_3, MEASURE5, MEMBER_1,
NEWTON, ORDINAL1;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_2;
equalities PROB_1, LIMFUNC1, XCMPLX_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, SEQ_4, ABSVALUE, URYSOHN1, XREAL_0, MEASURE5,
MEASURE6, INT_1, INTEGRA2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1,
XREAL_1, XXREAL_0, NEWTON, XXREAL_1, MEMBERED, XXREAL_2, EXTREAL1,
XXREAL_3, MEMBER_1;
schemes NAT_1;
begin :: Properties of the Intervals
theorem Th1:
for A being Subset of REAL, x being Real st x <> 0 holds
x" ** (x ** A) = A
proof
let A be Subset of REAL;
let x be Real;
assume
A1: x <> 0;
thus x" ** (x ** A) c= A
proof
let y be object;
assume
A2: y in x" ** (x ** A);
consider z being Real such that
A3: z in x ** A and
A4: y = x" * z by A2,INTEGRA2:39;
consider t being Real such that
A5: t in A and
A6: z = x * t by A3,INTEGRA2:39;
y = (x" * x) * t by A4,A6
.= 1 * t by A1,XCMPLX_0:def 7
.= t;
hence thesis by A5;
end;
let y be object;
assume
A7: y in A;
then reconsider y as Real;
set t = y / x";
A8: t in x ** A by A7,MEMBER_1:193;
y = x" * t by A1,XCMPLX_1:87,202;
hence thesis by A8,MEMBER_1:193;
end;
theorem Th2:
for x being Real st x <> 0 holds for A being Subset of REAL holds
A = REAL implies x ** A = A
proof
let x be Real;
assume
A1: x <> 0;
let A be Subset of REAL;
assume
A2: A = REAL;
for y being object st y in A holds y in x ** A
proof
let y be object;
assume y in A;
then reconsider y as Real;
reconsider z = y/x as Element of REAL by XREAL_0:def 1;
y = x * z by A1,XCMPLX_1:87;
hence thesis by A2,MEMBER_1:193;
end;
then A c= x ** A;
hence thesis by A2;
end;
theorem Th3:
for A being Subset of REAL st A <> {} holds 0 ** A = {0}
proof
let A be Subset of REAL;
assume
A1: A <> {};
A2: {0} c= 0 ** A
proof
let y be object;
consider t being object such that
A3: t in A by A1,XBOOLE_0:def 1;
reconsider t as Element of A by A3;
reconsider t as Real;
assume y in {0};
then y = 0 * t by TARSKI:def 1;
hence thesis by A3,MEMBER_1:193;
end;
0 ** A c= {0}
proof
let y be object;
assume
A4: y in 0 ** A;
then reconsider y as Real;
ex z being Real st z in A & y = 0 * z by A4,INTEGRA2:39;
hence thesis by TARSKI:def 1;
end;
hence thesis by A2;
end;
theorem
for x being Real holds x ** {} = {};
theorem Th5:
for a,b being R_eal st a <= b holds a = -infty & b = -infty or a
= -infty & b in REAL or a = -infty & b = +infty or a in REAL & b in REAL or a
in REAL & b = +infty or a = +infty & b = +infty
proof
let a,b be R_eal;
a in REAL or a in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4;
then
A1: a in REAL or a = -infty or a = +infty by TARSKI:def 2;
b in REAL or b in {-infty,+infty} by XBOOLE_0:def 3,XXREAL_0:def 4;
then
A2: b in REAL or b = -infty or b = +infty by TARSKI:def 2;
assume a <= b;
hence thesis by A1,A2,XXREAL_0:9,12;
end;
theorem Th6:
for A being Interval holds 0 ** A is interval
proof
let A be Interval;
per cases;
suppose
A = {};
hence thesis;
end;
suppose
A <> {};
then 0 ** A = {0} by Th3;
then 0 ** A = [.0,0 .] by XXREAL_1:17;
hence thesis;
end;
end;
theorem Th7:
for A being non empty Interval, x being Real st x<>0 holds A is
open_interval implies x ** A is open_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: x <> 0;
assume
A2: A is open_interval;
then consider a,b being R_eal such that
A3: A = ].a,b.[ by MEASURE5:def 2;
A4: a < b by A3,XXREAL_1:28;
now
per cases;
case
A5: x < 0;
now
per cases by A4,Th5;
case
a = -infty & b = -infty;
then ].a,b.[ = {};
then x ** A = {} by A3;
hence thesis;
end;
case
A6: a = -infty & b in REAL;
then reconsider s = b as Real;
set c = +infty;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A7: d = x * s;
A8: ].d,c.[ c= x ** A
proof
let q be object;
assume
A9: q in ].d,c.[;
then reconsider q as Real;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A10: d < q1 by A9,MEASURE5:def 1;
A11: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1,XCMPLX_1:87;
then
A12: q3 < b by A5,A7,A10,XREAL_1:65;
a < q3 by A6,XXREAL_0:12;
hence thesis by A3,A12,MEASURE5:def 1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A11,MEMBER_1:193;
end;
x ** A c= ].d,c.[
proof
let q be object;
assume
A13: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A16: q < +infty by XXREAL_0:9;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 < b by A3,A14,MEASURE5:def 1;
then consider r,o being Real such that
A17: r = z2 & o = b and
r <= o by A6;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
r < o by A3,A14,A17,MEASURE5:def 1;
then o1 < r1 by A5,XREAL_1:69;
hence thesis by A7,A15,A17,A16,MEASURE5:def 1;
end;
then x ** A = ].d,c.[ by A8;
hence thesis by MEASURE5:def 2;
end;
case
a = -infty & b = +infty;
hence thesis by A2,A3,A5,Th2,XXREAL_1:224;
end;
case
A18: a in REAL & b in REAL;
then reconsider s = a, r = b as Real;
reconsider d = x * s, g = x * r as R_eal by XXREAL_0:def 1;
A19: ].g,d.[ c= x ** A
proof
let q be object;
assume
A20: q in ].g,d.[;
then reconsider q as Real;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A21: q1 < d by A20,MEASURE5:def 1;
A22: g < q1 by A20,MEASURE5:def 1;
A23: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1,XCMPLX_1:87;
then
A24: a < q3 by A5,A21,XREAL_1:65;
q/x < (x * r)/x by A5,A22,XREAL_1:75;
then q3 < b by A5,XCMPLX_1:89;
hence thesis by A3,A24,MEASURE5:def 1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A23,MEMBER_1:193;
end;
x ** A c= ].g,d.[
proof
let q be object;
assume
A25: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A26: z2 in A and
A27: q = x * z2 by A25,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
a < z2 by A3,A26,MEASURE5:def 1;
then consider 1o,1ra being Real such that
A28: 1o= a & 1ra = z2 and
1o <= 1ra by A18;
z2 < b by A3,A26,MEASURE5:def 1;
then consider 2o,2r being Real such that
A29: 2o= z2 & 2r = b and
2o <= 2r by A18;
reconsider 1o1 = x * 1o, 1r1 = x * 1ra, 2o1 = x * 2o, 2r1 = x * 2r
as R_eal by XXREAL_0:def 1;
2o< 2r by A3,A26,A29,MEASURE5:def 1;
then
A30: 2r1 < 2o1 by A5,XREAL_1:69;
1o < 1ra by A3,A26,A28,MEASURE5:def 1;
then 1r1 < 1o1 by A5,XREAL_1:69;
hence thesis by A27,A28,A29,A30,MEASURE5:def 1;
end;
then x ** A = ].g,d.[ by A19;
hence thesis by MEASURE5:def 2;
end;
case
A31: a in REAL & b = +infty;
then reconsider s = a as Real;
set c = -infty;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
A32: ].c,d.[ c= x ** A
proof
let q be object;
assume
A33: q in ].c,d.[;
then reconsider q as Real;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A34: q = x * (q / x) by A1,XCMPLX_1:87;
q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
q1 <= d by A33,MEASURE5:def 1;
then x * q2 < x * s by A33,A34,MEASURE5:def 1;
then
A35: a < q3 by A5,XREAL_1:65;
q3 < b by A31,XXREAL_0:9;
hence thesis by A3,A35,MEASURE5:def 1;
end;
hence thesis by A34,MEMBER_1:193;
end;
x ** A c= ].c,d.[
proof
let q be object;
assume
A36: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A37: z2 in A and
A38: q = x * z2 by A36,INTEGRA2:39;
reconsider z2,q as R_eal by XXREAL_0:def 1;
a < z2 by A3,A37,MEASURE5:def 1;
then consider o,r being Real such that
A39: o = a & r = z2 and
o <= r by A31;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A40: -infty < q by XXREAL_0:12;
o < r by A3,A37,A39,MEASURE5:def 1;
then r1 < o1 by A5,XREAL_1:69;
hence thesis by A38,A39,A40,MEASURE5:def 1;
end;
then x ** A = ].c,d.[ by A32;
hence thesis by MEASURE5:def 2;
end;
case
a = +infty & b = +infty;
then ].a,b.[ = {};
then x ** A = {} by A3;
hence thesis;
end;
end;
hence thesis;
end;
case
x = 0;
hence thesis by A1;
end;
case
A41: 0 < x;
now
per cases by A4,Th5;
case
a = -infty & b = -infty;
then ].a,b.[ = {};
then x ** A = {} by A3;
hence thesis;
end;
case
A42: a = -infty & b in REAL;
then reconsider s = b as Real;
set c = -infty;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
A43: ].c,d.[ c= x ** A
proof
let q be object;
assume
A44: q in ].c,d.[;
then reconsider q as Real;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A45: q1 < d by A44,MEASURE5:def 1;
A46: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1,XCMPLX_1:87;
then
A47: q3 < b by A41,A45,XREAL_1:64;
a < q3 by A42,XXREAL_0:12;
hence thesis by A3,A47,MEASURE5:def 1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A46,MEMBER_1:193;
end;
x ** A c= ].c,d.[
proof
let q be object;
assume
A48: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A49: z2 in A and
A50: q = x * z2 by A48,INTEGRA2:39;
reconsider z2,q as R_eal by XXREAL_0:def 1;
z2 < b by A3,A49,MEASURE5:def 1;
then consider r,o being Real such that
A51: r = z2 & o = b and
r <= o by A42;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A52: -infty < q by XXREAL_0:12;
r < o by A3,A49,A51,MEASURE5:def 1;
then r1 < o1 by A41,XREAL_1:68;
hence thesis by A50,A51,A52,MEASURE5:def 1;
end;
then x ** A = ].c,d.[ by A43;
hence thesis by MEASURE5:def 2;
end;
case
a = -infty & b = +infty;
hence thesis by A2,A3,A41,Th2,XXREAL_1:224;
end;
case
A53: a in REAL & b in REAL;
then reconsider s = a, r = b as Real;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
A54: ].d,g.[ c= x ** A
proof
let q be object;
assume
A55: q in ].d,g.[;
then reconsider q as Real;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A56: q1 = q;
A57: q1 < g by A55,A56,MEASURE5:def 1;
A58: d < q1 by A55,A56,MEASURE5:def 1;
A59: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1,XCMPLX_1:87;
then
A60: a < q3 by A41,A56,A58,XREAL_1:64;
q/x < (x * r)/x by A41,A56,A57,XREAL_1:74;
then q3 < b by A41,XCMPLX_1:89;
hence thesis by A3,A60,MEASURE5:def 1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A59,MEMBER_1:193;
end;
x ** A c= ].d,g.[
proof
let q be object;
assume
A61: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A62: z2 in A and
A63: q = x * z2 by A61,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 < b by A3,A62,MEASURE5:def 1;
then consider 2o,2r being Real such that
A64: 2o= z2 & 2r = b and
2o <= 2r by A53;
reconsider 2o1 = x * 2o, 2r1 = x * 2r as R_eal by XXREAL_0:def 1;
2o< 2r by A3,A62,A64,MEASURE5:def 1;
then
A65: 2o1 < 2r1 by A41,XREAL_1:68;
a < z2 by A3,A62,MEASURE5:def 1;
then consider 1o,1ra being Real such that
A66: 1o= a & 1ra = z2 and
1o <= 1ra by A53;
reconsider 1o1 = x * 1o, 1r1 = x * 1ra as R_eal by XXREAL_0:def 1;
1o< 1ra by A3,A62,A66,MEASURE5:def 1;
then 1o1 < 1r1 by A41,XREAL_1:68;
hence thesis by A63,A66,A64,A65,MEASURE5:def 1;
end;
then x ** A = ].d,g.[ by A54;
hence thesis by MEASURE5:def 2;
end;
case
A67: a in REAL & b = +infty;
then reconsider s = a as Element of REAL;
set c = +infty;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
A68: x ** A c= ].d,c.[
proof
let q be object;
assume
A69: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A70: z2 in A and
A71: q = x * z2 by A69,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A72: q < +infty by XXREAL_0:9;
reconsider z2 as R_eal by XXREAL_0:def 1;
a < z2 by A3,A70,MEASURE5:def 1;
then consider o,r being Real such that
A73: o = a & r = z2 and
o <= r by A67;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
o < r by A3,A70,A73,MEASURE5:def 1;
then o1 < r1 by A41,XREAL_1:68;
hence thesis by A71,A73,A72,MEASURE5:def 1;
end;
].d,c.[ c= x ** A
proof
let q be object;
assume
A74: q in ].d,c.[;
then reconsider q as Real;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A75: q = x * (q / x) by A1,XCMPLX_1:87;
A76: d < q1 by A74,MEASURE5:def 1;
q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
a < q3 & q3 < b by A41,A67,A76,A75,XREAL_1:64,XXREAL_0:9;
hence thesis by A3,MEASURE5:def 1;
end;
hence thesis by A75,MEMBER_1:193;
end;
then x ** A = ].d,c.[ by A68;
hence thesis by MEASURE5:def 2;
end;
case
a = +infty & b = +infty;
then ].a,b.[ = {};
then x ** A = {} by A3;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th8:
for A being non empty Interval, x being Real st x<>0 holds A is
closed_interval implies x ** A is closed_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: x <> 0;
assume A is closed_interval;
then consider a,b being Real such that
A2: A = [.a,b.] by MEASURE5:def 3;
reconsider a,b as R_eal by XXREAL_0:def 1;
now
per cases;
case
A3: x < 0;
now
reconsider s = a, r = b as Real;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
A4: [.g,d.] c= x ** A
proof
let q be object;
assume
A5: q in [.g,d.];
then reconsider q as Real;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A6: g <= q1 by A5,XXREAL_1:1;
A7: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A8: q3 <= b
proof
consider p,o being Real such that
A9: p = g & o = q1 and
A10: p <= o by A6;
o/x <= p/x by A3,A10,XREAL_1:73;
hence thesis by A3,A9,XCMPLX_1:89;
end;
a <= q3
proof
q1 <= d & x * q2 = q by A1,A5,XCMPLX_1:87,XXREAL_1:1;
hence thesis by A3,XREAL_1:69;
end;
hence thesis by A2,A8,XXREAL_1:1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A7,MEMBER_1:193;
end;
x ** A c= [.g,d.]
proof
let q be object;
assume
A11: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A12: z2 in A and
A13: q = x * z2 by A11,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A12,XXREAL_1:1;
then consider 1o,1ra being Real such that
A14: 1o= a & 1ra = z2 and
A15: 1o <= 1ra;
z2 <= b by A2,A12,XXREAL_1:1;
then consider 2o,2r being Real such that
A16: 2o= z2 & 2r = b and
A17: 2o <= 2r;
A18: x * 2r <= x * 2o by A3,A17,XREAL_1:65;
x * 1o is R_eal & x * 1ra is R_eal by XXREAL_0:def 1;
then consider 1o1,1r1 being R_eal such that
A19: 1o1 = x * 1o & 1r1 = x * 1ra;
1r1 <= 1o1 by A3,A15,A19,XREAL_1:65;
hence thesis by A13,A14,A16,A18,A19,XXREAL_1:1;
end;
then x ** A = [.g,d.] by A4;
hence thesis by MEASURE5:def 3;
end;
hence thesis;
end;
case
x = 0;
hence thesis by A1;
end;
case
A20: 0 < x;
now
per cases by Th5;
case
a in REAL & b in REAL;
reconsider r = b as Real;
reconsider s = a as Real;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A21: d = x * s;
A22: [.d,g.] c= x ** A
proof
let q be object;
assume
A23: q in [.d,g.];
then reconsider q as Real by A21;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A24: q1 = q;
A25: q = x * (q / x) by A1,XCMPLX_1:87;
q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A27: q3 <= b
proof
q1 <= g by A23,A24,XXREAL_1:1;
then consider p,o being Real such that
A28: p = q1 & o = g and
A29: p <= o by A24;
p/x <= o/x by A20,A29,XREAL_1:72;
hence thesis by A20,A24,A28,XCMPLX_1:89;
end;
a <= q3
proof
d <= q1 by A23,A24,XXREAL_1:1;
hence thesis by A20,A21,A24,A25,XREAL_1:68;
end;
hence thesis by A2,A27,XXREAL_1:1;
end;
hence thesis by A25,MEMBER_1:193;
end;
x ** A c= [.d,g.]
proof
let q be object;
assume
A30: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A31: z2 in A and
A32: q = x * z2 by A30,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A31,XXREAL_1:1;
then consider 1o,1ra being Real such that
A33: 1o= a & 1ra = z2 and
A34: 1o <= 1ra;
z2 <= b by A2,A31,XXREAL_1:1;
then consider 2o,2r being Real such that
A35: 2o= z2 & 2r = b and
A36: 2o <= 2r;
A37: x * 2o <= x * 2r by A20,A36,XREAL_1:64;
x * 1o is R_eal & x * 1ra is R_eal by XXREAL_0:def 1;
then consider 1o1,1r1 being R_eal such that
A38: 1o1 = x * 1o & 1r1 = x * 1ra;
1o1 <= 1r1 by A20,A34,A38,XREAL_1:64;
hence thesis by A21,A32,A33,A35,A37,A38,XXREAL_1:1;
end;
then x ** A = [.d,g.] by A22;
hence thesis by A21,MEASURE5:def 3;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th9:
for A being non empty Interval, x being Real st 0 < x holds A is
right_open_interval implies x ** A is right_open_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
assume A is right_open_interval;
then consider a being Real,b being R_eal such that
A2: A = [.a,b.[ by MEASURE5:def 4;
A3: a < b by A2,XXREAL_1:27;
reconsider a as R_eal by XXREAL_0:def 1;
now
per cases by A3,Th5;
case
a = -infty & b = -infty;
hence thesis;
end;
case
a = -infty & b in REAL;
hence thesis;
end;
case
a = -infty & b = +infty;
hence thesis;
end;
case
A4: a in REAL & b in REAL;
then consider r being Real such that
A5: r = b;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A6: g = x * r;
consider s being Real such that
A7: s = a;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s;
A9: [.d,g.[ c= x ** A
proof
let q be object;
assume
A10: q in [.d,g.[;
then reconsider q as Real by A8;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A12: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A14: q3 < b
proof
q1 <= g by A10,XXREAL_1:3;
then consider p,o being Real such that
A15: p = q1 & o = g and
p <= o by A6;
p < o by A10,A15,XXREAL_1:3;
then p/x < o/x by A1,XREAL_1:74;
hence thesis by A1,A5,A6,A15,XCMPLX_1:89;
end;
a <= q3
proof
d <= q1 & x * q2 = q by A1,A10,XCMPLX_1:87,XXREAL_1:3;
hence thesis by A1,A7,A8,XREAL_1:68;
end;
hence thesis by A2,A14,XXREAL_1:3;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A12,MEMBER_1:193;
end;
x ** A c= [.d,g.[
proof
let q be object;
assume
A16: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A17: z2 in A and
A18: q = x * z2 by A16,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A2,A17,XXREAL_1:3;
then consider 2o,2r being Real such that
A19: 2o= z2 & 2r = b and
2o <= 2r by A4;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A20: 2o1 = x * 2o & 2r1 = x * 2r;
2o< 2r by A2,A17,A19,XXREAL_1:3;
then
A21: 2o1 < 2r1 by A1,A20,XREAL_1:68;
a <= z2 by A2,A17,XXREAL_1:3;
then consider 1o,1ra being Real such that
A22: 1o= a & 1ra = z2 and
A23: 1o <= 1ra;
x * 1o <= x * 1ra by A1,A23,XREAL_1:64;
hence thesis by A7,A5,A8,A6,A18,A22,A19,A20,A21,XXREAL_1:3;
end;
then x ** A = [.d,g.[ by A9;
hence thesis by A8,MEASURE5:def 4;
end;
case
A24: a in REAL & b = +infty;
consider s being Real such that
A25: s = a;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A26: d = x * s;
consider c being R_eal such that
A27: c = +infty;
A28: [.d,c.[ c= x ** A
proof
let q be object;
assume
A29: q in [.d,c.[;
then reconsider q as Real by A26;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A30: q1 = q;
A31: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A33: a <= q3
proof
d <= q1 & x * q2 = q by A1,A29,A30,XCMPLX_1:87,XXREAL_1:3;
hence thesis by A1,A25,A26,A30,XREAL_1:68;
end;
q3 < b by A24,XXREAL_0:9;
hence thesis by A2,A33,XXREAL_1:3;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A31,MEMBER_1:193;
end;
x ** A c= [.d,c.[
proof
let q be object;
assume
A34: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A35: z2 in A and
A36: q = x * z2 by A34,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A37: q < +infty by XXREAL_0:9;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A35,XXREAL_1:3;
then consider o,r being Real such that
A38: o = a & r = z2 and
A39: o <= r;
x * o <= x * r by A1,A39,XREAL_1:64;
hence thesis by A25,A27,A26,A36,A38,A37,XXREAL_1:3;
end;
then x ** A = [.d,c.[ by A28;
hence thesis by A26,MEASURE5:def 4;
end;
case
a = +infty & b = +infty;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th10:
for A being non empty Interval, x being Real st x < 0 holds A is
right_open_interval implies x ** A is left_open_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: x < 0;
assume A is right_open_interval;
then consider a being Real,b being R_eal such that
A2: A = [.a,b.[ by MEASURE5:def 4;
A3: a < b by A2,XXREAL_1:27;
reconsider a as R_eal by XXREAL_0:def 1;
now
per cases by A3,Th5;
case
a = -infty & b = -infty;
hence thesis;
end;
case
a = -infty & b in REAL;
hence thesis;
end;
case
a = -infty & b = +infty;
hence thesis;
end;
case
A4: a in REAL & b in REAL;
then consider r being Real such that
A5: r = b;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A6: g = x * r;
consider s being Real such that
A7: s = a;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s;
A9: ].g,d.] c= x ** A
proof
let q be object;
assume
A10: q in ].g,d.];
then reconsider q as Real by A8;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A11: q1 = q;
A12: g < q1 by A10,A11,XXREAL_1:2;
A13: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A15: q3 < b
proof
consider p,o being Real such that
A16: p = g & o = q1 and
p <= o by A6,A11,A12;
g < q1 by A10,A11,XXREAL_1:2;
then o/x < p/x by A1,A16,XREAL_1:75;
hence thesis by A1,A5,A6,A11,A16,XCMPLX_1:89;
end;
a <= q3
proof
q1 <= d & x * q2 = q by A1,A10,A11,XCMPLX_1:87,XXREAL_1:2;
hence thesis by A1,A7,A8,A11,XREAL_1:69;
end;
hence thesis by A2,A15,XXREAL_1:3;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A13,MEMBER_1:193;
end;
x ** A c= ].g,d.]
proof
let q be object;
assume
A17: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A2,A18,XXREAL_1:3;
then consider 2o,2r being Real such that
A20: 2o= z2 & 2r = b and
2o <= 2r by A4;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A21: 2o1 = x * 2o & 2r1 = x * 2r;
2o< 2r by A2,A18,A20,XXREAL_1:3;
then
A22: 2r1 < 2o1 by A1,A21,XREAL_1:69;
a <= z2 by A2,A18,XXREAL_1:3;
then consider 1o,1ra being Real such that
A23: 1o= a & 1ra = z2 and
A24: 1o <= 1ra;
x * 1ra <= x * 1o by A1,A24,XREAL_1:65;
hence thesis by A7,A5,A8,A6,A19,A23,A20,A21,A22,XXREAL_1:2;
end;
then x ** A = ].g,d.] by A9;
hence thesis by A8,MEASURE5:def 5;
end;
case
A25: a in REAL & b = +infty;
consider s being Real such that
A26: s = a;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A27: d = x * s;
consider c being R_eal such that
A28: c = -infty;
A29: ].c,d.] c= x ** A
proof
let q be object;
assume
A30: q in ].c,d.];
then reconsider q as Real by A27;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A31: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A32: a <= q3
proof
q1 <= d & x * q2 = q by A1,A30,XCMPLX_1:87,XXREAL_1:2;
hence thesis by A1,A26,A27,XREAL_1:69;
end;
q3 < b by A25,XXREAL_0:9;
hence thesis by A2,A32,XXREAL_1:3;
end;
q = x * q2 by A1,XCMPLX_1:87;
hence thesis by A31,MEMBER_1:193;
end;
x ** A c= ].c,d.]
proof
let q be object;
assume
A33: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A34: z2 in A and
A35: q = x * z2 by A33,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A36: -infty < q by XXREAL_0:12;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A34,XXREAL_1:3;
then consider o,r being Real such that
A37: o = a & r = z2 and
A38: o <= r;
x * r <= x * o by A1,A38,XREAL_1:65;
hence thesis by A26,A28,A27,A35,A37,A36,XXREAL_1:2;
end;
then x ** A = ].c,d.] by A29;
hence thesis by A27,MEASURE5:def 5;
end;
case
a = +infty & b = +infty;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th11:
for A being non empty Interval, x being Real st 0 < x holds A is
left_open_interval implies x ** A is left_open_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
assume A is left_open_interval;
then consider a being R_eal,b being Real such that
A2: A = ].a,b.] by MEASURE5:def 5;
A3: a < b by A2,XXREAL_1:26;
reconsider b as R_eal by XXREAL_0:def 1;
now
per cases by A3,Th5;
case
a = -infty & b = -infty;
hence thesis;
end;
case
A4: a = -infty & b in REAL;
consider s being Real such that
A5: s = b;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A6: d = x * s;
consider c being R_eal such that
A7: c = -infty;
A8: ].c,d.] c= x ** A
proof
let q be object;
assume
A9: q in ].c,d.];
then reconsider q as Real by A6;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A10: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A12: q3 <= b
proof
q1 <= d & x * q2 = q by A1,A9,XCMPLX_1:87,XXREAL_1:2;
hence thesis by A1,A5,A6,XREAL_1:68;
end;
a < q3 by A4,XXREAL_0:12;
hence thesis by A2,A12,XXREAL_1:2;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A10,MEMBER_1:193;
end;
x ** A c= ].c,d.]
proof
let q be object;
assume
A13: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A16: -infty < q by XXREAL_0:12;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A2,A14,XXREAL_1:2;
then consider r,o being Real such that
A17: r = z2 & o = b and
A18: r <= o;
x * r <= x * o by A1,A18,XREAL_1:64;
hence thesis by A5,A7,A6,A15,A17,A16,XXREAL_1:2;
end;
then x ** A = ].c,d.] by A8;
hence thesis by A6,MEASURE5:def 5;
end;
case
a = -infty & b = +infty;
hence thesis;
end;
case
A19: a in REAL & b in REAL;
then reconsider s = a as Real;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A20: d = x * s;
consider r being Real such that
A21: r = b;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A22: g = x * r;
A23: ].d,g.] c= x ** A
proof
let q be object;
assume
A24: q in ].d,g.];
then reconsider q as Real by A22;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A25: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A27: q3 <= b
proof
q1 <= g by A24,XXREAL_1:2;
then consider p,o being Real such that
A28: p = q1 & o = g and
A29: p <= o by A22;
p/x <= o/x by A1,A29,XREAL_1:72;
hence thesis by A1,A21,A22,A28,XCMPLX_1:89;
end;
d < q1 & x * q2 = q by A1,A24,XCMPLX_1:87,XXREAL_1:2;
then a < q3 by A1,A20,XREAL_1:64;
hence thesis by A2,A27,XXREAL_1:2;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A25,MEMBER_1:193;
end;
x ** A c= ].d,g.]
proof
let q be object;
assume
A30: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A31: z2 in A and
A32: q = x * z2 by A30,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A31,XXREAL_1:2;
then consider 1o,1ra being Real such that
A33: 1o= a & 1ra = z2 and
1o <= 1ra by A19;
1o< 1ra by A2,A31,A33,XXREAL_1:2;
then
A34: x * 1o < x * 1ra by A1,XREAL_1:68;
z2 <= b by A2,A31,XXREAL_1:2;
then consider 2o,2r being Real such that
A35: 2o= z2 & 2r = b and
A36: 2o <= 2r;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A37: 2o1 = x * 2o & 2r1 = x * 2r;
2o1 <= 2r1 by A1,A36,A37,XREAL_1:64;
hence thesis by A21,A20,A22,A32,A33,A35,A34,A37,XXREAL_1:2;
end;
then x ** A = ].d,g.] by A23;
hence thesis by A22,MEASURE5:def 5;
end;
case
a in REAL & b = +infty;
hence thesis;
end;
case
a = +infty & b = +infty;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th12:
for A being non empty Interval, x being Real st x < 0 holds A is
left_open_interval implies x ** A is right_open_interval
proof
let A be non empty Interval;
let x be Real;
assume
A1: x < 0;
assume A is left_open_interval;
then consider a being R_eal,b being Real such that
A2: A = ].a,b.] by MEASURE5:def 5;
A3: a < b by A2,XXREAL_1:26;
reconsider b as R_eal by XXREAL_0:def 1;
now
per cases by A3,Th5;
case
a = -infty & b = -infty;
hence thesis;
end;
case
A4: a = -infty & b in REAL;
consider s being Real such that
A5: s = b;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A6: d = x * s;
consider c being R_eal such that
A7: c = +infty;
A8: [.d,c.[ c= x ** A
proof
let q be object;
assume
A9: q in [.d,c.[;
then reconsider q as Element of REAL by A6,XREAL_0:def 1;
consider q2 being Real such that
A10: q2 = q / x;
reconsider q2 as Element of REAL by XREAL_0:def 1;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A11: q1 = q;
A12: q2 in A
proof
q2 is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A13: q3 = q2;
A14: q3 <= b
proof
d <= q1 & x * q2 = q by A1,A9,A11,A10,XCMPLX_1:87,XXREAL_1:3;
hence thesis by A1,A5,A6,A11,A13,XREAL_1:69;
end;
a < q3 by A4,A13,XXREAL_0:12;
hence thesis by A2,A13,A14,XXREAL_1:2;
end;
q = x * q2 by A1,A10,XCMPLX_1:87;
hence thesis by A12,MEMBER_1:193;
end;
x ** A c= [.d,c.[
proof
let q be object;
assume
A15: q in x ** A;
then reconsider q as Element of REAL;
consider z2 being Real such that
A16: z2 in A and
A17: q = x * z2 by A15,INTEGRA2:39;
reconsider q as R_eal by XXREAL_0:def 1;
A18: q < +infty by XXREAL_0:9;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A2,A16,XXREAL_1:2;
then consider r,o being Real such that
A19: r = z2 & o = b and
A20: r <= o;
x * o <= x * r by A1,A20,XREAL_1:65;
hence thesis by A5,A7,A6,A17,A19,A18,XXREAL_1:3;
end;
then x ** A = [.d,c.[ by A8;
hence thesis by A6,MEASURE5:def 4;
end;
case
a = -infty & b = +infty;
hence thesis;
end;
case
A21: a in REAL & b in REAL;
then reconsider s = a, r = b as Real;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A22: d = x * s;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A23: g = x * r;
A24: [.g,d.[ c= x ** A
proof
let q be object;
assume
A25: q in [.g,d.[;
then reconsider q as Real by A23;
consider q2 being Real such that
A26: q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A27: q1 = q;
A28: q1 < d by A25,A27,XXREAL_1:3;
A29: q2 in A
proof
q2 is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A30: q3 = q2;
A31: q3 <= b
proof
g <= q1 by A25,A27,XXREAL_1:3;
then consider p,o being Real such that
A32: p = g & o = q1 and
A33: p <= o by A23,A27;
o/x <= p/x by A1,A33,XREAL_1:73;
hence thesis by A1,A23,A27,A26,A30,A32,XCMPLX_1:89;
end;
x * q2 = q by A1,A26,XCMPLX_1:87;
then a < q3 by A1,A22,A27,A28,A30,XREAL_1:65;
hence thesis by A2,A30,A31,XXREAL_1:2;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A26,A29,MEMBER_1:193;
end;
x ** A c= [.g,d.[
proof
let q be object;
assume
A34: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A35: z2 in A and
A36: q = x * z2 by A34,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2,A35,XXREAL_1:2;
then consider 1o,1ra being Real such that
A37: 1o= a & 1ra = z2 and
1o <= 1ra by A21;
1o< 1ra by A2,A35,A37,XXREAL_1:2;
then
A38: x * 1ra < x * 1o by A1,XREAL_1:69;
z2 <= b by A2,A35,XXREAL_1:2;
then consider 2o,2r being Real such that
A39: 2o= z2 & 2r = b and
A40: 2o <= 2r;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A41: 2o1 = x * 2o & 2r1 = x * 2r;
2r1 <= 2o1 by A1,A40,A41,XREAL_1:65;
hence thesis by A22,A23,A36,A37,A39,A38,A41,XXREAL_1:3;
end;
then x ** A = [.g,d.[ by A24;
hence thesis by A23,MEASURE5:def 4;
end;
case
a in REAL & b = +infty;
hence thesis;
end;
case
a = +infty & b = +infty;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = [.inf A,sup A.] implies (B =
[.inf B,sup B.] & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t)
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
let B be non empty Interval;
assume
A2: B = x ** A;
A = [.inf A,sup A.] implies (B = [.inf B,sup B.] & for s,t being Real st
s = inf A & t = sup A holds inf B = x * s & sup B = x * t)
proof
assume
A3: A = [.inf A,sup A.];
A4: for s,t being Real st s = inf A & t = sup A holds inf B = x * s & sup
B = x * t
proof
let s,t be Real;
assume that
A5: s = inf A and
A6: t = sup A;
inf B = x * s & sup B = x * t
proof
s <= t by A5,A6,XXREAL_2:40;
then
A7: x * s <= x * t by A1,XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A9: g = x * t;
A10: [.d,g.] c= x ** A
proof
let q be object;
assume
A11: q in [.d,g.];
then reconsider q as Real by A8,A9;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A12: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A14: q3 <= sup A
proof
q1 <= g by A11,XXREAL_1:1;
then consider p,o being Real such that
A15: p = q1 & o = g and
A16: p <= o by A9;
p/x <= o/x by A1,A16,XREAL_1:72;
hence thesis by A1,A6,A9,A15,XCMPLX_1:89;
end;
inf A <= q3
proof
d <= q1 & x * q2 = q by A1,A11,XCMPLX_1:87,XXREAL_1:1;
hence thesis by A1,A5,A8,XREAL_1:68;
end;
hence thesis by A3,A14,XXREAL_1:1;
end;
q = x * q2 by A1,XCMPLX_1:87;
hence thesis by A12,MEMBER_1:193;
end;
x ** A c= [.d,g.]
proof
let q be object;
assume
A17: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
inf A <= z2 by A3,A18,XXREAL_1:1;
then consider 1o,1ra being Real such that
A20: 1o= inf A & 1ra = z2 and
A21: 1o <= 1ra by A5;
A22: x * 1o <= x * 1ra by A1,A21,XREAL_1:64;
z2 <= sup A by A3,A18,XXREAL_1:1;
then consider 2o,2r being Real such that
A23: 2o= z2 & 2r = sup A and
A24: 2o <= 2r by A6;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A25: 2o1 = x * 2o & 2r1 = x * 2r;
2o1 <= 2r1 by A1,A24,A25,XREAL_1:64;
hence thesis by A5,A6,A8,A9,A19,A20,A23,A22,A25,XXREAL_1:1;
end;
then x ** A = [.d,g.] by A10;
hence thesis by A2,A8,A9,A7,MEASURE6:10,14;
end;
hence thesis;
end;
inf A <= sup A by XXREAL_2:40;
then inf A in A & sup A in A by A3,XXREAL_1:1;
then A is closed_interval by A3,MEASURE5:def 3;
then x ** A is closed_interval by A1,Th8;
hence thesis by A2,A4,MEASURE6:17;
end;
hence thesis;
end;
theorem
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = ].inf A,sup A.] implies (B =
].inf B,sup B.] & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t)
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
let B be non empty Interval;
assume
A2: B = x ** A;
A3: inf A <= sup A by XXREAL_2:40;
assume
A4: A = ].inf A,sup A.];
then inf A <> sup A;
then inf A < sup A by A3,XXREAL_0:1;
then sup A in A by A4,XXREAL_1:2;
then reconsider b = sup A as Real;
A5: for s,t being Real st s = inf A & t = sup A holds inf B = x * s & sup B
= x * t
proof
let s,t be Real;
assume that
A6: s = inf A and
A7: t = sup A;
inf B = x * s & sup B = x * t
proof
s <= t by A6,A7,XXREAL_2:40;
then
A8: x * s <= x * t by A1,XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A9: d = x * s;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A10: g = x * t;
A11: ].d,g.] c= x ** A
proof
let q be object;
assume
A12: q in ].d,g.];
then reconsider q as Real by A10;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A13: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A14: q3 <= sup A
proof
q1 <= g by A12,XXREAL_1:2;
then consider p,o being Real such that
A15: p = q1 & o = g and
A16: p <= o by A10;
p/x <= o/x by A1,A16,XREAL_1:72;
hence thesis by A1,A7,A10,A15,XCMPLX_1:89;
end;
d < q1 & x * q2 = q by A1,A12,XCMPLX_1:87,XXREAL_1:2;
then inf A < q3 by A1,A6,A9,XREAL_1:64;
hence thesis by A4,A14,XXREAL_1:2;
end;
q = x * q2 by A1,XCMPLX_1:87;
hence thesis by A13,MEMBER_1:193;
end;
x ** A c= ].d,g.]
proof
let q be object;
assume
A17: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
reconsider q as R_eal by XXREAL_0:def 1;
inf A <= z2 by A4,A18,XXREAL_1:2;
then consider 1o,1ra being Real such that
A20: 1o= inf A & 1ra = z2 and
1o <= 1ra by A6;
1o< 1ra by A4,A18,A20,XXREAL_1:2;
then
A21: d < q by A1,A6,A9,A19,A20,XREAL_1:68;
z2 <= sup A by A4,A18,XXREAL_1:2;
then consider 2o,2r being Real such that
A22: 2o= z2 & 2r = sup A and
A23: 2o <= 2r by A7;
x * 2o <= x * 2r by A1,A23,XREAL_1:64;
hence thesis by A7,A10,A19,A22,A21,XXREAL_1:2;
end;
then x ** A = ].d,g.] by A11;
hence thesis by A2,A9,A10,A8,MEASURE6:9,13;
end;
hence thesis;
end;
A = ].inf A,b.] by A4;
then A is left_open_interval by MEASURE5:def 5;
then B is left_open_interval by A1,A2,Th11;
hence thesis by A5,MEASURE6:19;
end;
theorem
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = ].inf A,sup A.[ implies (B =
].inf B,sup B.[ & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t)
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
let B be non empty Interval;
assume
A2: B = x ** A;
A = ].inf A,sup A.[ implies (B = ].inf B,sup B.[ & for s,t being Real st
s = inf A & t = sup A holds inf B = x * s & sup B = x * t)
proof
assume
A3: A = ].inf A,sup A.[;
A4: for s,t being Real st s = inf A & t = sup A holds inf B = x * s & sup
B = x * t & B is open_interval
proof
let s,t be Real;
assume that
A5: s = inf A and
A6: t = sup A;
inf B = x * s & sup B = x * t & B is open_interval
proof
s <= t by A5,A6,XXREAL_2:40;
then
A7: x * s <= x * t by A1,XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A9: g = x * t;
A10: ].d,g.[ c= x ** A
proof
let q be object;
assume
A11: q in ].d,g.[;
then reconsider q as Real;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A12: q1 = q;
A13: q1 < g by A11,A12,MEASURE5:def 1;
A14: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A16: q3 < sup A
proof
consider p,o being Real such that
A17: p = q1 & o = g and
p <= o by A9,A12,A13;
p/x < o/x by A1,A13,A17,XREAL_1:74;
hence thesis by A1,A6,A9,A12,A17,XCMPLX_1:89;
end;
d < q1 & x * q2 = q by A1,A11,A12,MEASURE5:def 1,XCMPLX_1:87;
then inf A < q3 by A1,A5,A8,A12,XREAL_1:64;
hence thesis by A3,A16,MEASURE5:def 1;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A14,MEMBER_1:193;
end;
x ** A c= ].d,g.[
proof
let q be object;
assume
A18: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A19: z2 in A and
A20: q = x * z2 by A18,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
inf A <= z2 by A3,A19,MEASURE5:def 1;
then consider 1o,1ra being Real such that
A21: 1o= inf A & 1ra = z2 and
1o <= 1ra by A5;
1o< 1ra by A3,A19,A21,MEASURE5:def 1;
then
A22: x * 1o < x * 1ra by A1,XREAL_1:68;
z2 <= sup A by A3,A19,MEASURE5:def 1;
then consider 2o,2r being Real such that
A23: 2o= z2 & 2r = sup A and
2o <= 2r by A6;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A24: 2o1 = x * 2o & 2r1 = x * 2r;
2o< 2r by A3,A19,A23,MEASURE5:def 1;
then 2o1 < 2r1 by A1,A24,XREAL_1:68;
hence thesis by A5,A6,A8,A9,A20,A21,A23,A22,A24,MEASURE5:def 1;
end;
then x ** A = ].d,g.[ by A10;
hence thesis by A2,A8,A9,A7,MEASURE5:def 2,MEASURE6:8,12;
end;
hence thesis;
end;
A is open_interval by A3,MEASURE5:def 2;
then x ** A is open_interval by A1,Th7;
hence thesis by A2,A4,MEASURE6:16;
end;
hence thesis;
end;
theorem
for A being non empty Interval, x being Real st 0 < x for B
being non empty Interval st B = x ** A holds A = [.inf A,sup A.[ implies (B =
[.inf B,sup B.[ & for s,t being Real st s = inf A & t = sup A holds inf B = x *
s & sup B = x * t)
proof
let A be non empty Interval;
let x be Real;
assume
A1: 0 < x;
let B be non empty Interval;
assume
A2: B = x ** A;
A3: inf A <= sup A by XXREAL_2:40;
assume
A4: A = [.inf A,sup A.[;
then inf A <> sup A;
then inf A < sup A by A3,XXREAL_0:1;
then inf A in A by A4,XXREAL_1:3;
then reconsider a = inf A as Real;
A5: for s,t being Real st s = inf A & t = sup A holds inf B = x * s & sup B
= x * t & B is right_open_interval
proof
let s,t be Real;
assume that
A6: s = inf A and
A7: t = sup A;
inf B = x * s & sup B = x * t & B is right_open_interval
proof
s <= t by A6,A7,XXREAL_2:40;
then
A8: x * s <= x * t by A1,XREAL_1:64;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A9: d = x * s;
x * t is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A10: g = x * t;
A11: [.d,g.[ c= x ** A
proof
let q be object;
assume
A12: q in [.d,g.[;
then reconsider q as Real by A9;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A13: q1 < g by A12,XXREAL_1:3;
A14: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
inf A <= q3 & q3 < sup A & q3 in REAL
proof
A15: q3 < sup A
proof
consider p,o being Real such that
A16: p = q1 & o = g and
p <= o by A10,A13;
q1 < g by A12,XXREAL_1:3;
then p/x < o/x by A1,A16,XREAL_1:74;
hence thesis by A1,A7,A10,A16,XCMPLX_1:89;
end;
d <= q1 & x * q2 = q by A1,A12,XCMPLX_1:87,XXREAL_1:3;
hence thesis by A1,A6,A9,A15,XREAL_1:68;
end;
hence thesis by A4,XXREAL_1:3;
end;
q = x * (q / x) by A1,XCMPLX_1:87;
hence thesis by A14,MEMBER_1:193;
end;
x ** A c= [.d,g.[
proof
let q be object;
assume
A17: q in x ** A;
then reconsider q as Real;
consider z2 being Real such that
A18: z2 in A and
A19: q = x * z2 by A17,INTEGRA2:39;
reconsider z2 as R_eal by XXREAL_0:def 1;
z2 <= sup A by A4,A18,XXREAL_1:3;
then consider 2o,2r being Real such that
A20: 2o= z2 & 2r = sup A and
2o <= 2r by A7;
x * 2o is R_eal & x * 2r is R_eal by XXREAL_0:def 1;
then consider 2o1,2r1 being R_eal such that
A21: 2o1 = x * 2o & 2r1 = x * 2r;
2o< 2r by A4,A18,A20,XXREAL_1:3;
then
A22: 2o1 < 2r1 by A1,A21,XREAL_1:68;
inf A <= z2 by A4,A18,XXREAL_1:3;
then consider 1o,1ra being Real such that
A23: 1o= inf A & 1ra = z2 and
A24: 1o <= 1ra by A6;
x * 1o <= x * 1ra by A1,A24,XREAL_1:64;
hence thesis by A6,A7,A9,A10,A19,A23,A20,A21,A22,XXREAL_1:3;
end;
then x ** A = [.d,g.[ by A11;
hence thesis by A2,A9,A10,A8,MEASURE5:def 4,MEASURE6:11,15;
end;
hence thesis;
end;
A = [.a,sup A.[ by A4;
then A is right_open_interval by MEASURE5:def 4;
then x ** A is right_open_interval by A1,Th9;
hence thesis by A2,A5,MEASURE6:18;
end;
theorem Th17:
for A being non empty Interval, x being Real holds x ** A is
Interval
proof
let A be non empty Interval;
let x be Real;
per cases;
suppose
x = 0;
hence thesis by Th6;
end;
suppose
A1: x <> 0;
now
per cases by MEASURE5:1;
case
A is open_interval;
then x ** A is open_interval by A1,Th7;
hence thesis;
end;
case
A is closed_interval;
then x ** A is closed_interval by A1,Th8;
hence thesis;
end;
case
A2: A is right_open_interval;
per cases by A1;
case
x < 0;
then x ** A is left_open_interval by A2,Th10;
hence thesis;
end;
case
0 < x;
then x ** A is right_open_interval by A2,Th9;
hence thesis;
end;
end;
case
A3: A is left_open_interval;
now
per cases by A1;
case
x < 0;
then x ** A is right_open_interval by A3,Th12;
hence thesis;
end;
case
0 < x;
then x ** A is left_open_interval by A3,Th11;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
let A be interval Subset of REAL;
let x be Real;
cluster x ** A -> interval;
correctness
proof
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
hence thesis by Th17;
end;
end;
end;
Lm1: for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_above holds A is bounded_above
proof
let A be non empty Subset of REAL, x be Real such that
A1: x > 0 and
A2: x**A is bounded_above;
A3: sup(x**A) <> +infty by A2;
consider r being Real such that
A4: r in A by MEMBERED:9;
per cases by A3,XXREAL_0:14;
suppose
A5: sup(x**A) = -infty;
take 0;
A6: x*r in x**A by A4,MEMBER_1:193;
-infty is UpperBound of x**A by A5,XXREAL_2:def 3;
hence thesis by A6,XXREAL_0:6,XXREAL_2:def 1;
end;
suppose
sup(x**A) in REAL;
then reconsider r = sup(x**A) as Real;
take r/x;
let z be ExtReal;
assume
A7: z in A;
x" ** (x ** A) = A by A1,Th1;
then consider s being Real such that
A8: s in x**A and
A9: z = x" * s by A7,INTEGRA2:39;
s <= r by A8,XXREAL_2:4;
then s/x <= r/x by A1,XREAL_1:72;
hence thesis by A9;
end;
end;
theorem Th18:
for A being non empty Subset of REAL, x being Real, y being
R_eal st x = y & 0 <= y holds sup(x ** A) = y * sup A
proof
let A be non empty Subset of REAL, x being Real,
y being R_eal such that
A1: x = y and
A2: 0 <= y;
reconsider Y = x ** A as non empty Subset of REAL;
per cases;
suppose
A3: A is not bounded_above;
per cases by A2;
suppose
A4: y = 0;
then x ** A = {0} by A1,INTEGRA2:40;
hence sup(x ** A) = 0 by XXREAL_2:11
.= y * sup A by A4;
end;
suppose
A5: y > 0;
then Y is not bounded_above by A1,A3,Lm1;
hence sup(x ** A) = +infty by XXREAL_2:73
.= y * +infty by A5,XXREAL_3:def 5
.= y * sup A by A3,XXREAL_2:73;
end;
end;
suppose
A is bounded_above;
then reconsider X = A as non empty bounded_above real-membered set;
reconsider u = upper_bound X as Real;
x ** X is bounded_above by A1,A2,INTEGRA2:9;
then reconsider Y as non empty bounded_above real-membered set;
thus sup(x ** A) = upper_bound Y .= x * u by A1,A2,INTEGRA2:13
.= y * sup A by A1,EXTREAL1:1;
end;
end;
Lm2: for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_below holds A is bounded_below
proof
let A be non empty Subset of REAL, x be Real such that
A1: x > 0 and
A2: x**A is bounded_below;
A3: inf(x**A) <> -infty by A2;
consider r being Real such that
A4: r in A by MEMBERED:9;
per cases by A3,XXREAL_0:14;
suppose
A5: inf(x**A) = +infty;
take 0;
A6: x*r in x**A by A4,MEMBER_1:193;
+infty is LowerBound of x**A by A5,XXREAL_2:def 4;
hence thesis by A6,XXREAL_0:4,XXREAL_2:def 2;
end;
suppose
inf(x**A) in REAL;
then reconsider r = inf(x**A) as Real;
take r/x;
let z be ExtReal;
assume
A7: z in A;
x" ** (x ** A) = A by A1,Th1;
then consider s being Real such that
A8: s in x**A and
A9: z = x" * s by A7,INTEGRA2:39;
r/x <= s/x by A1,A8,XREAL_1:72,XXREAL_2:3;
hence thesis by A9;
end;
end;
theorem Th19:
for A being non empty Subset of REAL, x being Real, y being
R_eal st x = y & 0 <= y holds inf(x ** A) = y * inf A
proof
let A be non empty Subset of REAL, x being Real,
y being R_eal such that
A1: x = y and
A2: 0 <= y;
reconsider Y = x ** A as non empty Subset of REAL;
per cases;
suppose
A3: A is not bounded_below;
per cases by A2;
suppose
A4: y = 0;
then x ** A = {0} by A1,INTEGRA2:40;
hence inf(x ** A) = 0 by XXREAL_2:13
.= y * inf A by A4;
end;
suppose
A5: y > 0;
then Y is not bounded_below by A1,A3,Lm2;
hence inf(x ** A) = -infty by XXREAL_2:74
.= y * -infty by A5,XXREAL_3:def 5
.= y * inf A by A3,XXREAL_2:74;
end;
end;
suppose
A is bounded_below;
then reconsider X = A as non empty bounded_below real-membered set;
reconsider u = lower_bound X as Real;
x ** X is bounded_below by A1,A2,INTEGRA2:11;
then reconsider Y as non empty bounded_below real-membered set;
thus inf(x ** A) = lower_bound Y .= x * u by A1,A2,INTEGRA2:15
.= y * inf A by A1,EXTREAL1:1;
end;
end;
theorem
for A being Interval, x,y being Real st 0 <= x & y
= diameter(A) holds x * y = diameter(x ** A)
proof
let A be Interval;
let x,y be Real such that
A1: 0 <= x and
A2: y = diameter(A);
per cases;
suppose
A3: A is empty;
then
A4: x ** A is empty;
thus x * y = 0 by A2,A3,MEASURE5:10
.= diameter(x ** A) by A4,MEASURE5:10;
end;
suppose
A5: A is non empty;
then consider z being Real such that
A6: z in A;
reconsider z as Real;
A7: x * z in x ** A by A6,MEMBER_1:193;
reconsider AA = A as non empty Subset of REAL by A5;
reconsider u = x as R_eal by XXREAL_0:def 1;
A8: inf(x ** AA) = u * inf AA by A1,Th19;
reconsider z = x as R_eal by XXREAL_0:def 1;
thus x * y = z * diameter A by A2,EXTREAL1:1
.= z * (sup A - inf A) by A5,MEASURE5:def 6
.= z * sup A - (z * inf A) by XXREAL_3:100
.= sup(x ** A) - inf(x ** A) by A1,A8,Th18
.= diameter(x ** A) by A7,MEASURE5:def 6;
end;
end;
theorem Th21:
for eps being Real st 0 < eps
ex n being Nat st 1 < 2|^n * eps
proof
let eps be Real;
assume
A1: 0 < eps;
consider n being Nat such that
A2: 1 / eps < n by SEQ_4:3;
take n;
n < 2|^n by NEWTON:86;
then 1/eps < 2|^n by A2,XXREAL_0:2;
then 1/eps * eps < 2|^n * eps by A1,XREAL_1:68;
hence thesis by A1,XCMPLX_1:87;
end;
theorem Th22:
for a,b being Real st 0 <= a & 1 < b - a
ex n being Nat st a < n & n < b
proof
let a,b be Real;
assume that
A1: 0 <= a and
A2: 1 < b - a;
a < [\a/]+1 by INT_1:29;
reconsider n = [\a/]+1 as Element of NAT by A1,INT_1:3;
take n;
thus a < n by INT_1:29;
[\a/] <= a by INT_1:def 6;
then
A3: [\a/]+1 <= a+1 by XREAL_1:6;
1+a < b by A2,XREAL_1:20;
hence thesis by A3,XXREAL_0:2;
end;
theorem
for n being Nat holds dyadic(n) c= DYADIC
by URYSOHN1:def 2;
theorem Th24:
for a,b being Real st a < b & 0 <= a & b <= 1
ex c being Real st c in DYADIC & a < c & c < b
proof
let a,b be Real;
assume that
A1: a < b and
A2: 0 <= a and
A3: b <= 1;
set eps = b - a;
consider n being Nat such that
A4: 1 < 2|^n * eps by A1,Th21,XREAL_1:50;
set aa = 2|^n * a, bb = 2|^n * b;
1 < bb - aa by A4;
then consider m being Nat such that
A5: aa < m and
A6: m < bb by A2,Th22;
set x = m / 2|^n;
take x;
A7: 0 < 2|^n by NEWTON:83;
m / 2|^n < b by A6,NEWTON:83,XREAL_1:83;
then m / 2|^n < 1 by A3,XXREAL_0:2;
then m < 2|^n by A7,XREAL_1:181;
then x in dyadic(n) by URYSOHN1:def 1;
hence thesis by A7,A5,A6,URYSOHN1:def 2,XREAL_1:81,83;
end;
theorem Th25:
for a,b being Real st a < b
ex c being Real st c in DOM & a < c & c < b
proof
let a,b be Real;
assume
A1: a < b;
per cases;
suppose
A2: a < 0 & b <= 1;
now
per cases;
case
A3: b <= 0;
consider c being Real such that
A4: a < c and
A5: c < b by A1,XREAL_1:5;
reconsider c as Real;
halfline 0 = {g where g is Real : g<0} by XXREAL_1:229;
then c in halfline 0 by A3,A5;
then c in (halfline 0) \/ DYADIC by XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
hence thesis by A4,A5;
end;
case
A6: 0 < b;
set a1 = 0;
consider c being Real such that
A7: c in DYADIC and
A8: a1 < c & c < b by A2,A6,Th24;
c in (halfline 0) \/ DYADIC by A7,XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
hence thesis by A2,A8;
end;
end;
hence thesis;
end;
suppose
A9: a < 0 & 1 < b;
consider a1,b1 being Real such that
A10: a1 = 0 & b1 = 1;
consider c being Real such that
A11: c in DYADIC and
A12: a1 < c & c < b1 by A10,Th24;
take c;
c in (halfline 0) \/ DYADIC by A11,XBOOLE_0:def 3;
hence thesis by A9,A10,A12,URYSOHN1:def 3,XBOOLE_0:def 3,XXREAL_0:2;
end;
suppose
0 <= a & b <= 1;
then consider c being Real such that
A13: c in DYADIC and
A14: a < c & c < b by A1,Th24;
take c;
c in (halfline 0) \/ DYADIC by A13,XBOOLE_0:def 3;
hence thesis by A14,URYSOHN1:def 3,XBOOLE_0:def 3;
end;
suppose
A15: 0 <= a & 1 < b;
now
per cases;
case
A16: 1 <= a;
consider c being Real such that
A17: a < c and
A18: c < b by A1,XREAL_1:5;
reconsider c as Real;
right_open_halfline 1 =
{g where g is Real : 1<g} & 1 < c by A16,A17,
XXREAL_0:2,XXREAL_1:230;
then c in right_open_halfline 1;
then c in DYADIC \/ (right_open_halfline 1) by XBOOLE_0:def 3;
then c in (halfline 0) \/ (DYADIC \/ right_open_halfline 1) by
XBOOLE_0:def 3;
then c in DOM by URYSOHN1:def 3,XBOOLE_1:4;
hence thesis by A17,A18;
end;
case
A19: a < 1;
set b1 = 1;
consider c being Real such that
A20: c in DYADIC and
A21: a < c and
A22: c < b1 by A15,A19,Th24;
c in (halfline 0) \/ DYADIC by A20,XBOOLE_0:def 3;
then
A23: c in DOM by URYSOHN1:def 3,XBOOLE_0:def 3;
c < b by A15,A22,XXREAL_0:2;
hence thesis by A21,A23;
end;
end;
hence thesis;
end;
end;
theorem
for A being non empty Subset of ExtREAL holds for a,b being R_eal st A
c= [.a,b.] holds a <= inf A & sup A <= b
proof
let A be non empty Subset of ExtREAL;
let a,b be R_eal;
assume
A1: A c= [.a,b.];
then reconsider B = [.a,b.] as non empty Subset of ExtREAL by MEMBERED:2;
for x being ExtReal st x in B holds x <= b by XXREAL_1:1;
then b is UpperBound of B by XXREAL_2:def 1;
then
A2: b is UpperBound of A by A1,XXREAL_2:6;
for x being ExtReal holds (x in B implies a <= x) by XXREAL_1:1;
then a is LowerBound of B by XXREAL_2:def 2;
then a is LowerBound of A by A1,XXREAL_2:5;
hence thesis by A2,XXREAL_2:def 3,def 4;
end;
theorem
0 in DYADIC & 1 in DYADIC
proof
0 in dyadic(0) & 1 in dyadic(0) by URYSOHN1:6;
hence thesis by URYSOHN1:def 2;
end;
theorem
DYADIC c= [. 0,1 .]
proof
let x be object;
assume
A1: x in DYADIC;
then reconsider x as Real;
A2: ex n being Nat st x in dyadic(n) by A1,URYSOHN1:def 2;
reconsider x as R_eal by XXREAL_0:def 1;
0 <= x & x <= 1 by A2,URYSOHN1:1;
hence thesis by XXREAL_1:1;
end;
theorem
for n,k being Nat st n <= k holds dyadic(n) c= dyadic(k)
proof
let n,k be Nat;
A1: for s being Nat holds dyadic(n) c= dyadic(n+s)
proof
defpred P[Nat] means dyadic(n) c= dyadic(n+$1);
A2: for k being Nat st P[k] holds P[(k+1)]
proof
let k be Nat;
A3: dyadic(n+k) c= dyadic(n+k+1) by URYSOHN1:5;
assume dyadic(n) c= dyadic(n+k);
hence thesis by A3,XBOOLE_1:1;
end;
A4: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
assume n <= k;
then consider s being Nat such that
A5: k = n + s by NAT_1:10;
thus thesis by A1,A5;
end;
theorem Th30: :: JGRAPH_1:31
for a,b,c,d being Real st a < c & c < b & a < d & d < b holds
|.d - c qua Complex.| < b - a
proof
let a,b,c,d be Real;
assume that
A1: a < c and
A2: c < b & a < d and
A3: d < b;
A4: c + a < b + d by A2,XREAL_1:8;
then c - d <= b - a by XREAL_1:21;
then
A5: -(b - a) <= -(c - d) by XREAL_1:24;
A6: a + d < c + b by A1,A3,XREAL_1:8;
A7: |.d - c qua Complex.| <> b - a
proof
assume
A8: |.d - c qua Complex.| = b - a;
A9: d - c = b - a or d - c = -(b - a)
proof
per cases;
suppose
0 <= d - c;
hence thesis by A8,ABSVALUE:def 1;
end;
suppose
not 0 <= d - c;
then b - a = -(d - c) by A8,ABSVALUE:def 1;
hence thesis;
end;
end;
now
per cases by A9;
case
d - c = b - a;
hence thesis by A6;
end;
case
d - c = -(b - a);
hence thesis by A4;
end;
end;
hence thesis;
end;
d - c < b - a by A6,XREAL_1:21;
then |.d - c qua Complex.| <= b - a by A5,ABSVALUE:5;
hence thesis by A7,XXREAL_0:1;
end;
theorem
for eps being Real st 0 < eps
for d being Real st 0 < d
ex r1,r2 being Real
st r1 in DYADIC \/ (right_open_halfline 1) & r2 in DYADIC \/ (
right_open_halfline 1) & 0 < r1 & r1 < d & d < r2 & r2 - r1 < eps
proof
let eps be Real;
assume 0 < eps;
then consider eps1 being Real such that
A1: 0 < eps1 and
A2: eps1 < eps by XREAL_1:5;
reconsider eps1 as Real;
let d be Real;
assume
A3: 0 < d;
per cases;
suppose
eps1 < d;
then
A4: 0 < d - eps1 by XREAL_1:50;
d - eps1 < d - 0 by A1,XREAL_1:15;
then ex c being Real st c in DOM & d - eps1 < c & c < d by Th25;
then consider r1 being Real such that
A5: d - eps1 < r1 and
A6: r1 < d and
A7: r1 in DOM;
r1 in (halfline 0) \/ DYADIC or r1 in right_open_halfline 1 by A7,
URYSOHN1:def 3,XBOOLE_0:def 3;
then
A8: r1 in halfline 0 or r1 in DYADIC or r1 in right_open_halfline 1 by
XBOOLE_0:def 3;
eps - eps < eps - eps1 by A2,XREAL_1:15;
then d + 0 < d + (eps - eps1) by XREAL_1:8;
then ex c being Real st c in DOM & d < c & c < d + (eps - eps1)
by Th25;
then consider r2 being Real such that
A9: d < r2 and
A10: r2 < d + (eps - eps1) and
A11: r2 in DOM;
r2 in halfline 0 \/ DYADIC or r2 in right_open_halfline 1 by A11,
URYSOHN1:def 3,XBOOLE_0:def 3;
then
A12: r2 in halfline 0 or r2 in DYADIC or r2 in right_open_halfline 1 by
XBOOLE_0:def 3;
A13: r1 < r2 by A6,A9,XXREAL_0:2;
then
A14: d - eps1 < r2 by A5,XXREAL_0:2;
take r1,r2;
A15: (d + (eps - eps1)) - (d - eps1) = eps;
r1 < d + (eps - eps1) by A10,A13,XXREAL_0:2;
then
A16: |.r2 - r1 qua Complex.| < eps by A5,A10,A14,A15,Th30;
0 <= r2 - r1 by A13,XREAL_1:48;
hence thesis by A5,A6,A9,A4,A8,A12,A16,ABSVALUE:def 1,XBOOLE_0:def 3
,XXREAL_1:233;
end;
suppose
A17: d <= eps1;
consider r1 being Real such that
A18: r1 in DOM and
A19: 0 < r1 and
A20: r1 < d by A3,Th25;
A21: r1 in halfline 0 \/ DYADIC or r1 in right_open_halfline 1 by A18,
URYSOHN1:def 3,XBOOLE_0:def 3;
0 + d < r1 + eps1 by A17,A19,XREAL_1:8;
then ex c being Real st c in DOM & d < c & c < r1 + eps1 by Th25;
then consider r2 being Real such that
A22: d < r2 and
A23: r2 < r1 + eps1 and
A24: r2 in DOM;
take r1,r2;
A25: r2 in halfline 0 \/ DYADIC or r2 in right_open_halfline 1 by A24,
URYSOHN1:def 3,XBOOLE_0:def 3;
not r1 in halfline 0 by A19,XXREAL_1:233;
then
A26: r1 in DYADIC or r1 in right_open_halfline 1 by A21,XBOOLE_0:def 3;
not r2 in halfline 0 by A3,A22,XXREAL_1:233;
then
A27: r2 in DYADIC or r2 in right_open_halfline 1 by A25,XBOOLE_0:def 3;
r2 - r1 < r1 + eps1 - r1 by A23,XREAL_1:9;
hence thesis by A2,A19,A20,A22,A26,A27,XBOOLE_0:def 3,XXREAL_0:2;
end;
end;
begin :: Addenda
:: missing, 2008.06.10, A.T.
theorem
for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_above holds A is bounded_above by Lm1;
theorem
for A being non empty Subset of REAL, x being Real
st x > 0 & x**A is
bounded_below holds A is bounded_below by Lm2;