:: Basic Properties of Extended Real Numbers
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000-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, SUPINF_1, REAL_1, RELAT_1, XXREAL_0, ARYTM_3, COMPLEX1,
CARD_1, ARYTM_1, FINSEQ_1, CARD_3, FUNCT_1, SUBSET_1, SUPINF_2, NAT_1,
FUNCT_2, FUNCOP_1, XBOOLE_0, TARSKI, ORDINAL4, PARTFUN1, RFINSEQ,
XCMPLX_0, MESFUNC1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0,
XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, RFINSEQ, RFUNCT_3,
RVSUM_1, FUNCOP_1, FINSEQ_1, FINSEQ_4, NAT_1, NAT_D, SUPINF_1, SUPINF_2,
MEASURE6;
constructors BINOP_1, DOMAIN_1, REAL_1, NAT_1, FINSEQ_4, FINSOP_1, RVSUM_1,
SUPINF_2, RFINSEQ, RFUNCT_3, MEASURE6, BINARITH, BINOP_2, SUPINF_1,
CLASSES1, NAT_D, RELSET_1, XXREAL_3, FINSEQ_1, FUNCT_1, FUNCT_2, INT_1,
FUNCOP_1, COMPLEX1, ARYTM_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, VALUED_0, CARD_1, XXREAL_3;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SUPINF_2, XXREAL_3, XCMPLX_0;
theorems FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, NAT_1, TARSKI,
FUNCT_1, INT_1, XCMPLX_1, XBOOLE_0, RFINSEQ, RELAT_1, FUNCOP_1, XREAL_1,
XXREAL_0, XREAL_0, PARTFUN1, ORDINAL1, XXREAL_3, SUPINF_2, ABSVALUE,
COMPLEX1;
schemes FUNCT_2, FINSEQ_2, NAT_1, RECDEF_1;
begin :: Operations "x * y","x / y", "|.x.|" in R_eal numbers
theorem
for x,y being ExtReal, a,b being Real holds x = a & y = b
implies x * y = a * b by XXREAL_3:def 5;
theorem Th2:
for x,y being ExtReal, a,b being Real st x = a & y = b
holds x / y = a / b
proof
let x,y be ExtReal, a,b be Real such that
A1: x = a;
assume y = b;
then y" = b" by XXREAL_3:def 6;
hence thesis by A1,XXREAL_3:def 5;
end;
definition
let x be ExtReal;
func |. x .| -> R_eal equals
:Def1:
x if 0 <= x otherwise -x;
coherence by XXREAL_0:def 1;
consistency;
projectivity;
end;
registration
let x be Real, a be Complex;
identify |.x.| with |.a.| when x = a;
compatibility
proof assume
A1: x = a;
per cases;
suppose
A2: 0 <= x;
hence |.x.| = a by A1,Def1 .= |.a.| by A2,A1,ABSVALUE:def 1;
end;
suppose
A3: 0 > x;
hence |.x.| = -(x qua ExtReal) by Def1
.= |.a.| by A3,A1,ABSVALUE:def 1;
end;
end;
end;
theorem
for x being R_eal st 0 <= x holds |. x .| = x by Def1;
theorem
for x being R_eal st x < 0 holds |. x .| = -x by Def1;
registration let x be R_eal;
cluster |.x.| -> non negative;
coherence
proof per cases;
suppose
A1: 0 <= x;
then |. x .| = x by Def1;
hence thesis by A1;
end;
suppose
A2: x < 0;
then |. x .| = -x by Def1;
hence thesis by A2;
end;
end;
end;
::$CT 2
begin :: Sum of Finite Sequence of Extended Real Numbers
:: from CONVFUN1, 2010.02.13, A.T.
definition
let F be FinSequence of ExtREAL;
func Sum(F) -> R_eal means
:Def2:
ex f being sequence of ExtREAL st it = f.(len F) & f.0 = 0. &
for i being Nat st i < len F holds f.(i+1)= f.i+F.(i+1);
existence
proof
defpred P[FinSequence of ExtREAL] means ex f being sequence of
ExtREAL st f.0 = 0. & for i being Element of NAT st i < len $1 holds f.(i+1) =
f.i+$1.(i+1);
A1: for F being FinSequence of ExtREAL for x being Element of ExtREAL st P
[F] holds P[F^<*x*>]
proof
let F be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume P[F];
then consider f being sequence of ExtREAL such that
A2: f.0 = 0. and
A3: for i being Element of NAT st i < len F holds f.(i+1) = f.i+F.(i +1);
defpred R[Element of NAT,set] means ($1 <= len F implies $2 = f.$1) & (
$1 = (len F)+1 implies $2 = f.(len F) + x);
A4: for i being Element of NAT ex g being Element of ExtREAL st R[i,g]
proof
let i be Element of NAT;
per cases;
suppose
A5: i <> (len F)+1;
take f.i;
thus thesis by A5;
end;
suppose
A6: i = (len F)+1;
take f.(len F) + x;
thus thesis by A6,NAT_1:13;
end;
end;
consider f9 being sequence of ExtREAL such that
A7: for i being Element of NAT holds R[i,f9.i] from FUNCT_2:sch 3(A4
);
thus P[F^<*x*>]
proof
take f9;
thus f9.0 = 0. by A2,A7;
thus for i being Element of NAT st i < len(F^<*x*>) holds f9.(i+1)=f9.
i+(F^<*x*>).(i+1)
proof
let i be Element of NAT;
assume i < len(F^<*x*>);
then i < (len F)+(len <*x*>) by FINSEQ_1:22;
then i < (len F)+1 by FINSEQ_1:39;
then
A8: i <= len F by NAT_1:13;
then
A9: f9.i = f.i by A7;
per cases by A8,XXREAL_0:1;
suppose
A10: i < len F;
then
A11: i+1 <= len F by INT_1:7;
1<=i+1 by NAT_1:12;
then i+1 in Seg len F by A11,FINSEQ_1:1;
then
A12: i+1 in dom F by FINSEQ_1:def 3;
f9.(i+1) = f.(i+1) by A7,A11;
then f9.(i+1)=f9.i+F.(i+1) by A3,A9,A10;
hence thesis by A12,FINSEQ_1:def 7;
end;
suppose
A13: i = len F;
then f9.(i+1) = f9.i + x by A7,A9;
hence thesis by A13,FINSEQ_1:42;
end;
end;
end;
end;
A14: P[<*> ExtREAL]
proof
reconsider f = NAT --> 0. as sequence of ExtREAL;
take f;
thus f.0 = 0. by FUNCOP_1:7;
thus thesis;
end;
for F being FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A14
,A1);
then consider f being sequence of ExtREAL such that
A15: f.0 = 0. and
A16: for i being Element of NAT st i < len F holds f.(i+1) = f.i+F.(i+ 1);
A17: for i being Nat st i < len F holds f.(i+1) = f.i+F.(i+ 1)
proof let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A16;
end;
take f.(len F);
thus thesis by A15,A17;
end;
uniqueness
proof
let g1, g2 be Element of ExtREAL;
given f1 being sequence of ExtREAL such that
A18: g1 = f1.(len F) and
A19: f1.0 = 0. and
A20: for i being Nat st i < len F holds f1.(i+1) = f1.i+F.( i+1);
given f2 being sequence of ExtREAL such that
A21: g2 = f2.(len F) and
A22: f2.0 = 0. and
A23: for i being Nat st i < len F holds f2.(i+1) = f2.i+F.( i+1);
defpred P[Nat] means $1 <= len F implies f1.$1 = f2.$1;
A24: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A25: P[i];
thus P[i+1]
proof
assume i+1 <= len F;
then
A26: i < len F by NAT_1:13;
then f1.(i+1) = f1.i+F.(i+1) by A20;
hence thesis by A23,A25,A26;
end;
end;
A27: P[0] by A19,A22;
for i being Nat holds P[i] from NAT_1:sch 2(A27,A24);
hence thesis by A18,A21;
end;
end;
theorem Th5:
Sum(<*> ExtREAL) = 0.
proof
reconsider F = <*> ExtREAL as FinSequence of ExtREAL;
ex f being sequence of ExtREAL st Sum F = f.(len F) & f.0 = 0. &
for i being Nat st i < len F holds f.(i+1) = f.i+F.(i+1) by Def2;
hence thesis;
end;
theorem Th6:
for a being R_eal holds Sum<*a*> = a
proof
let a be R_eal;
set F = <*a*>;
consider f being sequence of ExtREAL such that
A1: Sum F = f.(len F) and
A2: f.0 = 0. and
A3: for i being Nat st i < len F holds f.(i+1) = f.i+F.(i+1)
by Def2;
A4: f.(0+1) = f.0+F.(0+1) by A3;
Sum F = f.1 by A1,FINSEQ_1:39;
then Sum F = F.1 by A2,A4,XXREAL_3:4
.= a;
hence thesis;
end;
Lm1: for F being FinSequence of ExtREAL, x being Element of ExtREAL holds Sum(
F^<*x*>) = Sum F + x
proof
let F be FinSequence of ExtREAL, x be Element of ExtREAL;
consider f being sequence of ExtREAL such that
A1: Sum(F^<*x*>) = f.(len(F^<*x*>)) and
A2: f.0 = 0. and
A3: for i being Nat st i < len (F^<*x*>) holds f.(i+1)=f.i+(F
^<*x*>).(i+1) by Def2;
A4: len(F^<*x*>) = (len F)+(len <*x*>) by FINSEQ_1:22
.= (len F)+1 by FINSEQ_1:39;
for i being Nat st i < len F holds f.(i+1)=f.i+F.(i+1)
proof
let i be Nat;
A5: 1 <= i+1 by NAT_1:11;
assume
A6: i < len F;
then i+1 <= len F by INT_1:7;
then i+1 in Seg len F by A5,FINSEQ_1:1;
then
A7: i+1 in dom F by FINSEQ_1:def 3;
i < len(F^<*x*>) by A4,A6,NAT_1:13;
then f.(i+1)=f.i+(F^<*x*>).(i+1) by A3;
hence thesis by A7,FINSEQ_1:def 7;
end;
then
A8: Sum F = f.(len F) by A2,Def2;
len F < len(F^<*x*>) by A4,NAT_1:13;
then f.((len F)+1)=f.(len F)+(F^<*x*>).((len F)+1) by A3;
hence thesis by A1,A4,A8,FINSEQ_1:42;
end;
theorem
for a,b being R_eal holds Sum<*a,b*> = a+b
proof
let a,b be R_eal;
thus Sum<*a,b*> = Sum(<*a*>^<*b*>) by FINSEQ_1:def 9
.= Sum<*a*> + b by Lm1
.= a + b by Th6;
end;
Lm2: for F being FinSequence of ExtREAL st not -infty in rng F holds Sum F <>
-infty
proof
defpred P[FinSequence of ExtREAL] means not -infty in rng $1 implies Sum $1
<> -infty;
A1: for F being FinSequence of ExtREAL for x being Element of ExtREAL st P[F
] holds P[F^<*x*>]
proof
let F be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume
A2: P[F];
A3: Sum(F^<*x*>) = Sum F + x by Lm1;
assume not -infty in rng(F^<*x*>);
then
A4: not -infty in rng F \/ rng <*x*> by FINSEQ_1:31;
then not -infty in rng <*x*> by XBOOLE_0:def 3;
then not -infty in {x} by FINSEQ_1:38;
then x <> -infty by TARSKI:def 1;
hence thesis by A2,A4,A3,XBOOLE_0:def 3,XXREAL_3:17;
end;
A5: P[<*> ExtREAL] by Th5;
thus for F being FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2 (A5,
A1);
end;
theorem Th8:
for F,G being FinSequence of ExtREAL st not -infty in rng F & not
-infty in rng G holds Sum(F^G) = Sum(F)+Sum(G)
proof
let F,G be FinSequence of ExtREAL;
defpred P[FinSequence of ExtREAL] means not -infty in rng $1 implies Sum(F^
$1) = Sum(F)+Sum($1);
assume
A1: not -infty in rng F;
A2: for H being FinSequence of ExtREAL for x being Element of ExtREAL st P[H
] holds P[H^<*x*>]
proof
let H be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume
A3: P[H];
thus P[H^<*x*>]
proof
assume not -infty in rng(H^<*x*>);
then
A4: not -infty in rng H \/ rng <*x*> by FINSEQ_1:31;
then not -infty in rng H by XBOOLE_0:def 3;
then
A5: Sum H <> -infty by Lm2;
not -infty in rng <*x*> by A4,XBOOLE_0:def 3;
then not -infty in {x} by FINSEQ_1:38;
then
A6: x <> -infty by TARSKI:def 1;
A7: Sum F <> -infty by A1,Lm2;
F^(H^<*x*>) = F^H^<*x*> by FINSEQ_1:32;
hence Sum(F^(H^<*x*>)) = Sum F + Sum H + x by A3,A4,Lm1,XBOOLE_0:def 3
.= Sum F + (Sum H + x) by A6,A7,A5,XXREAL_3:29
.= Sum F + Sum(H^<*x*>) by Lm1;
end;
end;
assume
A8: not -infty in rng G;
A9: P[<*> ExtREAL]
proof
set H = <*> ExtREAL;
assume not -infty in rng H;
thus Sum(F^H) = Sum F by FINSEQ_1:34
.= Sum F + Sum H by Th5,XXREAL_3:4;
end;
for H being FinSequence of ExtREAL holds P[H] from FINSEQ_2:sch 2 (A9,
A2);
hence thesis by A8;
end;
Lm3: for n,q being Nat st q in Seg(n+1) ex p being Permutation of Seg(n+1) st
for i being Element of NAT st i in Seg(n+1) holds (i<q implies p.i=i) & (i=q
implies p.i=n+1) & (i>q implies p.i=i-1)
proof
let n,q be Nat;
defpred R[Nat,set] means ($1<q implies $2=$1) & ($1=q implies $2=
n+1) & ($1>q implies $2=$1-1);
assume
A1: q in Seg(n+1);
A2: for i being Nat st i in Seg(n+1) ex p being Element of NAT st
R[i,p]
proof
let i be Nat;
assume i in Seg(n+1);
per cases by XXREAL_0:1;
suppose
A3: i<q;
take i;
i in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
suppose
A4: i=q;
take n+1;
thus thesis by A4;
end;
suppose
A5: i>q;
1 <= q by A1,FINSEQ_1:1;
then reconsider p=i-1 as Element of NAT by A5,INT_1:5,XXREAL_0:2;
take p;
thus thesis by A5;
end;
end;
consider p being FinSequence of NAT such that
A6: dom p = Seg(n+1) and
A7: for i being Nat st i in Seg(n+1) holds R[i,p/.i] from
RECDEF_1:sch 17(A2);
A8: for i being Element of NAT st i in Seg(n+1) holds i=q iff p/.i=n+1
proof
let i be Element of NAT;
assume
A9: i in Seg(n+1);
hence i=q implies p/.i=n+1 by A7;
thus p/.i=n+1 implies i=q
proof
assume
A10: p/.i=n+1;
per cases by XXREAL_0:1;
suppose
i=q;
hence thesis;
end;
suppose
i<q;
then n+1<q by A7,A9,A10;
hence thesis by A1,FINSEQ_1:1;
end;
suppose
i>q;
then i-1 = n+1 by A7,A9,A10;
then i >= n+1+1;
then i > n+1 by NAT_1:13;
hence thesis by A9,FINSEQ_1:1;
end;
end;
end;
A11: for i being Element of NAT st i in Seg(n+1) holds (i<q implies p.i=i) &
(i=q implies p.i=n+1) & (i>q implies p.i=i-1)
proof
let i be Element of NAT;
assume
A12: i in Seg(n+1);
then p/.i = p.i by A6,PARTFUN1:def 6;
hence thesis by A7,A12;
end;
for i being object holds i in rng p iff i in Seg(n+1)
proof
let i being object;
thus i in rng p implies i in Seg(n+1)
proof
assume i in rng p;
then consider j being object such that
A13: j in Seg(n+1) and
A14: p.j = i by A6,FUNCT_1:def 3;
reconsider j as Element of NAT by A13;
per cases by XXREAL_0:1;
suppose
j<q;
hence thesis by A11,A13,A14;
end;
suppose
j=q;
then i = n+1 by A11,A13,A14;
hence thesis by FINSEQ_1:4;
end;
suppose
A15: j>q;
then
A16: i = j-1 by A11,A13,A14;
A17: 1 <= q by A1,FINSEQ_1:1;
then reconsider i as Element of NAT by A15,A16,INT_1:5,XXREAL_0:2;
j <= n+1 by A13,FINSEQ_1:1;
then i <= n by A16,XREAL_1:20;
then
A18: i <= n+1 by NAT_1:12;
1 < i+1 by A15,A16,A17,XXREAL_0:2;
then 1 <= i by NAT_1:13;
hence thesis by A18,FINSEQ_1:1;
end;
end;
thus i in Seg(n+1) implies i in rng p
proof
assume
A19: i in Seg(n+1);
then reconsider i as Element of NAT;
i <= n+1 by A19,FINSEQ_1:1;
then
A20: i = n+1 or i < n+1 by XXREAL_0:1;
per cases by A20,NAT_1:13;
suppose
i < q;
then p.i = i by A11,A19;
hence thesis by A6,A19,FUNCT_1:3;
end;
suppose
A21: q <= i & i <= n;
A22: 1 <= i+1 by NAT_1:12;
i+1 <= n+1 by A21,XREAL_1:6;
then
A23: i+1 in Seg(n+1) by A22,FINSEQ_1:1;
q < i+1 by A21,NAT_1:13;
then p.(i+1) = i+1-1 by A11,A23
.= i;
hence thesis by A6,A23,FUNCT_1:3;
end;
suppose
i=n+1;
then p.q = i by A1,A11;
hence thesis by A1,A6,FUNCT_1:3;
end;
end;
end;
then
A24: rng p = Seg(n+1) by TARSKI:2;
then
A25: p is Function of Seg(n+1), Seg(n+1) by A6,FUNCT_2:1;
A26: for i being Element of NAT st i in Seg(n+1) & p/.i<>n+1 holds i<q iff p
/.i<q
proof
let i be Element of NAT;
assume that
A27: i in Seg(n+1) and
A28: p/.i<>n+1;
thus i<q implies p/.i<q by A7,A27;
thus p/.i<q implies i<q
proof
assume
A29: p/.i<q;
per cases by XXREAL_0:1;
suppose
i<q;
hence thesis;
end;
suppose
i=q;
hence thesis by A7,A27,A28;
end;
suppose
A30: i>q;
then p/.i = i-1 by A7,A27;
then i-1+1 < q+1 by A29,XREAL_1:8;
hence thesis by A30,NAT_1:13;
end;
end;
end;
for i1,i2 being object st i1 in Seg(n+1) & i2 in Seg(n+1) & p.i1 = p.i2
holds i1 = i2
proof
let i1,i2 be object;
assume that
A31: i1 in Seg(n+1) and
A32: i2 in Seg(n+1) and
A33: p.i1 = p.i2;
reconsider i1 as Element of NAT by A31;
A34: p/.i1 = p.i1 by A6,A31,PARTFUN1:def 6;
reconsider i2 as Element of NAT by A32;
A35: p/.i2 = p.i2 by A6,A32,PARTFUN1:def 6;
per cases;
suppose
A36: p/.i1 = n+1;
then i1 = q by A8,A31;
hence thesis by A8,A32,A33,A34,A35,A36;
end;
suppose
A37: p/.i1 <> n+1 & p/.i1 < q;
then i1<q by A26,A31;
then
A38: p/.i1=i1 by A7,A31;
i2<q by A26,A32,A33,A34,A35,A37;
hence thesis by A7,A32,A33,A34,A35,A38;
end;
suppose
A39: p/.i1 <> n+1 & p/.i1 >= q;
then
A40: i1 <> q by A8,A31;
i1 >= q by A26,A31,A39;
then i1 > q by A40,XXREAL_0:1;
then
A41: p/.i1=i1-1 by A7,A31;
A42: i2 <> q by A8,A32,A33,A34,A35,A39;
i2 >= q by A26,A32,A33,A34,A35,A39;
then i2 > q by A42,XXREAL_0:1;
then p/.i2=i2-1 by A7,A32;
hence thesis by A6,A32,A33,A34,A41,PARTFUN1:def 6,XCMPLX_1:19;
end;
end;
then p is one-to-one by A6,FUNCT_1:def 4;
then reconsider p as Permutation of Seg(n+1) by A24,A25,FUNCT_2:57;
take p;
thus thesis by A11;
end;
Lm4: for n,q being Nat, s,p being Permutation of Seg(n+1), s9 being
FinSequence of Seg(n+1) st s9=s & q=s.(n+1) & for i being Element of NAT st i
in Seg(n+1) holds (i<q implies p.i=i) & (i=q implies p.i=n+1) & (i>q implies p.
i=i-1) holds p*s9|n is Permutation of Seg n
proof
let n,q be Nat, s,p be Permutation of Seg(n+1), s9 be FinSequence of Seg(n+1
);
assume that
A1: s9=s and
A2: q=s.(n+1) and
A3: for i being Element of NAT st i in Seg(n+1) holds (i<q implies p.i=i
) & (i=q implies p.i=n+1) & (i>q implies p.i=i-1);
A4: dom p = Seg(n+1) by FUNCT_2:def 1;
reconsider r=p*s9|n as FinSequence of Seg(n+1) by FINSEQ_2:32;
A5: 0+n <= 1+n by XREAL_1:6;
then
A6: Seg n c= Seg(n+1) by FINSEQ_1:5;
s9|n = s9 | Seg n by FINSEQ_1:def 16;
then
A7: s9|n is one-to-one by A1,FUNCT_1:52;
A8: rng p = Seg(n+1) by FUNCT_2:def 3;
A9: dom s = Seg(n+1) by FUNCT_2:def 1;
then len s9 = n+1 by A1,FINSEQ_1:def 3;
then len(s9|n) = n by A5,FINSEQ_1:59;
then len r = n by FINSEQ_2:33;
then
A10: dom r = Seg n by FINSEQ_1:def 3;
A11: rng s = Seg(n+1) by FUNCT_2:def 3;
then q in Seg(n+1) by A2,A9,FINSEQ_1:4,FUNCT_1:3;
then
A12: q <= n+1 by FINSEQ_1:1;
aaa: rng r c= Seg(n+1) by RELAT_1:def 19;
for i being object holds i in rng r iff i in Seg n
proof
let i being object;
thus i in rng r implies i in Seg n
proof
assume
bbb: i in rng r;
then consider j being object such that
A13: j in Seg n and
A14: r.j = i by A10,FUNCT_1:def 3;
reconsider j as Element of NAT by A13;
A15: j <= n by A13,FINSEQ_1:1;
then
A16: (s9|n).j = s.j by A1,FINSEQ_3:112;
then
A17: i = p.(s.j) by A10,A13,A14,FUNCT_1:12;
s.j in dom p by A9,A11,A4,A6,A13,FUNCT_1:3;
then p.(s.j) in rng p by FUNCT_1:3;
then reconsider i as Element of NAT by A8,A10,A13,A14,A16,FUNCT_1:12;
A19: n+1 in dom s by A9,FINSEQ_1:4;
A20: s.j in Seg(n+1) by A9,A11,A6,A13,FUNCT_1:3;
then reconsider q1 = s.j as Element of NAT;
j < n+1 by A15,NAT_1:13;
then
A21: q1 <> q by A2,A9,A6,A13,A19,FUNCT_1:def 4;
per cases by A21,XXREAL_0:1;
suppose
q1 < q;
then i < q by A3,A17,A20;
then i < n+1 by A12,XXREAL_0:2;
then
A22: i <= n by NAT_1:13;
1 <= i by bbb,aaa,FINSEQ_1:1;
hence thesis by A22,FINSEQ_1:1;
end;
suppose
A23: q1 > q;
A24: q1 <= n+1 by A20,FINSEQ_1:1;
i = q1-1 by A3,A17,A20,A23;
then
A25: i <= n by A24,XREAL_1:20;
1 <= i by bbb,aaa,FINSEQ_1:1;
hence thesis by A25,FINSEQ_1:1;
end;
end;
assume
A26: i in Seg n;
then reconsider i as Element of NAT;
per cases;
suppose
A27: i < q;
then
A28: p.i = i by A3,A6,A26;
consider j being object such that
A29: j in dom s and
A30: i = s.j by A11,A6,A26,FUNCT_1:def 3;
j in Seg(n+1) by A29;
then reconsider j as Element of NAT;
j <= n+1 by A29,FINSEQ_1:1;
then j < n+1 by A2,A27,A30,XXREAL_0:1;
then
A31: j <= n by NAT_1:13;
1 <= j by A29,FINSEQ_1:1;
then
A32: j in dom r by A10,A31,FINSEQ_1:1;
(s9|n).j = s.j by A1,A31,FINSEQ_3:112;
then r.j = i by A28,A30,A32,FUNCT_1:12;
hence thesis by A32,FUNCT_1:3;
end;
suppose
A33: i >= q;
i <= n by A26,FINSEQ_1:1;
then
A34: i+1 <= n+1 by XREAL_1:6;
1 <= i+1 by NAT_1:12;
then
A35: i+1 in Seg(n+1) by A34,FINSEQ_1:1;
then consider j being object such that
A36: j in dom s and
A37: i+1 = s.j by A11,FUNCT_1:def 3;
j in Seg(n+1) by A36;
then reconsider j as Element of NAT;
A38: j <= n+1 by A36,FINSEQ_1:1;
j <> n+1 by A2,A33,A37,NAT_1:13;
then j < n+1 by A38,XXREAL_0:1;
then
A39: j <= n by NAT_1:13;
1 <= j by A36,FINSEQ_1:1;
then
A40: j in Seg n by A39,FINSEQ_1:1;
i+1 > q by A33,NAT_1:13;
then
A41: p.(i+1) = i+1-1 by A3,A35
.= i;
(s9|n).j = s.j by A1,A39,FINSEQ_3:112;
then r.j = p.(s.j) by A10,A40,FUNCT_1:12;
hence thesis by A10,A37,A41,A40,FUNCT_1:3;
end;
end;
then
A42: rng r = Seg n by TARSKI:2;
then p*s9|n is Function of Seg n, Seg n by A10,FUNCT_2:1;
hence thesis by A42,A7,FUNCT_2:57;
end;
Lm5: for n,q being Nat, p being Permutation of Seg(n+1), F,H being
FinSequence of ExtREAL st F=H*p & q in Seg(n+1) & len H = n+1 & not -infty in
rng H & for i being Element of NAT st i in Seg(n+1) holds (i<q implies p.i=i) &
(i=q implies p.i=n+1) & (i>q implies p.i=i-1) holds Sum F = Sum H
proof
let n,q be Nat, p be Permutation of Seg(n+1), F,H be FinSequence of ExtREAL;
assume that
A1: F=H*p and
A2: q in Seg(n+1) and
A3: len H = n+1 and
A4: not -infty in rng H and
A5: for i being Element of NAT st i in Seg(n+1) holds (i<q implies p.i=i
) & (i=q implies p.i=n+1) & (i>q implies p.i=i-1);
A6: 1 <= q by A2,FINSEQ_1:1;
then q-1 >= 1-1 by XREAL_1:9;
then
A7: q-'1 = q-1 by XREAL_0:def 2;
set H1 = H|n;
A8: H1 = (H1|(q-'1))^(H1/^(q-'1)) by RFINSEQ:8;
reconsider p9 = p as FinSequence of Seg(n+1) by FINSEQ_2:25;
dom p = Seg(n+1) by FUNCT_2:def 1;
then
A9: len p9 = n+1 by FINSEQ_1:def 3;
A10: q <= n+1 by A2,FINSEQ_1:1;
then
A11: q-'1 <= n+1-1 by A7,XREAL_1:9;
A12: dom H = Seg(n+1) by A3,FINSEQ_1:def 3;
then H is Function of Seg(n+1), ExtREAL by FINSEQ_2:26;
then
A13: len F = n+1 by A1,A9,FINSEQ_2:33;
then
A14: len(F/^q) = n+1-q by A10,RFINSEQ:def 1;
A15: n <= n+1 by NAT_1:11;
then
A16: len(F|(q-'1)) = q-'1 by A11,A13,FINSEQ_1:59,XXREAL_0:2;
A17: dom F = Seg(n+1) by A13,FINSEQ_1:def 3;
A18: for i being Nat st 1 <= i & i <= q-'1 holds (F|(q-'1)).i=(H1|(q-'1)).i
proof
let i be Nat;
assume that
A19: 1 <= i and
A20: i <= q-'1;
A21: (F|(q-'1)).i = F.i by A20,FINSEQ_3:112;
A22: H1.i = H.i by A11,A20,FINSEQ_3:112,XXREAL_0:2;
A23: (H1|(q-'1)).i = H1.i by A20,FINSEQ_3:112;
A24: i < q-'1+1 by A20,NAT_1:13;
i <= n by A11,A20,XXREAL_0:2;
then i <= n+1 by A15,XXREAL_0:2;
then
A25: i in Seg(n+1) by A19,FINSEQ_1:1;
then F.i = H.(p.i) by A1,A17,FUNCT_1:12;
hence thesis by A5,A7,A21,A23,A22,A25,A24;
end;
0+n <= 1+n by XREAL_1:6;
then
A26: len H1 = n by A3,FINSEQ_1:59;
then
A27: len(H1|(q-'1)) = q-'1 by A11,FINSEQ_1:59;
A28: len(H1/^(q-'1)) = n-(q-1) by A7,A11,A26,RFINSEQ:def 1;
for i being Nat st 1 <= i & i <= n+1-q holds (F/^q).i=(H1/^(q-'1)).i
proof
reconsider n1 = n+1-q as Element of NAT by A10,INT_1:5;
let i be Nat;
assume that
A29: 1 <= i and
A30: i <= n+1-q;
A31: i+q <= n+1 by A30,XREAL_1:19;
A32: i in Seg n1 by A29,A30,FINSEQ_1:1;
then i in dom(H1/^(q-'1)) by A28,FINSEQ_1:def 3;
then
A33: (H1/^(q-'1)).i = H1.(i+(q-'1)) by A11,A26,RFINSEQ:def 1;
i+(q-'1) = i+q-1 by A7;
then i+(q-'1) <= n by A31,XREAL_1:20;
then
A34: (H1/^(q-'1)).i = H.(i+q-1) by A7,A33,FINSEQ_3:112;
A35: 1 <= i+q by A29,NAT_1:12;
then i+q in dom F by A17,A31,FINSEQ_1:1;
then
A36: F.(i+q) = H.(p.(i+q)) by A1,FUNCT_1:12;
dom(F/^q) = Seg n1 by A14,FINSEQ_1:def 3;
then
A37: (F/^q).i = F.(i+q) by A10,A13,A32,RFINSEQ:def 1;
i+q >= 1+q by A29,XREAL_1:6;
then
A38: i+q>q by NAT_1:13;
i+q in Seg(n+1) by A31,A35,FINSEQ_1:1;
hence thesis by A5,A37,A34,A36,A38;
end;
then
A39: F/^q = H1/^(q-'1) by A14,A28,FINSEQ_1:14;
A40: F = (F|(q-'1))^<*F.q*>^(F/^q) by A6,A10,A13,FINSEQ_5:84;
then
A41: rng F = rng((F|(q-'1))^<*F.q*>) \/ rng(F/^q) by FINSEQ_1:31;
p.q = n+1 by A2,A5;
then
A42: F.q = H.(n+1) by A1,A2,A17,FUNCT_1:12;
A43: H1 = H | Seg n by FINSEQ_1:def 16;
then rng H1 c= rng H by RELAT_1:70;
then not -infty in rng H1 by A4;
then
A44: not -infty in rng(H1|(q-'1)) \/ rng(H1/^(q-'1)) by A8,FINSEQ_1:31;
then
A45: not -infty in rng(H1|(q-'1)) by XBOOLE_0:def 3;
A46: not -infty in rng F by A1,A4,FUNCT_1:14;
then
A47: not -infty in rng((F|(q-'1))^<*F.q*>) by A41,XBOOLE_0:def 3;
then
A48: not -infty in rng(F|(q-'1)) \/ rng<*F.q*> by FINSEQ_1:31;
then not -infty in rng(F|(q-'1)) by XBOOLE_0:def 3;
then
A49: Sum(F|(q-'1)) <> -infty by Lm2;
not -infty in rng<*F.q*> by A48,XBOOLE_0:def 3;
then not -infty in {F.q} by FINSEQ_1:39;
then
A50: -infty <> F.q by TARSKI:def 1;
A51: not -infty in rng(F/^q) by A46,A41,XBOOLE_0:def 3;
then
A52: Sum(F/^q) <> -infty by Lm2;
A53: H|(n+1) = H | Seg(n+1) by FINSEQ_1:def 16;
H|(n+1) = H by A3,FINSEQ_1:58;
then
A54: H = H1^<*H.(n+1)*> by A12,A43,A53,FINSEQ_1:4,FINSEQ_5:10;
A55: not -infty in rng(H1/^(q-'1)) by A44,XBOOLE_0:def 3;
thus Sum F = Sum((F|(q-'1))^<*F.q*>) + Sum(F/^q) by A40,A47,A51,Th8
.= Sum(F|(q-'1)) + F.q + Sum(F/^q) by Lm1
.= Sum(F|(q-'1)) + Sum(F/^q) + F.q by A50,A49,A52,XXREAL_3:29
.= Sum(H1|(q-'1)) + Sum(H1/^(q-'1)) + H.(n+1) by A16,A27,A18,A42,A39,
FINSEQ_1:14
.= Sum H1 + H.(n+1) by A8,A45,A55,Th8
.= Sum H by A54,Lm1;
end;
theorem
for F,G being FinSequence of ExtREAL, s being Permutation of dom F
st G = F*s & not -infty in rng F holds Sum(F) = Sum(G)
proof
let F,G be FinSequence of ExtREAL, s be Permutation of dom F;
defpred P[Nat] means
for F,G being FinSequence of ExtREAL, s being Permutation of Seg $1
st len F = $1 & G = F*s & not -infty in rng F
holds Sum F = Sum G;
A1: P[0]
proof
let F,G be FinSequence of ExtREAL, s be Permutation of Seg 0;
assume that
A2: len F = 0 and
A3: G = F*s;
F = <*> ExtREAL by A2;
hence thesis by A3;
end;
A4: for n being non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A5: P[n];
thus P[n+1]
proof
let F,G be FinSequence of ExtREAL, s be Permutation of Seg(n+1);
assume that
A6: len F = n+1 and
A7: G = F*s and
A8: not -infty in rng F;
reconsider s9=s as FinSequence of Seg(n+1) by FINSEQ_2:25;
A9: rng s = Seg(n+1) by FUNCT_2:def 3;
A10: dom s = Seg(n+1) by FUNCT_2:def 1;
then n+1 in dom s by FINSEQ_1:4;
then
A11: s.(n+1) in Seg(n+1) by A9,FUNCT_1:def 3;
then reconsider q=s.(n+1) as Element of NAT;
consider p being Permutation of Seg(n+1) such that
A12: for i being Element of NAT st i in Seg(n+1) holds (i<q implies
p.i=i) & (i=q implies p.i=n+1) & (i>q implies p.i=i-1) by A11,Lm3;
reconsider p2 = p" as FinSequence of Seg(n+1) by FINSEQ_2:25;
A13: dom p = Seg(n+1) by FUNCT_2:def 1;
p.q = n+1 by A11,A12;
then
A14: F.(s.(n+1)) = F.(p2.(n+1)) by A11,A13,FUNCT_1:34;
A15: 0+n <= 1+n by XREAL_1:6;
then
A16: Seg n c= Seg(n+1) by FINSEQ_1:5;
A17: dom F = Seg(n+1) by A6,FINSEQ_1:def 3;
then
A18: F is Function of Seg(n+1), ExtREAL by FINSEQ_2:26;
then reconsider H = F*p2 as FinSequence of ExtREAL by FINSEQ_2:32;
A19: H*p = F*(p2*p) by RELAT_1:36
.= F*(id Seg(n+1)) by A13,FUNCT_1:39
.= F by A17,RELAT_1:52;
len s9 = n+1 by A10,FINSEQ_1:def 3;
then
A20: len G = n+1 by A7,A18,FINSEQ_2:33;
then
A21: dom G = Seg(n+1) by FINSEQ_1:def 3;
then
A22: G.(n+1) = F.(s.(n+1)) by A7,FINSEQ_1:4,FUNCT_1:12;
reconsider p1 = p*s9|n as Permutation of Seg n by A12,Lm4;
A23: dom p1 = Seg n by FUNCT_2:def 1;
reconsider p19 = p1 as FinSequence of Seg n by FINSEQ_2:25;
A24: not -infty in rng H by A8,FUNCT_1:14;
bbb: dom p2 = rng p by FUNCT_1:33;
then dom p2 = Seg(n+1) by FUNCT_2:def 3;
then len p2 = n+1 by FINSEQ_1:def 3;
then
A25: len H = n+1 by A18,FINSEQ_2:33;
then
A26: dom H = Seg(n+1) by FINSEQ_1:def 3;
A27: len(H|n) = n by A25,A15,FINSEQ_1:59;
A28: G|n = (H|n)*p1
proof
dom(H|n) = Seg n by A27,FINSEQ_1:def 3;
then
A29: H|n is Function of Seg n, ExtREAL by FINSEQ_2:26;
then reconsider H1 = (H|n)*p19 as FinSequence of ExtREAL
by FINSEQ_2:32;
n in NAT by ORDINAL1:def 12;
then len p19 = n by A23,FINSEQ_1:def 3;
then
A30: len H1 = n by A29,FINSEQ_2:33;
A31: for i being Nat st 1 <= i & i <= n holds (G|n).i=((H|n)*p1).i
proof
let i be Nat;
assume that
A32: 1 <= i and
A33: i <= n;
A34: i in Seg n by A32,A33,FINSEQ_1:1;
then
A35: s.i in rng s by A10,A16,FUNCT_1:3;
i in dom H1 by A30,A34,FINSEQ_1:def 3;
then
A36: ((H|n)*p1).i = (H|n).(p1.i) by FUNCT_1:12;
rng p1 = Seg n by FUNCT_2:def 3;
then
A37: p1.i in Seg n by A23,A34,FUNCT_1:3;
then reconsider a = p1.i as Element of NAT;
a <= n by A37,FINSEQ_1:1;
then
A38: ((H|n)*p1).i = H.(p1.i) by A36,FINSEQ_3:112;
(s9|n).i = s.i by A33,FINSEQ_3:112;
then
A39: p1.i = p.(s.i) by A23,A34,FUNCT_1:12;
A40: (G|n).i = G.i by A33,FINSEQ_3:112;
z01: p.(s.i) in rng p by A9,A13,A35,FUNCT_1:def 3;
s.i = (p").(p.(s.i)) by A9,A13,A35,FUNCT_1:34;
then F.(s.i) = (F*p2).(p.(s.i)) by z01,bbb,FUNCT_1:13;
hence thesis by A7,A21,A16,A38,A39,A40,A34,FUNCT_1:12;
end;
len(G|n) = n by A20,A15,FINSEQ_1:59;
hence thesis by A30,A31,FINSEQ_1:14;
end;
G|n = G | Seg n by FINSEQ_1:def 16;
then G = (G|n)^<*G.(n+1)*> by A20,FINSEQ_3:55;
then
A41: Sum G = Sum(G|n)+G.(n+1) by Lm1;
A42: H|n = H | Seg n by FINSEQ_1:def 16;
then H = (H|n)^<*H.(n+1)*> by A25,FINSEQ_3:55;
then
A43: Sum H = Sum(H|n)+H.(n+1) by Lm1;
rng(H|n) c= rng H by A42,RELAT_1:70;
then not -infty in rng (H|n) by A8,FUNCT_1:14;
then
A44: Sum(G|n) = Sum(H|n) by A5,A27,A28;
H.(n+1) = F.(p2.(n+1)) by A26,FINSEQ_1:4,FUNCT_1:12;
hence thesis by A11,A12,A25,A44,A14,A22,A41,A43,A24,A19,Lm5;
end;
end;
A45: P[1]
proof
let F,G be FinSequence of ExtREAL, s be Permutation of Seg 1;
assume that
A46: len F = 1 and
A47: G = F*s;
reconsider s1 = s as FinSequence of Seg 1 by FINSEQ_2:25;
dom s = Seg 1 by FUNCT_2:def 1;
then
A48: len s1 = 1 by FINSEQ_1:def 3;
dom F = Seg 1 by A46,FINSEQ_1:def 3;
then F is Function of Seg 1, ExtREAL by FINSEQ_2:26;
then len G = 1 by A47,A48,FINSEQ_2:33;
then
A49: G = <*G.1*> by FINSEQ_1:40;
then rng G = {G.1} by FINSEQ_1:39;
then G.1 in rng G by TARSKI:def 1;
then
A50: G.1 in rng F by A47,FUNCT_1:14;
A51: F = <*F.1*> by A46,FINSEQ_1:40;
then rng F = {F.1} by FINSEQ_1:39;
hence thesis by A51,A49,A50,TARSKI:def 1;
end;
A52: for n being non zero Nat holds P[n] from NAT_1:sch 10(A45,A4);
A53: len F = 0 or len F <> 0;
dom F = Seg(len F) by FINSEQ_1:def 3;
hence thesis by A1,A52,A53;
end;
reserve x,y,w,z for ExtReal,
a for Real;
begin :: Basic properties of absolute value for extended real numbers
theorem Th1:
x = a implies |.x.| = |.a qua Complex.|
proof
assume
A1: x = a;
reconsider x as R_eal by XXREAL_0:def 1;
per cases;
suppose
0 <= x;
then |.x.| = a by A1,Def1;
hence thesis by ABSVALUE:def 1;
end;
suppose
A2: not 0 <= x;
then |.x.| = -x by Def1
.= -a by A1,SUPINF_2:2;
hence thesis by A1,A2,ABSVALUE:def 1;
end;
end;
theorem
|.x.| = x or |.x.| = -x by Def1;
theorem
0 <= |.x.|
proof
reconsider x as R_eal by XXREAL_0:def 1;
0 <= |.x.|;
hence thesis;
end;
theorem Th4:
x <> 0 implies 0 < |.x.|
proof
assume
A1: x <> 0;
per cases;
suppose
0 <= x;
hence thesis by A1,Def1;
end;
suppose
A2: not 0 <= x;
then 0 < -x;
hence thesis by A2,Def1;
end;
end;
theorem
x = 0 iff |.x.| = 0 by Th4,Def1;
theorem
|.x.| = -x & x <> 0 implies x < 0
proof
reconsider x as R_eal by XXREAL_0:def 1;
0 <= |.x.|;
hence thesis;
end;
theorem Th7:
x <= 0 implies |.x.| = -x
proof
assume
A1: x <= 0;
per cases by A1;
suppose
x < 0;
hence thesis by Def1;
end;
suppose
A2: x = 0;
then -0 = -x;
hence thesis by A2,Def1;
end;
end;
theorem
|.x * y.| = |.x.| * |.y.|
proof
reconsider x,y as R_eal by XXREAL_0:def 1;
per cases;
suppose
x = 0;
then |.x.| = 0 & |.x * y.| = 0 by Def1;
hence thesis;
end;
suppose
A1: 0 < x;
per cases;
suppose
y = 0;
then |.y.| = 0 & |.x * y.| = 0 by Def1;
hence thesis;
end;
suppose
0 < y;
then
A2: |.y.| = y by Def1;
|.x.| = x by A1,Def1;
hence thesis by A2,Def1;
end;
suppose
A3: y < 0;
then
A4: |.y.| = -y by Def1;
|.x.| = x by A1,Def1;
then |.x.| * |.y.| = -(x * y) by A4,XXREAL_3:92;
hence thesis by A1,A3,Def1;
end;
end;
suppose
A5: x < 0;
per cases;
suppose
y = 0;
then |.y.| = 0 & |.x * y.| = 0 by Def1;
hence thesis;
end;
suppose
A6: 0 < y;
then |.y.| = y by Def1;
then
A7: |.x.| * |.y.| = (-x) * y by A5,Def1;
|.x * y.| = -(x * y) by A5,A6,Def1;
hence thesis by A7,XXREAL_3:92;
end;
suppose
y < 0;
then |.y.| = -y by Def1;
then |.x.| * |.y.| = (-x) * (-y) by A5,Def1;
then |.x.| * |.y.| = -(x * (-y)) by XXREAL_3:92
.= -(-(x * y)) by XXREAL_3:92;
hence thesis by Def1;
end;
end;
end;
theorem Th9:
-|.x.| <= x & x <= |.x.|
proof
reconsider x as R_eal by XXREAL_0:def 1;
per cases;
suppose
A1: 0 <= x;
thus thesis by A1,Def1;
end;
suppose
not 0 <= x;
then |.x.|=-x by Def1;
hence thesis;
end;
end;
theorem Th10:
|.x.| < y implies -y < x & x < y
proof
assume
A1: |.x.| < y;
reconsider x,y as R_eal by XXREAL_0:def 1;
A2: |.x.| < y by A1;
per cases;
suppose 0 <= x;
hence thesis by A2,Def1;
end;
suppose
A3: not 0 <= x;
then |.x.|=-x by Def1;
hence thesis by A1,A3,XXREAL_3:60;
end;
end;
theorem Th11:
-y < x & x < y implies 0 < y & |.x.| < y
proof
assume that
A1: -y < x and
A2: x < y;
per cases;
suppose
0 <= x;
hence thesis by A2,Def1;
end;
suppose
A3: not 0 <= x;
-x < y by A1,XXREAL_3:60;
hence thesis by A3,Def1;
end;
end;
theorem Th12:
-y <= x & x <= y iff |.x.| <= y
proof
A1: -y <= x & x <= y implies |.x.| <= y
proof
assume that
A2: -y <= x and
A3: x <= y;
per cases;
suppose
0 <= x;
hence thesis by A3,Def1;
end;
suppose
A4: not 0 <= x;
-x <= y by A2,XXREAL_3:60;
hence thesis by A4,Def1;
end;
end;
|.x.| <= y implies -y <= x & x <= y
proof
assume
A5: |.x.| <= y;
per cases by A5,XXREAL_0:1;
suppose
|.x.| = y;
hence thesis by Th9;
end;
suppose
|.x.| < y;
hence thesis by Th10;
end;
end;
hence thesis by A1;
end;
theorem Th13:
|.x + y.| <= |.x.| + |.y.|
proof
A1: -|.x.| <= x & -|.y.| <= y by Th9;
A2: x <= |.x.| & y <= |.y.| by Th9;
A3: -|.x.|-|.y.| = -(|.x.|+|.y.|) by XXREAL_3:25;
x + y <= |.x.| + |.y.| & -|.x.|+(-|.y.|) <= x + y by A1,A2,XXREAL_3:36;
hence thesis by A3,Th12;
end;
theorem Th14:
-infty < x & x < +infty & x <> 0 implies |.x.|*|. 1. / x .| = 1.
proof
assume that
A1: -infty < x & x < +infty and
A2: x <> 0;
reconsider a = x as Element of REAL by A1,XXREAL_0:14;
A3: 1./x = 1/a by Th2;
per cases;
suppose 0 <= x;
then |.x.| = a & |. 1./x .| = 1/a by A3,Def1;
then |.x.|*|. 1./x .| = a * (1/a) by XXREAL_3:def 5;
hence thesis by A2,XCMPLX_1:106;
end;
suppose
A4: not 0 <= x;
then
A5: |.x.| = -x by Def1
.= -a by SUPINF_2:2;
1./x < 0 by A3,A4;
then |. 1./x .| = -(1./x) by Def1
.= -(1/a) by A3,SUPINF_2:2;
then |.x.|*|. 1./x .| = (-a) * (-(1/a)) by A5,XXREAL_3:def 5
.= a * (1/a);
hence thesis by A4,XCMPLX_1:106;
end;
end;
theorem
x = +infty or x = -infty implies |.x.|*|. 1./x .| = 0
proof
assume x = +infty or x = -infty;
then |. 1./x .| = 0 by Def1;
hence thesis;
end;
theorem
x <> 0 implies |. 1./x .| = 1./|.x.|
proof
assume
A1: x <> 0;
per cases;
suppose
A2: x = +infty;
then |. 1./x .| = 0 by Def1;
hence thesis by A2,Def1;
end;
suppose
x = -infty;
then |. 1./x .| = 0 & |.x.| = +infty by Def1,XXREAL_3:5;
hence thesis;
end;
suppose
A3: x <> +infty & x <> -infty;
A4: 0 < |.x.| by A1,Th4;
A5: x < +infty by A3,XXREAL_0:4;
-infty <= x by XXREAL_0:5;
then
A6: -infty < x by A3,XXREAL_0:1;
then -(+infty) < x by XXREAL_3:def 3;
then
A7: |.x.| < +infty by A5,Th11;
|. 1./x .|*|.x.| = 1. by A1,A6,A5,Th14;
hence thesis by A4,A7,XXREAL_3:88;
end;
end;
theorem
not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y<>0 implies |.
x/y.| = |.x.|/|.y.|
proof
assume that
A1: not((x=-infty or x=+infty) & (y=-infty or y=+infty)) and
A2: y<>0;
reconsider y as R_eal by XXREAL_0:def 1;
per cases;
suppose
A3: x = +infty;
A4: -infty < y by A1,A3,XXREAL_0:12,14;
per cases by A2;
suppose
A5: 0 < y;
then x / y = +infty by A3,A1,XXREAL_3:83;
then
A6: |.x/y.| = +infty by Def1;
|.y.| = y by A5,Def1;
hence thesis by A3,A1,A5,A6,XXREAL_3:83;
end;
suppose
A7: y < 0;
then |.y.| = -y by Def1;
then
A8: |.y.| < +infty by A4,XXREAL_3:5,38;
x / y = -infty by A3,A1,A7,XXREAL_3:85;
then |.x/y.| = +infty by Def1,XXREAL_3:5;
hence thesis by A8,A2,A3,Th4,XXREAL_3:83;
end;
end;
suppose
A9: x = -infty;
A10: -infty < y by A1,A9,XXREAL_0:12,14;
per cases by A2;
suppose
A11: 0 < y;
then
A12: x / y = -infty by A9,A1,XXREAL_3:86;
A13: |.x.| = +infty by A9,Def1,XXREAL_3:5;
|.y.| = y by A11,Def1;
hence thesis by A9,A1,A11,A12,A13,XXREAL_3:83;
end;
suppose
A14: y < 0;
then |.y.| = -y by Def1;
then
A15: |.y.| < +infty by A10,XXREAL_3:5,38;
A16: x / y = +infty by A9,A1,A14,XXREAL_3:84;
0 < |.y.| & |.x.| = +infty by A2,A9,Th4,Def1,XXREAL_3:5;
hence thesis by A15,A16,XXREAL_3:83;
end;
end;
suppose
x <> +infty & x <> -infty;
then reconsider a = x as Element of REAL by XXREAL_0:14;
per cases;
suppose
y = +infty;
then |.x/y.| = 0 & |.y.| = +infty by Def1;
hence thesis;
end;
suppose
y = -infty;
then |.x/y.| = 0 & |.y.| = +infty by Def1,XXREAL_3:5;
hence thesis;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Element of REAL by XXREAL_0:14;
|.x.| = |.a qua Complex.| & |.y.| = |.b qua Complex.| by Th1;
then
A17: |.x.|/|.y.| = |.a qua Complex.|/|.b qua Complex.| by Th2;
x/y = a/b by Th2;
then |.x/y.| = |.a/b qua Complex.| by Th1;
hence thesis by A17,COMPLEX1:67;
end;
end;
end;
theorem Th18:
|.x.| = |.-x.|
proof
reconsider x as R_eal by XXREAL_0:def 1;
per cases;
suppose 0 < x;
then |.-x.| = -(-x) by Def1
.= x;
hence thesis;
end;
suppose x < 0;
then |.x.| = -x by Def1;
hence thesis;
end;
suppose x = 0;
hence thesis;
end;
end;
theorem Th19:
|.+infty.| = +infty & |.-infty.| = +infty
proof
thus |.+infty.| = +infty by Def1;
--infty = +infty by XXREAL_3:23;
hence thesis by Def1;
end;
theorem Th20:
x is Real or y is Real implies |.x.|-|.y.| <= |.x-y.|
proof
assume
A1: x is Real or y is Real;
reconsider x,y as R_eal by XXREAL_0:def 1;
per cases by A1;
suppose y is Real;
then (x - y) + y = x by XXREAL_3:22;
then |.x.| <= |.x-y.| + |.y.| by Th13;
hence thesis by XXREAL_3:42;
end;
suppose
x is Real;
then reconsider a = x as Real;
A2: |.x.| = |.a.|;
per cases;
suppose
A3: y = +infty or y = -infty;
|.y.| = +infty by Th19,A3;
then |.x.| - |.y.| = -infty by A2,XXREAL_3:13;
then |.x.|-|.y.| <= |.x-y.|;
hence thesis;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Element of REAL by XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then
A4: |.x-y.| = |.a-b qua Complex.| by Th1;
|.y.| = |.b qua Complex.| by Th1;
then |.x.|-|.y.| = |.a qua Complex.|-|.b qua Complex.|
by A2,SUPINF_2:3;
hence thesis by A4,COMPLEX1:59;
end;
end;
end;
theorem
|.x-y.| <= |.x.| + |.y.|
proof
reconsider x,y as R_eal by XXREAL_0:def 1;
per cases;
suppose x = +infty or x = -infty;
then |.x.| + |.y.| = +infty by Th19,XXREAL_3:def 2;
hence thesis by XXREAL_0:3;
end;
suppose
A1: x <> +infty & x <> -infty;
then reconsider a = x as Element of REAL by XXREAL_0:14;
per cases;
suppose
A2: y = +infty;
x - y = -infty by A1,A2,XXREAL_3:13;
hence thesis by A2,Th19,XXREAL_3:def 2;
end;
suppose
A3: y = -infty;
x - y = +infty by A1,A3,XXREAL_3:14;
hence thesis by A3,Th19,XXREAL_3:def 2;
end;
suppose
y <> +infty & y <> -infty;
then reconsider b = y as Element of REAL by XXREAL_0:14;
|.x.|=|.a qua Complex.| & |.y.|=|.b qua Complex.| by Th1;
then
A4: |.x.|+|.y.|=|.a qua Complex.|+|.b qua Complex.| by SUPINF_2:1;
x - y = a - b by SUPINF_2:3;
then |.x-y.| = |.a-b qua Complex.| by Th1;
hence thesis by A4,COMPLEX1:57;
end;
end;
end;
::$CT
theorem
|.x.| <= z & |.y.| <= w implies |.x+y.| <= z + w
proof
assume
A1: |.x.| <= z & |.y.| <= w;
then -z <= x & -w <= y by Th12;
then
A2: -z + -w <= x + y by XXREAL_3:36;
x <= z & y <= w by A1,Th12;
then
A3: x + y <= z + w by XXREAL_3:36;
-z -w = -(z + w) by XXREAL_3:25;
hence thesis by A3,A2,Th12;
end;
theorem
x is Real or y is Real implies |.|.x.|-|.y.|.| <= |.x-y.|
proof
A1: |.y.|-|.x.| = -(|.x.|-|.y.|) by XXREAL_3:26;
assume
A2: x is Real or y is Real;
then
A3: |.x.|-|.y.| <= |.x-y.| by Th20;
y - x = -(x - y) by XXREAL_3:26;
then
A4: |.y-x.| = |.x-y.| by Th18;
|.y.|-|.x.| <= |.y-x.| by A2,Th20;
then -|.x-y.| <= -(-(|.x.|-|.y.|)) by A4,A1,XXREAL_3:38;
hence thesis by A3,Th12;
end;
theorem
0 <= x * y implies |.x+y.| = |.x.|+|.y.|
proof
assume
A1: 0 <= x * y;
per cases by A1;
suppose (0 <= x or 0 < x) & (0 <= y or 0 < y);
then |.x.| = x & |.y.| = y by Def1;
hence thesis by Def1;
end;
suppose
A2: (x <= 0 or x < 0) & (y <= 0 or y < 0);
then
A3: |.x+y.| = -(x + y) by Th7
.= -x -y by XXREAL_3:25;
|.x.| = -x by A2,Th7;
hence thesis by A2,A3,Th7;
end;
end;
begin
theorem
x <> +infty & y <> +infty & not ( x = +infty & y = +infty or x =
-infty & y = -infty ) implies min(x,y) = (x + y - |.x - y.|) / 2
proof
assume that
A1: x <> +infty and
A2: y <> +infty and
A3: not ( x = +infty & y = +infty or x = -infty & y = -infty );
per cases;
suppose
A4: x = -infty;
then x + y = -infty & x - y = -infty by A2,A3,XXREAL_3:14,def 2;
then
A5: x + y - |.x - y.| = -infty by XXREAL_3:14;
A6: min(x,y) = -infty by A4,XXREAL_0:44;
thus thesis by A6,A5,XXREAL_3:86;
end;
suppose
x <> -infty;
then reconsider a = x as Element of REAL by A1,XXREAL_0:14;
per cases;
suppose
A7: y = -infty;
then x + y = -infty & x - y = +infty by A1,A3,XXREAL_3:14,def 2;
then
A8: x + y - |.x - y.| = -infty by XXREAL_3:14;
A9: min(x,y) = -infty by A7,XXREAL_0:44;
thus thesis by A9,A8,XXREAL_3:86;
end;
suppose
y <> -infty;
then reconsider b = y as Element of REAL by A2,XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then x + y = a + b & |.x - y.| = |.a-b.| by SUPINF_2:1;
then
A10: x + y - |.x - y.| = a + b - |.a-b qua Complex.| by SUPINF_2:3;
(x + y - |.x - y.|) / 2 = (a+b-|.a-b qua Complex.|)/2 by A10,Th2;
hence thesis by COMPLEX1:73;
end;
end;
end;
theorem
x <> -infty & y <> -infty & not ( x = +infty & y = +infty or x =
-infty & y = -infty ) implies max(x,y) = (x + y + |.x - y.|) / 2
proof
assume that
A1: x <> -infty and
A2: y <> -infty and
A3: not ( x = +infty & y = +infty or x = -infty & y = -infty );
per cases;
suppose
A4: x = +infty;
then x + y = +infty & x - y = +infty by A2,A3,XXREAL_3:13,def 2;
then
A5: x + y + |.x - y.| = +infty by XXREAL_3:def 2;
A6: max(x,y) = +infty by A4,XXREAL_0:41;
thus thesis by A6,A5,XXREAL_3:83;
end;
suppose
x <> +infty;
then reconsider a = x as Element of REAL by A1,XXREAL_0:14;
per cases;
suppose
A7: y = +infty;
then x + y = +infty & x - y = -infty by A1,A3,XXREAL_3:13,def 2;
then
A8: x + y + |.x - y.| = +infty by XXREAL_3:def 2;
A9: max(x,y) = +infty by A7,XXREAL_0:41;
thus thesis by A9,A8,XXREAL_3:83;
end;
suppose
y <> +infty;
then reconsider b = y as Element of REAL by A2,XXREAL_0:14;
x - y = a - b by SUPINF_2:3;
then x + y = a + b & |.x - y.| = |.a-b.| by SUPINF_2:1;
then
A10: x + y + |.x - y.| = a + b + |.a-b qua Complex.| by SUPINF_2:1;
(x + y + |.x - y.|) / 2 = (a+b+|.a-b qua Complex.|)/2 by A10,Th2;
hence thesis by COMPLEX1:74;
end;
end;
end;
definition
let x,y be R_eal;
redefine func max(x,y) -> R_eal; :: redefines max (XXREAL_0, definition)
coherence by XXREAL_0:def 1;
redefine func min(x,y) -> R_eal; :: redefines min (XXREAL_0, definition)
coherence by XXREAL_0:def 1;
end;
theorem
min(x,y) + max(x,y)= x + y
proof
per cases;
suppose
A1: x <= y;
then min(x,y) = x by XXREAL_0:def 9;
hence thesis by A1,XXREAL_0:def 10;
end;
suppose
A2: not x <= y;
then min(x,y) = y by XXREAL_0:def 9;
hence thesis by A2,XXREAL_0:def 10;
end;
end;
begin ::Addenda
:: missing, 2007.07.20, A.T.
theorem Th28:
|.x.| = +infty implies x = +infty or x = -infty
proof
A1: |.x.| = x or -|.x.| = --x by Def1;
assume |.x.| = +infty;
hence thesis by A1,XXREAL_3:5;
end;
theorem
|.x.| < +infty iff x in REAL by Th19,Th28,XXREAL_0:4,14;