:: Some Special Matrices of Real Elements and Their Properties
:: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue
::
:: Received October 19, 2006
:: Copyright (c) 2006-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, NAT_1, MATRIX_1, RELAT_1, XXREAL_0, CARD_1,
ARYTM_3, LATTICE3, FUNCT_4, FINSEQ_1, TREES_1, COMPLEX1, ARYTM_1,
FUNCOP_1, QC_LANG1, VECTSP_1, REAL_1, MATRIXR1, ZFMISC_1, MATRIX10,
FUNCT_7;
notations COMPLEX1, TARSKI, ZFMISC_1, SUBSET_1, FINSEQ_1, MATRIX_0, ORDINAL1,
FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, MATRIXR1,
RLVECT_1, VECTSP_1, STRUCT_0, MATRIX_3, GROUP_1, MATRIX_1;
constructors XXREAL_0, REAL_1, BINOP_2, MEMBERED, COMPLEX1, MATRIX_3,
MATRIXR1, RELSET_1, FUNCT_7, NUMBERS;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VECTSP_1, ORDINAL1;
requirements NUMERALS, SUBSET, ARITHM, REAL;
equalities MATRIX_0, MATRIXR1;
theorems MATRIX_0, MATRIX_3, MATRIXR1, XREAL_1, ABSVALUE, VECTSP_1, MATRIX_4,
FINSEQ_1, FINSEQ_3, COMPLEX1, MATRIXC1, XXREAL_0, XREAL_0, MATRIX_1;
schemes MATRIX_0;
begin
reserve a,b for Real,
i,j,n for Nat,
M,M1,M2,M3,M4 for Matrix of n, REAL;
definition
let M be Matrix of REAL;
attr M is Positive means
:Def1:
for i,j st [i,j] in Indices M holds M*(i,j) > 0;
attr M is Negative means
:Def2:
for i,j st [i,j] in Indices M holds M*(i,j) < 0;
attr M is Nonpositive means
:Def3:
for i,j st [i,j] in Indices M holds M*(i, j) <= 0;
attr M is Nonnegative means
:Def4:
for i,j st [i,j] in Indices M holds M*(i, j) >= 0;
end;
definition
let M1,M2 be Matrix of REAL;
pred M1 is_less_than M2 means
for i,j st [i,j] in Indices M1 holds M1 *(i,j) < M2*(i,j);
pred M1 is_less_or_equal_with M2 means
for i,j st [i,j] in Indices M1 holds M1*(i,j) <= M2*(i,j);
end;
definition
let M be Matrix of REAL;
func |:M:| -> Matrix of REAL means
:Def7:
len it = len M & width it = width
M & for i,j holds [i,j] in Indices M implies it*(i,j) = |.M*(i,j).|;
existence
proof
deffunc F(Nat,Nat) = In(|.M*($1,$2).|,REAL);
consider M1 being Matrix of len M,width M,REAL such that
A1: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j) from
MATRIX_0:sch 1;
take M1;
A2: len M1=len M by MATRIX_0:def 2;
A3: now
per cases;
case
A4: len M= 0;
then width M1=0 by A2,MATRIX_0:def 3;
hence width M1=width M by A4,MATRIX_0:def 3;
end;
case
len M>0;
hence width M1=width M by MATRIX_0:23;
end;
end;
thus len M1 = len M & width M1 = width M by A3,A2;
let i,j;
assume
A5: [i,j] in Indices M;
dom M = dom M1 by A2,FINSEQ_3:29;
hence M1*(i,j) = In(|.M*(i,j).|,REAL) by A1,A3,A5
.= |.M*(i,j).|;
end;
uniqueness
proof
let M1,M2 be Matrix of REAL;
assume that
A6: len M1=len M and
A7: width M1 =width M and
A8: for i,j st [i,j] in Indices M holds M1*(i,j)=|.M*(i,j).| and
A9: len M2=len M & width M2 =width M and
A10: for i,j st [i,j] in Indices M holds M2*(i,j)=|.M*(i,j).|;
now
let i,j;
assume
A11: [i,j] in Indices M1;
A12: dom M1 = dom M by A6,FINSEQ_3:29;
hence M1*(i,j)=|.M*(i,j).| by A7,A8,A11
.=M2*(i,j) by A7,A10,A11,A12;
end;
hence thesis by A6,A7,A9,MATRIX_0:21;
end;
end;
definition
let n;
let M;
redefine func -M -> Matrix of n,REAL; :: redefines - (MATRIXR1, definition)
coherence
proof
len M=n by MATRIX_0:24;
then
A1: len (-M)=n by MATRIX_1:def 4;
width M=n by MATRIX_0:24;
then width (-M)=n by MATRIX_1:def 4;
hence thesis by A1,MATRIX_0:51;
end;
end;
definition
let n;
let M;
redefine func |:M:| -> Matrix of n,REAL; :: redefines |: (MATRIX10, definition)
coherence
proof
len M=n by MATRIX_0:24;
then
A1: len |:M:|=n by Def7;
width M=n by MATRIX_0:24;
then width |:M:|=n by Def7;
hence thesis by A1,MATRIX_0:51;
end;
end;
definition
let n;
let M1,M2;
redefine func M1+M2 -> Matrix of n,REAL; :: redefines + (MATRIXR1, definition)
coherence
proof
A1: width M2=n by MATRIX_0:24;
width M1=n by MATRIX_0:24;
then len (M1+M2)=len M1 & width (M1+M2)=width M2 by A1,MATRIX_1:def 6;
hence thesis by A1,MATRIX_0:24,51;
end;
end;
definition
let n;
let M1,M2;
redefine func M1-M2 -> Matrix of n,REAL; :: redefines - (MATRIXR1, definition)
coherence
proof
len (M1+ -M2)=len M1 by MATRIX_1:def 6;
hence thesis by MATRIX_1:def 7;
end;
end;
definition
let n;
let a be Real;
let M;
redefine func a*M -> Matrix of n,REAL; :: redefines * (MATRIXR1, definition)
coherence
proof
A1: width (a*M)=width M by MATRIXR1:27;
width M=n & len (a*M)=len M by MATRIXR1:27,MATRIX_0:24;
hence thesis by A1,MATRIX_0:24,51;
end;
end;
Lm1: 1 in REAL by XREAL_0:def 1;
Lm2: -1 in REAL by XREAL_0:def 1;
registration
let n;
cluster (n,n) --> 1 -> Positive for Matrix of n,REAL;
coherence
by Lm1,MATRIX_0:46;
cluster ((n,n) --> -1) -> Negative for Matrix of n,REAL;
coherence
proof let M be Matrix of n,REAL such that
A1: M = (n,n) --> -1;
let i,j;
assume [i,j] in Indices M;
then M*(i,j) = -1 by A1,Lm2,MATRIX_0:46;
hence thesis;
end;
cluster ((n,n) --> -1) -> Nonpositive for Matrix of n,REAL;
coherence
by Lm2,MATRIX_0:46;
cluster ((n,n) --> 1) -> Nonnegative for Matrix of n,REAL;
coherence
by Lm1,MATRIX_0:46;
end;
registration
let n;
cluster Positive Nonnegative for Matrix of n,REAL;
existence
proof
take (n,n) --> In(1,REAL);
thus thesis;
end;
cluster Negative Nonpositive for Matrix of n,REAL;
existence
proof
take (n,n) --> -In(1,REAL);
thus thesis;
end;
end;
registration
cluster Positive Nonnegative for Matrix of REAL;
existence
proof
take (1,1) --> In(1,REAL);
thus thesis;
end;
cluster Negative Nonpositive for Matrix of REAL;
existence
proof
take (1,1) --> -In(1,REAL);
thus thesis;
end;
end;
registration
let M be Positive Matrix of REAL;
cluster M@ -> Positive;
coherence
proof
for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) > 0
proof
let i,j;
assume [i,j] in Indices (M@);
then
A1: [j,i] in Indices M by MATRIX_0:def 6;
then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
hence thesis by A1,Def1;
end;
hence thesis;
end;
end;
registration
let M be Negative Matrix of REAL;
cluster M@ -> Negative;
coherence
proof
for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) < 0
proof
let i,j;
assume [i,j] in Indices (M@);
then
A1: [j,i] in Indices M by MATRIX_0:def 6;
then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
hence thesis by A1,Def2;
end;
hence thesis;
end;
end;
registration
let M be Nonpositive Matrix of REAL;
cluster M@ -> Nonpositive;
coherence
proof
for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) <= 0
proof
let i,j;
assume [i,j] in Indices (M@);
then
A1: [j,i] in Indices M by MATRIX_0:def 6;
then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
hence thesis by A1,Def3;
end;
hence thesis;
end;
end;
registration
let M be Nonnegative Matrix of REAL;
cluster M@ -> Nonnegative;
coherence
proof
for i,j st [i,j] in Indices (M@) holds (M@)*(i,j) >= 0
proof
let i,j;
assume [i,j] in Indices (M@);
then
A1: [j,i] in Indices M by MATRIX_0:def 6;
then (M@)*(i,j) = M*(j,i) by MATRIX_0:def 6;
hence thesis by A1,Def4;
end;
hence thesis;
end;
end;
Lm3: len M1=len M2 & width M1=width M2
proof
width M1=n & len M1=n by MATRIX_0:24;
hence thesis by MATRIX_0:24;
end;
theorem
for x1 be Element of F_Real for x2 be Real st x1 = x2 holds -x1=-x2;
theorem Th2:
for M being Matrix of REAL st [i,j] in Indices M holds (-M)*(i,j) =-(M*(i,j))
proof
let M be Matrix of REAL;
assume [i,j] in Indices M;
then (-M)*(i,j)= -((MXR2MXF M)*(i,j)) by MATRIX_1:def 4,VECTSP_1:def 5;
hence thesis by VECTSP_1:def 5;
end;
theorem Th3:
for M1,M2 be Matrix of REAL st len M1=len M2 & width M1=width M2
& [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i,j))
proof
let M1,M2 be Matrix of REAL;
assume that
A1: len M1=len M2 and
A2: width M1=width M2 and
A3: [i,j] in Indices M1;
A4: 1<=j & j<=width M2 by A2,A3,MATRIXC1:1;
1<= i & i<=len M2 by A1,A3,MATRIXC1:1;
then
A5: [i,j] in Indices MXR2MXF M2 by A4,MATRIXC1:1;
(M1-M2)*(i,j) = ((MXR2MXF M1)+(-(MXR2MXF M2)))*(i,j) by MATRIX_1:def 7
,VECTSP_1:def 5
.= (MXR2MXF M1)*(i,j)+(-MXR2MXF M2)*(i,j) by A3,MATRIX_1:def 6
.= (MXR2MXF M1)*(i,j)+-((MXR2MXF M2)*(i,j)) by A5,MATRIX_1:def 4;
hence thesis by VECTSP_1:def 5;
end;
theorem Th4:
for M being Matrix of REAL st [i,j] in Indices M holds (a*M)*(i,j
)=a*(M*(i,j))
proof
let M be Matrix of REAL;
a in REAL by XREAL_0:def 1;
then reconsider aa=a as Element of F_Real by VECTSP_1:def 5;
A1: MXR2MXF(a*M) = MXR2MXF MXF2MXR (aa*(MXR2MXF M)) by MATRIXR1:def 7
.= aa*(MXR2MXF M);
assume [i,j] in Indices M;
then (a*M)*(i,j) = aa*((MXR2MXF M)*(i,j)) by A1,MATRIX_3:def 5,VECTSP_1:def 5
;
hence thesis by VECTSP_1:def 5;
end;
theorem Th5:
Indices M = Indices |:M:|
proof
A1: Seg len M = dom M by FINSEQ_1:def 3;
len |:M:|= len M & width |:M:| =width M by Def7;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem
|:a*M:|=|.a.|*|:M:|
proof
A1: len (a*M)=len M & width (a*M) =width M by MATRIXR1:27;
len (|.a.|*|:M:|)=len |:M:| by MATRIXR1:27;
then
A2: len (|.a.|*|:M:|)=len M by Def7;
A3: for i,j st [i,j] in Indices |:a*M:| holds |:a*M:|*(i,j) = (|.a.|*|:M:|)
*(i,j)
proof
A4: Indices (a*M) = Indices M by MATRIXR1:28;
A5: Indices (a*M) = Indices M by MATRIXR1:28;
let i,j;
assume
A6: [i,j] in Indices |:a*M:|;
A7: Indices |:M:| = Indices M by Th5;
A8: Indices |:a*M:| = Indices (a*M) by Th5;
then
A9: |:a*M:|*(i,j)=|.(a*M)*(i,j).| by A6,Def7
.=|.a*(M*(i,j)).| by A6,A8,A4,Th4
.=|.a.|*|.M*(i,j).| by COMPLEX1:65;
(|.a.|*|:M:|)*(i,j)=|.a.|*(|:M:|*(i,j)) by A6,A8,A5,Th4,A7
.=|:a*M:|*(i,j) by A6,A8,A9,A5,Def7;
hence thesis;
end;
width (|.a.|*|:M:|) =width |:M:| by MATRIXR1:27;
then
A10: width (|.a.|*|:M:|) =width M by Def7;
len |:a*M:|=len (a*M) & width |:a*M:|=width (a*M) by Def7;
hence thesis by A1,A2,A10,A3,MATRIX_0:21;
end;
theorem
M is Negative implies -M is Positive
proof
A1: Indices M=[:Seg n, Seg n:] & Indices (-M)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M is Negative;
for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)>0
proof
let i,j;
assume
A3: [i,j] in Indices (-M);
then M*(i,j)<0 by A2,A1;
then -M*(i,j)>0 by XREAL_1:58;
hence thesis by A1,A3,Th2;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is Positive implies M1+M2 is Positive
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Positive & M2 is Positive;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
proof
let i,j;
assume
A4: [i,j] in Indices (M1+M2);
then M1*(i,j) > 0 & M2*(i,j) > 0 by A3,A1,A2;
then M1*(i,j)+M2*(i,j)>0;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
-M2 is_less_than M1 implies M1+M2 is Positive
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A5: -M2 is_less_than M1;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
proof
let i,j;
assume
A6: [i,j] in Indices (M1+M2);
then (-M2)*(i,j)<M1*(i,j) by A5,A3,A4;
then -M2*(i,j)<M1*(i,j) by A2,A4,A6,Th2;
then M1*(i,j)+M2*(i,j)>0 by XREAL_1:62;
hence thesis by A1,A4,A6,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonnegative & M2 is Positive implies M1+M2 is Positive
proof
A1: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Nonnegative & M2 is Positive;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
proof
let i,j;
assume
A4: [i,j] in Indices (M1+M2);
then M1*(i,j)>=0 & M2*(i,j)>0 by A3,A1,A2;
then M1*(i,j)+M2*(i,j)>0;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies
M1+M2 is Positive
proof
assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M2:| is_less_than |:M1:|;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>0
proof
let i,j;
assume
A7: [i,j] in Indices (M1+M2);
then [i,j] in Indices |:M2:| by A4,A5,Th5;
then |:M2:|*(i,j)<|:M1:|*(i,j) by A3;
then |.M2*(i,j).|<|:M1:|*(i,j) by A4,A5,A7,Def7;
then |.M2*(i,j).|<|.M1*(i,j).| by A6,A5,A7,Def7;
then
A8: |.M1*(i,j).|-|.M2*(i,j).|>0 by XREAL_1:50;
M2*(i,j)<0 by A2,A4,A5,A7;
then
A9: -(M2*(i,j))=|.M2*(i,j).| by ABSVALUE:def 1;
M1*(i,j)>0 by A1,A6,A5,A7;
then M1*(i,j)=|.M1*(i,j).| by ABSVALUE:def 1;
then M1*(i,j)+M2*(i,j)>0 by A9,A8;
hence thesis by A6,A5,A7,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is Negative implies M1-M2 is Positive
proof
assume
A1: M1 is Positive & M2 is Negative;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>0
proof
let i,j;
assume
A5: [i,j] in Indices (M1-M2);
then M1*(i,j)>0 & M2*(i,j)<0 by A1,A2,A3;
then M1*(i,j)-M2*(i,j)>0-0;
hence thesis by A3,A4,A5,Th3;
end;
hence thesis;
end;
theorem
M2 is_less_than M1 implies M1-M2 is Positive
proof
assume
A1: M2 is_less_than M1;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M1 = [:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>0
proof
let i,j;
assume
A6: [i,j] in Indices (M1-M2);
then M1*(i,j)>M2*(i,j) by A1,A2,A4;
then M1*(i,j)-M2*(i,j)>0 by XREAL_1:50;
hence thesis by A4,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
a>0 & M is Positive implies a*M is Positive
proof
assume that
A1: a>0 and
A2: M is Positive;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>0
proof
let i,j;
assume [i,j] in Indices (a*M);
then
A3: [i,j] in Indices M by MATRIXR1:28;
then M*(i,j)>0 by A2;
then a*(M*(i,j))>0 by A1,XREAL_1:129;
hence thesis by A3,Th4;
end;
hence thesis;
end;
theorem
a<0 & M is Negative implies a*M is Positive
proof
assume that
A1: a<0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<0 by A2,A3;
then a*(M*(i,j))>0 by A1,XREAL_1:130;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
M is Positive implies (-M) is Negative
proof
A1: Indices M = [:Seg n, Seg n:] & Indices -M = [:Seg n, Seg n:] by MATRIX_0:24
;
assume
A2: M is Positive;
for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)<0
proof
let i,j;
assume
A3: [i,j] in Indices (-M);
then M*(i,j)>0 by A2,A1;
then (-1)*(M*(i,j))<0*(-1) by XREAL_1:69;
then -(M*(i,j))<0;
hence thesis by A1,A3,Th2;
end;
hence thesis;
end;
theorem
M1 is Negative & M2 is Negative implies M1+M2 is Negative
proof
assume that
A1: M1 is Negative and
A2: M2 is Negative;
A3: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
proof
let i,j;
assume
A6: [i,j] in Indices (M1+M2);
then M1*(i,j) < 0 by A1,A3,A4;
then M1*(i,j)+M2*(i,j)<M2*(i,j) by XREAL_1:30;
then M1*(i,j)+M2*(i,j)<0 by A2,A5,A4,A6;
hence thesis by A3,A4,A6,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_than -M2 implies M1+M2 is Negative
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A4: M1 is_less_than -M2;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
proof
let i,j;
assume
A5: [i,j] in Indices (M1+M2);
then M1*(i,j)<(-M2)*(i,j) by A4,A1,A3;
then M1*(i,j)<-M2*(i,j) by A2,A3,A5,Th2;
then M1*(i,j)+M2*(i,j)<0 by XREAL_1:61;
hence thesis by A1,A3,A5,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies
M1+M2 is Negative
proof
assume that
A1: M1 is Positive and
A2: M2 is Negative and
A3: |:M1:| is_less_than |:M2:|;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<0
proof
let i,j;
assume
A7: [i,j] in Indices (M1+M2);
then [i,j] in Indices |:M1:| by A4,A5,Th5;
then |:M1:|*(i,j)<|:M2:|*(i,j) by A3;
then |.M1*(i,j).|<|:M2:|*(i,j) by A4,A5,A7,Def7;
then |.M1*(i,j).|<|.M2*(i,j).| by A6,A5,A7,Def7;
then
A8: |.M1*(i,j).|-|.M2*(i,j).|<|.M2*(i,j).|-|.M2*(i,j).| by XREAL_1:9;
M2*(i,j)<0 by A2,A6,A5,A7;
then
A9: -(M2*(i,j))=|.M2*(i,j).| by ABSVALUE:def 1;
M1*(i,j)>0 by A1,A4,A5,A7;
then |.M1*(i,j).|=M1*(i,j) by ABSVALUE:def 1;
then M1*(i,j)+M2*(i,j)=|.M1*(i,j).|-|.M2*(i,j).| by A9;
hence thesis by A4,A5,A7,A8,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 implies M1-M2 is Negative
proof
assume
A1: M1 is_less_than M2;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)<0
proof
let i,j;
assume
A4: [i,j] in Indices (M1-M2);
then M1*(i,j)<M2*(i,j) by A1,A2;
then M1*(i,j)-M2*(i,j)<0 by XREAL_1:49;
hence thesis by A2,A3,A4,Th3;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is Negative implies M2-M1 is Negative
proof
assume
A1: M1 is Positive & M2 is Negative;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & Indices (M2-M1) = [:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<0
proof
let i,j;
assume
A5: [i,j] in Indices (M2-M1);
then M1*(i,j)>0 & M2*(i,j)<0 by A1,A2,A3;
then M2*(i,j)-M1*(i,j)<0;
hence thesis by A3,A4,A5,Th3;
end;
hence thesis;
end;
theorem
a<0 & M is Positive implies a*M is Negative
proof
assume that
A1: a<0 and
A2: M is Positive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)>0 by A2,A3;
then a*(M*(i,j))<0 by A1,XREAL_1:132;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a>0 & M is Negative implies a*M is Negative
proof
assume that
A1: a>0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<0 by A2,A3;
then a*(M*(i,j))<0 by A1,XREAL_1:132;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
M is Nonnegative implies -M is Nonpositive
proof
A1: Indices M = [:Seg n, Seg n:] & Indices -M = [:Seg n, Seg n:] by MATRIX_0:24
;
assume
A2: M is Nonnegative;
for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)<=0
proof
let i,j;
assume
A3: [i,j] in Indices (-M);
then M*(i,j)>=0 by A2,A1;
then -(M*(i,j))<=0;
hence thesis by A1,A3,Th2;
end;
hence thesis;
end;
theorem
M is Negative implies M is Nonpositive;
theorem
M1 is Nonpositive & M2 is Nonpositive implies M1+M2 is Nonpositive
proof
assume that
A1: M1 is Nonpositive and
A2: M2 is Nonpositive;
A3: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=0
proof
let i,j;
assume
A6: [i,j] in Indices (M1+M2);
then M1*(i,j) <= 0 by A1,A3,A4;
then
A7: (M1*(i,j))+(M2*(i,j))<=(M2*(i,j)) by XREAL_1:32;
M2*(i,j) <= 0 by A2,A5,A4,A6;
hence thesis by A3,A4,A6,A7,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with -M2 implies M1+M2 is Nonpositive
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A4: M1 is_less_or_equal_with (-M2);
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=0
proof
let i,j;
assume
A5: [i,j] in Indices (M1+M2);
then M1*(i,j)<=(-M2)*(i,j) by A4,A1,A3;
then M1*(i,j)<=-M2*(i,j) by A2,A3,A5,Th2;
then M1*(i,j)+M2*(i,j)<=0 by XREAL_1:59;
hence thesis by A1,A3,A5,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 implies M1-M2 is Nonpositive
proof
assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1-M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)<=0
proof
let i,j;
assume
A4: [i,j] in Indices (M1-M2);
then M1*(i,j)<=M2*(i,j) by A1,A2;
then M1*(i,j)-M2*(i,j)<=0 by XREAL_1:47;
hence thesis by A2,A3,A4,Th3;
end;
hence thesis;
end;
theorem
a<=0 & M is Positive implies a*M is Nonpositive
proof
assume that
A1: a<=0 and
A2: M is Positive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)>0 by A2,A3;
then a*(M*(i,j))<=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a>=0 & M is Negative implies a*M is Nonpositive
proof
assume that
A1: a>=0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<0 by A2,A3;
then a*(M*(i,j))<=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a>=0 & M is Nonpositive implies a*M is Nonpositive
proof
assume that
A1: a>=0 and
A2: M is Nonpositive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<=0 by A2,A3;
then a*(M*(i,j))<=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a<=0 & M is Nonnegative implies a*M is Nonpositive
proof
assume that
A1: a<=0 and
A2: M is Nonnegative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)<=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)>=0 by A2,A3;
then a*(M*(i,j))<=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
|:M:| is Nonnegative
proof
for i,j st [i,j] in Indices |:M:| holds |:M:|*(i,j)>=0
proof
let i,j;
assume
A1: [i,j] in Indices |:M:|;
Indices |:M:| = Indices M by Th5;
then |:M:|*(i,j)=|.M*(i,j).| by A1,Def7;
hence thesis by COMPLEX1:46;
end;
hence thesis;
end;
theorem
M1 is Positive implies M1 is Nonnegative;
theorem
M is Nonpositive implies (-M) is Nonnegative
proof
A1: Indices M = [:Seg n, Seg n:] & Indices (-M) = [:Seg n, Seg n:] by
MATRIX_0:24;
assume
A2: M is Nonpositive;
for i,j st [i,j] in Indices (-M) holds (-M)*(i,j)>=0
proof
let i,j;
assume
A3: [i,j] in Indices (-M);
then M*(i,j)<=0 by A2,A1;
then -M*(i,j)>=0;
hence thesis by A1,A3,Th2;
end;
hence thesis;
end;
theorem Th36:
M1 is Nonnegative & M2 is Nonnegative implies M1+M2 is Nonnegative
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M2) = [:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Nonnegative & M2 is Nonnegative;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>=0
proof
let i,j;
assume
A4: [i,j] in Indices (M1+M2);
then M1*(i,j)>=0 & M2*(i,j)>=0 by A3,A1,A2;
then (M1*(i,j))+(M2*(i,j))>=0;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
-M1 is_less_or_equal_with M2 implies M1+M2 is Nonnegative
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A4: -M1 is_less_or_equal_with M2;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)>=0
proof
let i,j;
assume
A5: [i,j] in Indices (M1+M2);
then (-M1)*(i,j)<=M2*(i,j) by A4,A2,A3;
then -M1*(i,j)<=M2*(i,j) by A1,A3,A5,Th2;
then M1*(i,j)+M2*(i,j)>=0 by XREAL_1:60;
hence thesis by A1,A3,A5,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M2 is_less_or_equal_with M1 implies M1-M2 is Nonnegative
proof
assume
A1: M2 is_less_or_equal_with M1;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M1 = [:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices (M1-M2) holds (M1-M2)*(i,j)>=0
proof
let i,j;
assume
A6: [i,j] in Indices (M1-M2);
then M1*(i,j)>=M2*(i,j) by A1,A2,A4;
then M1*(i,j)-M2*(i,j)>=0 by XREAL_1:48;
hence thesis by A4,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
a>=0 & M is Positive implies a*M is Nonnegative
proof
assume that
A1: a>=0 and
A2: M is Positive;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
proof
let i,j;
assume [i,j] in Indices (a*M);
then
A3: [i,j] in Indices M by MATRIXR1:28;
then M*(i,j)>0 by A2;
then a*(M*(i,j))>=0 by A1;
hence thesis by A3,Th4;
end;
hence thesis;
end;
theorem
a<=0 & M is Negative implies a*M is Nonnegative
proof
assume that
A1: a<=0 and
A2: M is Negative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<0 by A2,A3;
then a*(M*(i,j))>=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a<=0 & M is Nonpositive implies a*M is Nonnegative
proof
assume that
A1: a<=0 and
A2: M is Nonpositive;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)<=0 by A2,A3;
then a*(M*(i,j))>=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem Th42:
a>=0 & M is Nonnegative implies a*M is Nonnegative
proof
assume that
A1: a>=0 and
A2: M is Nonnegative;
A3: Indices (a*M) = Indices M by MATRIXR1:28;
for i,j st [i,j] in Indices (a*M) holds (a*M)*(i,j)>=0
proof
let i,j;
assume
A4: [i,j] in Indices (a*M);
then M*(i,j)>=0 by A2,A3;
then a*(M*(i,j))>=0 by A1;
hence thesis by A3,A4,Th4;
end;
hence thesis;
end;
theorem
a>=0 & b>=0 & M1 is Nonnegative & M2 is Nonnegative implies a*M1+b*M2
is Nonnegative
proof
assume a>=0 & b>=0 & M1 is Nonnegative & M2 is Nonnegative;
then a*M1 is Nonnegative & b*M2 is Nonnegative by Th42;
hence thesis by Th36;
end;
begin
theorem
M1 is_less_than M2 implies M1 is_less_or_equal_with M2;
theorem
M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3
proof
A1: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
assume
A2: M1 is_less_than M2 & M2 is_less_than M3;
for i,j st [i,j] in Indices M1 holds M1*(i,j)<M3*(i,j)
proof
let i,j;
assume [i,j] in Indices M1;
then M1*(i,j)<M2*(i,j) & M2*(i,j)<M3*(i,j) by A2,A1;
hence thesis by XXREAL_0:2;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & M3 is_less_than M4 implies (M1+M3) is_less_than ( M2+M4)
proof
A1: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M1 = [:Seg n, Seg n:] & Indices (M1+M3) = [:Seg n, Seg n:] by
MATRIX_0:24;
assume
A4: M1 is_less_than M2 & M3 is_less_than M4;
for i,j st [i,j] in Indices (M1+M3) holds (M1+M3)*(i,j)<(M2+M4)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (M1+M3);
then
A6: (M1+M3)*(i,j)=M1*(i,j)+M3*(i,j) & M2*(i,j)+M4*(i,j)=(M2+M4)*(i,j) by A1,A3,
MATRIXR1:25;
M1*(i,j)<M2*(i,j) & M3*(i,j)<M4*(i,j) by A4,A2,A3,A5;
hence thesis by A6,XREAL_1:8;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 implies M1+M3 is_less_than M2+M3
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M3) = [:Seg n, Seg n:] by MATRIX_0:24;
assume
A4: M1 is_less_than M2;
for i,j st [i,j] in Indices (M1+M3) holds (M1+M3)*(i,j)<(M2+M3)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (M1+M3);
then M1*(i,j)<M2*(i,j) by A4,A1,A3;
then M1*(i,j)+M3*(i,j)<M2*(i,j)+M3*(i,j) by XREAL_1:8;
then (M1+M3)*(i,j)<M2*(i,j)+M3*(i,j) by A1,A3,A5,MATRIXR1:25;
hence thesis by A2,A3,A5,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 implies M3-M2 is_less_than M3-M1
proof
assume
A1: M1 is_less_than M2;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M3-M1) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: width M2=width M3 by Lm3;
A5: Indices M3 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
A7: for i,j st [i,j] in Indices (M3-M1) holds (M3-M2)*(i,j)<(M3-M1)*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (M3-M1);
then M1*(i,j)<M2*(i,j) by A1,A2,A3;
then M3*(i,j)-M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:15;
then (M3-M2)*(i,j)<M3*(i,j)-M1*(i,j) by A3,A5,A4,A8,Th3;
hence thesis by A3,A6,A5,A4,A8,Th3;
end;
Indices (M3-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
hence thesis by A3,A7;
end;
theorem
|:M1+M2:| is_less_or_equal_with |:M1:|+|:M2:|
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A3: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices |:M1+M2:| holds |:M1+M2:|*(i,j)<=(|:M1:|+|:
M2:|)*(i,j)
proof
let i,j;
assume [i,j] in Indices |:M1+M2:|;
then
A4: [i,j] in Indices (M1+M2) by Th5;
then [i,j] in Indices |:M1:| by A1,A2,Th5;
then
A5: (|:M1:|+|:M2:|)*(i,j)=|:M1:|*(i,j)+|:M2:|*(i,j) by MATRIXR1:25
.=|.M1*(i,j).|+|:M2:|*(i,j) by A1,A2,A4,Def7
.=|.M1*(i,j).|+|.M2*(i,j).| by A3,A2,A4,Def7;
|:M1+M2:|*(i,j) =|.(M1+M2)*(i,j).| by A4,Def7
.=|.M1*(i,j)+M2*(i,j).| by A1,A2,A4,MATRIXR1:25;
hence thesis by A5,COMPLEX1:56;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 implies (M1-M3) is_less_or_equal_with (M2- M3)
proof
assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M2-M3)*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices (M1-M3);
then M1*(i,j)<=M2*(i,j) by A1,A2,A5;
then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M3*(i,j) by XREAL_1:9;
then (M1-M3)*(i,j)<=M2*(i,j)-M3*(i,j) by A2,A5,A6,A7,Th3;
hence thesis by A5,A4,A3,A7,Th3;
end;
hence thesis;
end;
theorem
(M1-M3) is_less_or_equal_with (M2-M3) implies M1 is_less_or_equal_with M2
proof
assume
A1: (M1-M3) is_less_or_equal_with (M2-M3);
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
for i,j st [i,j] in Indices M1 holds M1*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M1;
then (M1-M3)*(i,j)<=(M2-M3)*(i,j) by A1,A2,A5;
then M1*(i,j)-M3*(i,j)<=(M2-M3)*(i,j) by A6,A7,Th3;
then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M3*(i,j) by A2,A4,A3,A7,Th3;
then (M1*(i,j)-M3*(i,j))+M3*(i,j)<=(M2*(i,j)-M3*(i,j))+M3*(i,j) by
XREAL_1:6;
hence thesis;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2-M3 implies M3 is_less_or_equal_with M2-M1
proof
assume
A1: M1 is_less_or_equal_with M2-M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: len M2=len M3 & width M2=width M3 by Lm3;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices M3 holds M3*(i,j)<=(M2-M1)*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M3;
then M1*(i,j)<=(M2-M3)*(i,j) by A1,A2,A3;
then M1*(i,j)<=M2*(i,j)-M3*(i,j) by A5,A3,A4,A7,Th3;
then M3*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:11;
hence thesis by A5,A3,A6,A7,Th3;
end;
hence thesis;
end;
theorem
M1-M2 is_less_or_equal_with M3 implies M1-M3 is_less_or_equal_with M2
proof
assume
A1: M1-M2 is_less_or_equal_with M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M3 & width M1=width M3 by Lm3;
A4: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices (M1-M3);
then (M1-M2)*(i,j)<=M3*(i,j) by A1,A4,A5;
then M1*(i,j)-M2*(i,j)<=M3*(i,j) by A2,A5,A6,A7,Th3;
then M1*(i,j)-M3*(i,j)<=M2*(i,j) by XREAL_1:12;
hence thesis by A2,A5,A3,A7,Th3;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies M1-M4
is_less_than M2-M3
proof
assume
A1: M1 is_less_than M2 & M3 is_less_or_equal_with M4;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: width M2=width M3 by Lm3;
A6: Indices (M1-M4) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<(M2-M3)*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (M1-M4);
then M1*(i,j)<M2*(i,j) & M3*(i,j)<=M4*(i,j) by A1,A2,A4,A6;
then M1*(i,j)-M4*(i,j)<M2*(i,j)-M3*(i,j) by XREAL_1:14;
then (M1-M4)*(i,j)<M2*(i,j)-M3*(i,j) by A2,A6,A7,A8,Th3;
hence thesis by A6,A3,A5,A8,Th3;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies M1-M4
is_less_than M2-M3
proof
assume
A1: M1 is_less_or_equal_with M2 & M3 is_less_than M4;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: width M2=width M3 by Lm3;
A6: Indices (M1-M4) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<(M2-M3)*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (M1-M4);
then M1*(i,j)<=M2*(i,j) & M3*(i,j)<M4*(i,j) by A1,A2,A4,A6;
then M1*(i,j)-M4*(i,j)<M2*(i,j)-M3*(i,j) by XREAL_1:15;
then (M1-M4)*(i,j)<M2*(i,j)-M3*(i,j) by A2,A6,A7,A8,Th3;
hence thesis by A6,A3,A5,A8,Th3;
end;
hence thesis;
end;
theorem
M1-M2 is_less_or_equal_with M3-M4 implies M1-M3 is_less_or_equal_with M2-M4
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M2 & width M1=width M2 by Lm3;
A7: len M1=len M3 & width M1=width M3 by Lm3;
A8: len M3=len M4 & width M3=width M4 by Lm3;
assume
A9: M1-M2 is_less_or_equal_with M3-M4;
for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M2-M4)*(i,j)
proof
let i,j;
assume
A10: [i,j] in Indices (M1-M3);
then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A2,A3;
then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A3,A6,A10,Th3;
then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A4,A3,A8,A10,Th3;
then M1*(i,j)-M3*(i,j)<=M2*(i,j)-M4*(i,j) by XREAL_1:16;
then (M1-M3)*(i,j)<=M2*(i,j)-M4*(i,j) by A1,A3,A7,A10,Th3;
hence thesis by A5,A3,A6,A8,A7,A10,Th3;
end;
hence thesis;
end;
theorem
M1-M2 is_less_or_equal_with M3-M4 implies M4-M2 is_less_or_equal_with M3-M1
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M4 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M4-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: len M1=len M3 & width M1=width M3 by Lm3;
A7: len M3=len M4 & width M3=width M4 by Lm3;
A8: len M1=len M2 & width M1=width M2 by Lm3;
assume
A9: M1-M2 is_less_or_equal_with M3-M4;
for i,j st [i,j] in Indices (M4-M2) holds (M4-M2)*(i,j)<=(M3-M1)*(i,j)
proof
let i,j;
assume
A10: [i,j] in Indices (M4-M2);
then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A3,A5;
then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A5,A8,A10,Th3;
then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A2,A5,A7,A10,Th3;
then M4*(i,j)-M2*(i,j)<=M3*(i,j)-M1*(i,j) by XREAL_1:17;
then (M4-M2)*(i,j)<=M3*(i,j)-M1*(i,j) by A4,A5,A8,A7,A6,A10,Th3;
hence thesis by A2,A5,A6,A10,Th3;
end;
hence thesis;
end;
theorem
M1-M2 is_less_or_equal_with M3-M4 implies M4-M3 is_less_or_equal_with M2-M1
proof
A1: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M4 = [:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices M3 = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices (M1-M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices (M4-M3) = [:Seg n, Seg n:] by MATRIX_0:24;
A7: len M3=len M4 & width M3=width M4 by Lm3;
A8: len M1=len M2 & width M1=width M2 by Lm3;
assume
A9: M1-M2 is_less_or_equal_with M3-M4;
for i,j st [i,j] in Indices (M4-M3) holds (M4-M3)*(i,j)<=(M2-M1)*(i,j)
proof
let i,j;
assume
A10: [i,j] in Indices (M4-M3);
then (M1-M2)*(i,j)<=(M3-M4)*(i,j) by A9,A5,A6;
then M1*(i,j)-M2*(i,j)<=(M3-M4)*(i,j) by A1,A6,A8,A10,Th3;
then M1*(i,j)-M2*(i,j)<=M3*(i,j)-M4*(i,j) by A4,A6,A7,A10,Th3;
then M4*(i,j)-M3*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:18;
then (M4-M3)*(i,j)<=M2*(i,j)-M1*(i,j) by A3,A6,A7,A10,Th3;
hence thesis by A2,A6,A8,A10,Th3;
end;
hence thesis;
end;
theorem
M1+M2 is_less_or_equal_with M3 implies M1 is_less_or_equal_with M3-M2
proof
assume
A1: M1+M2 is_less_or_equal_with M3;
A2: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: Indices (M1+M2) = [:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M3 = [:Seg n, Seg n:] & len M2=len M3 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices M1 holds M1*(i,j)<=(M3-M2)*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices M1;
then (M1+M2)*(i,j)<=M3*(i,j) by A1,A2,A4;
then M1*(i,j)+M2*(i,j)<=M3*(i,j) by A6,MATRIXR1:25;
then M1*(i,j)<=M3*(i,j)-M2*(i,j) by XREAL_1:19;
hence thesis by A2,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
M1+M2 is_less_or_equal_with M3+M4 implies M1-M3 is_less_or_equal_with M4-M2
proof
assume
A1: M1+M2 is_less_or_equal_with M3+M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M4 by Lm3;
A4: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: Indices M4=[:Seg n, Seg n:] & len M2=len M4 by Lm3,MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: Indices (M1-M3)=[:Seg n,Seg n:] by MATRIX_0:24;
A8: len M1=len M3 & width M1=width M3 by Lm3;
for i,j st [i,j] in Indices (M1-M3) holds (M1-M3)*(i,j)<=(M4-M2)*(i,j)
proof
let i,j;
assume
A9: [i,j] in Indices (M1-M3);
then (M1+M2)*(i,j)<=(M3+M4)*(i,j) by A1,A4,A7;
then M1*(i,j)+M2*(i,j)<=(M3+M4)*(i,j) by A2,A7,A9,MATRIXR1:25;
then M1*(i,j)+M2*(i,j)<=M3*(i,j)+M4*(i,j) by A6,A7,A9,MATRIXR1:25;
then M1*(i,j)-M3*(i,j)<=M4*(i,j)-M2*(i,j) by XREAL_1:21;
then (M1-M3)*(i,j)<=M4*(i,j)-M2*(i,j) by A2,A7,A8,A9,Th3;
hence thesis by A7,A5,A3,A9,Th3;
end;
hence thesis;
end;
theorem
M1+M2 is_less_or_equal_with M3-M4 implies M1+M4 is_less_or_equal_with M3-M2
proof
assume
A1: M1+M2 is_less_or_equal_with M3-M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1+M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A4: Indices (M1+M4)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: len M2=len M3 & width M2=width M3 by Lm3;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: len M3=len M4 & width M3=width M4 by Lm3;
for i,j st [i,j] in Indices (M1+M4) holds (M1+M4)*(i,j)<=(M3-M2)*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (M1+M4);
then (M1+M2)*(i,j)<=(M3-M4)*(i,j) by A1,A3,A4;
then M1*(i,j)+M2*(i,j)<=(M3-M4)*(i,j) by A2,A4,A8,MATRIXR1:25;
then M1*(i,j)+M2*(i,j)<=M3*(i,j)-M4*(i,j) by A6,A4,A7,A8,Th3;
then M1*(i,j)+M4*(i,j)<=M3*(i,j)-M2*(i,j) by XREAL_1:22;
then (M1+M4)*(i,j)<=M3*(i,j)-M2*(i,j) by A2,A4,A8,MATRIXR1:25;
hence thesis by A6,A4,A5,A8,Th3;
end;
hence thesis;
end;
theorem
M1-M2 is_less_or_equal_with M3+M4 implies M1-M4 is_less_or_equal_with M3+M2
proof
assume
A1: M1-M2 is_less_or_equal_with M3+M4;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (M1-M2)=[:Seg n,Seg n:] by MATRIX_0:24;
A4: Indices (M1-M4)=[:Seg n,Seg n:] by MATRIX_0:24;
A5: len M1=len M2 & width M1=width M2 by Lm3;
A6: Indices M3=[:Seg n, Seg n:] by MATRIX_0:24;
A7: len M1=len M4 & width M1=width M4 by Lm3;
for i,j st [i,j] in Indices (M1-M4) holds (M1-M4)*(i,j)<=(M3+M2)*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (M1-M4);
then (M1-M2)*(i,j)<=(M3+M4)*(i,j) by A1,A3,A4;
then M1*(i,j)-M2*(i,j)<=(M3+M4)*(i,j) by A2,A4,A5,A8,Th3;
then M1*(i,j)-M2*(i,j)<=M3*(i,j)+M4*(i,j) by A6,A4,A8,MATRIXR1:25;
then M1*(i,j)-M4*(i,j)<=M3*(i,j)+M2*(i,j) by XREAL_1:23;
then (M1-M4)*(i,j)<=M3*(i,j)+M2*(i,j) by A2,A4,A7,A8,Th3;
hence thesis by A6,A4,A8,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 implies -M2 is_less_or_equal_with -M1
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A4: M1 is_less_or_equal_with M2;
for i,j st [i,j] in Indices (-M2) holds (-M2)*(i,j)<=(-M1)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (-M2);
then M1*(i,j)<=M2*(i,j) by A4,A1,A3;
then -M2*(i,j)<=-M1*(i,j) by XREAL_1:24;
then (-M2)*(i,j)<=-M1*(i,j) by A2,A3,A5,Th2;
hence thesis by A1,A3,A5,Th2;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with -M2 implies M2 is_less_or_equal_with -M1
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is_less_or_equal_with -M2;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(-M1)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)<=(-M2)*(i,j) by A2,A1;
then M1*(i,j)<=-M2*(i,j) by A3,Th2;
then M2*(i,j)<=-M1*(i,j) by XREAL_1:25;
hence thesis by A1,A3,Th2;
end;
hence thesis;
end;
theorem
-M2 is_less_or_equal_with M1 implies -M1 is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices (-M2)=[:Seg n, Seg n:] by MATRIX_0:24;
A4: Indices (-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A5: -M2 is_less_or_equal_with M1;
for i,j st [i,j] in Indices (-M1) holds (-M1)*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices (-M1);
then (-M2)*(i,j)<=M1*(i,j) by A5,A4,A3;
then -M2*(i,j)<=M1*(i,j) by A2,A4,A6,Th2;
then -M1*(i,j)<=M2*(i,j) by XREAL_1:26;
hence thesis by A1,A4,A6,Th2;
end;
hence thesis;
end;
theorem
M1 is Positive implies M2 is_less_than M2+M1
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is Positive;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M2+M1)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)>0 by A2,A1;
then M2*(i,j)<M2*(i,j)+M1*(i,j) by XREAL_1:29;
hence thesis by A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Negative implies M1+M2 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A2: M1 is Negative;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<M2*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices (M1+M2);
then M1*(i,j)<0 by A2,A1;
then M1*(i,j)+M2*(i,j)<M2*(i,j) by XREAL_1:30;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonnegative implies M2 is_less_or_equal_with M1+M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is Nonnegative;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M1+M2)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)>=0 by A2,A1;
then M2*(i,j)<=M1*(i,j)+M2*(i,j) by XREAL_1:31;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonpositive implies M1+M2 is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices (M1+M2)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A2: M1 is Nonpositive;
for i,j st [i,j] in Indices (M1+M2) holds (M1+M2)*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices (M1+M2);
then M1*(i,j)<=0 by A2,A1;
then M1*(i,j)+M2*(i,j)<=M2*(i,j) by XREAL_1:32;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonpositive & M3 is_less_or_equal_with M2 implies M3+M1
is_less_or_equal_with M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Nonpositive & M3 is_less_or_equal_with M2;
for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A4: [i,j] in Indices (M3+M1);
then M1*(i,j)<=0 & M3*(i,j)<=M2*(i,j) by A3,A1,A2;
then M3*(i,j)+M1*(i,j)<=M2*(i,j) by XREAL_1:35;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonpositive & M3 is_less_than M2 implies M3+M1 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Nonpositive & M3 is_less_than M2;
for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<M2*(i,j)
proof
let i,j;
assume
A4: [i,j] in Indices (M3+M1);
then M1*(i,j)<=0 & M3*(i,j)<M2*(i,j) by A3,A1,A2;
then M3*(i,j)+M1*(i,j)<M2*(i,j) by XREAL_1:36;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Negative & M3 is_less_or_equal_with M2 implies M3+M1 is_less_than M2
proof
A1: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A2: Indices M3=[:Seg n, Seg n:] & Indices (M3+M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
assume
A3: M1 is Negative & M3 is_less_or_equal_with M2;
for i,j st [i,j] in Indices (M3+M1) holds (M3+M1)*(i,j)<M2*(i,j)
proof
let i,j;
assume
A4: [i,j] in Indices (M3+M1);
then M1*(i,j)<0 & M3*(i,j)<=M2*(i,j) by A3,A1,A2;
then M3*(i,j)+M1*(i,j)<M2*(i,j) by XREAL_1:37;
hence thesis by A2,A4,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2
is_less_or_equal_with M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is Nonnegative & M2 is_less_or_equal_with M3;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M1+M3)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)>=0 & M2*(i,j)<=M3*(i,j) by A2,A1;
then M2*(i,j)<=M1*(i,j)+M3*(i,j) by XREAL_1:38;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is Positive & M2 is_less_or_equal_with M3;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M1+M3)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)>0 & M2*(i,j)<=M3*(i,j) by A2,A1;
then M2*(i,j)<M1*(i,j)+M3*(i,j) by XREAL_1:39;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than M1+M3
proof
A1: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
assume
A2: M1 is Nonnegative & M2 is_less_than M3;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M1+M3)*(i,j)
proof
let i,j;
assume
A3: [i,j] in Indices M2;
then M1*(i,j)>=0 & M2*(i,j)<M3*(i,j) by A2,A1;
then M2*(i,j)<M1*(i,j)+M3*(i,j) by XREAL_1:40;
hence thesis by A1,A3,MATRIXR1:25;
end;
hence thesis;
end;
theorem
M1 is Nonnegative implies M2-M1 is_less_or_equal_with M2
proof
assume
A1: M1 is Nonnegative;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<=M2*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices (M2-M1);
then M1*(i,j)>=0 by A1,A2,A4;
then M2*(i,j)-M1*(i,j)<=M2*(i,j) by XREAL_1:43;
hence thesis by A4,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
M1 is Positive implies M2-M1 is_less_than M2
proof
assume
A1: M1 is Positive;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<M2*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices (M2-M1);
then M1*(i,j)>0 by A1,A2,A4;
then M2*(i,j)-M1*(i,j)<M2*(i,j) by XREAL_1:44;
hence thesis by A4,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
M1 is Nonpositive implies M2 is_less_or_equal_with M2-M1
proof
assume
A1: M1 is Nonpositive;
A2: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M2-M1)*(i,j)
proof
let i,j;
assume
A4: [i,j] in Indices M2;
then M1*(i,j)<=0 by A1,A2;
then M2*(i,j)<=M2*(i,j)-M1*(i,j) by XREAL_1:45;
hence thesis by A3,A4,Th3;
end;
hence thesis;
end;
theorem
M1 is Negative implies M2 is_less_than M2-M1
proof
assume
A1: M1 is Negative;
A2: Indices M1=[:Seg n, Seg n:] & Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A3: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M2-M1)*(i,j)
proof
let i,j;
assume
A4: [i,j] in Indices M2;
then M1*(i,j)<0 by A1,A2;
then M2*(i,j)<M2*(i,j)-M1*(i,j) by XREAL_1:46;
hence thesis by A3,A4,Th3;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 implies M2-M1 is Nonnegative
proof
assume
A1: M1 is_less_or_equal_with M2;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M1=width M2 by Lm3;
A4: Indices (M2-M1)=[:Seg n, Seg n:] by MATRIX_0:24;
A5: Indices M2=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)>=0
proof
let i,j;
assume
A6: [i,j] in Indices (M2-M1);
then M1*(i,j)<=M2*(i,j) by A1,A2,A4;
then M2*(i,j)-M1*(i,j)>=0 by XREAL_1:48;
hence thesis by A4,A5,A3,A6,Th3;
end;
hence thesis;
end;
theorem
M1 is Nonnegative & M2 is_less_than M3 implies M2-M1 is_less_than M3
proof
assume
A1: M1 is Nonnegative & M2 is_less_than M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: Indices M2=[:Seg n, Seg n:] & Indices (M2-M1)=[:Seg n, Seg n:] by
MATRIX_0:24;
A4: len M1=len M2 & width M1=width M2 by Lm3;
for i,j st [i,j] in Indices (M2-M1) holds (M2-M1)*(i,j)<M3*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (M2-M1);
then M1*(i,j)>=0 & M2*(i,j)<M3*(i,j) by A1,A2,A3;
then M2*(i,j)-M1*(i,j)<M3*(i,j) by XREAL_1:51;
hence thesis by A3,A4,A5,Th3;
end;
hence thesis;
end;
theorem
M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2
is_less_or_equal_with M3-M1
proof
assume
A1: M1 is Nonpositive & M2 is_less_or_equal_with M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<=(M3-M1)*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M2;
then M1*(i,j)<=0 & M2*(i,j)<=M3*(i,j) by A1,A2,A5;
then M2*(i,j)<=M3*(i,j)-M1*(i,j) by XREAL_1:52;
hence thesis by A5,A6,A4,A3,A7,Th3;
end;
hence thesis;
end;
theorem
M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than M3-M1
proof
assume
A1: M1 is Nonpositive & M2 is_less_than M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M3-M1)*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M2;
then M1*(i,j)<=0 & M2*(i,j)<M3*(i,j) by A1,A2,A5;
then M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:53;
hence thesis by A5,A6,A4,A3,A7,Th3;
end;
hence thesis;
end;
theorem
M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than M3-M1
proof
assume
A1: M1 is Negative & M2 is_less_or_equal_with M3;
A2: Indices M1=[:Seg n, Seg n:] by MATRIX_0:24;
A3: width M2=width M3 by Lm3;
A4: width M1=width M2 & len M2=len M3 by Lm3;
A5: Indices M2=[:Seg n, Seg n:] by MATRIX_0:24;
A6: Indices M3=[:Seg n, Seg n:] & len M1=len M2 by Lm3,MATRIX_0:24;
for i,j st [i,j] in Indices M2 holds M2*(i,j)<(M3-M1)*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M2;
then M1*(i,j)<0 & M2*(i,j)<=M3*(i,j) by A1,A2,A5;
then M2*(i,j)<M3*(i,j)-M1*(i,j) by XREAL_1:54;
hence thesis by A5,A6,A4,A3,A7,Th3;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & a>0 implies a*M1 is_less_than a*M2
proof
assume that
A1: M1 is_less_than M2 and
A2: a>0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(a*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)<M2*(i,j) by A1,A3;
then a*(M1*(i,j))<a*(M2*(i,j)) by A2,XREAL_1:68;
then
A6: (a*M1)*(i,j)<a*(M2*(i,j)) by A3,A5,Th4;
[i,j] in Indices M2 by A4,A5,MATRIX_0:24;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2
proof
assume that
A1: M1 is_less_than M2 and
A2: a>=0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(a*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)<M2*(i,j) by A1,A3;
then a*(M1*(i,j))<=a*(M2*(i,j)) by A2,XREAL_1:64;
then
A6: (a*M1)*(i,j)<=a*(M2*(i,j)) by A3,A5,Th4;
[i,j] in Indices M2 by A4,A5,MATRIX_0:24;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & a<0 implies a*M2 is_less_than a*M1
proof
assume that
A1: M1 is_less_than M2 and
A2: a<0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<(a*M1)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M2);
then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
then M1*(i,j)<M2*(i,j) by A1;
then a*(M2*(i,j))<a*(M1*(i,j)) by A2,XREAL_1:69;
then (a*M2)*(i,j)<a*(M1*(i,j)) by A3,A5,Th4;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
M1 is_less_than M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1
proof
assume that
A1: M1 is_less_than M2 and
A2: a<=0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<=(a*M1)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M2);
then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
then M1*(i,j)<M2*(i,j) by A1;
then a*(M2*(i,j))<=a*(M1*(i,j)) by A2,XREAL_1:65;
then (a*M2)*(i,j)<=a*(M1*(i,j)) by A3,A5,Th4;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 & a>=0 implies a*M1 is_less_or_equal_with a*M2
proof
assume that
A1: M1 is_less_or_equal_with M2 and
A2: a>=0;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M2 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(a*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)<=M2*(i,j) by A1,A3;
then a*(M1*(i,j))<=a*(M2*(i,j)) by A2,XREAL_1:64;
then
A6: (a*M1)*(i,j)<=a*(M2*(i,j)) by A3,A5,Th4;
[i,j] in Indices M2 by A4,A5,MATRIX_0:24;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
M1 is_less_or_equal_with M2 & a<=0 implies a*M2 is_less_or_equal_with a*M1
proof
assume that
A1: M1 is_less_or_equal_with M2 and
A2: a<=0;
A3: Indices (a*M2) = Indices M2 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
for i,j st [i,j] in Indices (a*M2) holds (a*M2)*(i,j)<=(a*M1)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M2);
then
A6: [i,j] in Indices M1 by A4,MATRIX_0:24;
then M1*(i,j)<=M2*(i,j) by A1;
then a*(M2*(i,j))<=a*(M1*(i,j)) by A2,XREAL_1:65;
then (a*M2)*(i,j)<=a*(M1*(i,j)) by A3,A5,Th4;
hence thesis by A6,Th4;
end;
hence thesis;
end;
theorem
a>=0 & a<=b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies
a*M1 is_less_or_equal_with b*M2
proof
assume that
A1: a>=0 & a<=b and
A2: M1 is Nonnegative & M1 is_less_or_equal_with M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)>=0 & M1*(i,j)<=M2*(i,j) by A2,A3;
then a*(M1*(i,j))<=b*(M2*(i,j)) by A1,XREAL_1:66;
then (a*M1)*(i,j)<=b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;
theorem
a<=0 & b<=a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies
a*M1 is_less_or_equal_with b*M2
proof
assume that
A1: a<=0 & b<=a and
A2: M1 is Nonpositive & M2 is_less_or_equal_with M1;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<=(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)<=0 & M2*(i,j)<=M1*(i,j) by A2,A4,A3;
then a*(M1*(i,j))<=b*(M2*(i,j)) by A1,XREAL_1:67;
then (a*M1)*(i,j)<=b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;
theorem
a<0 & b<=a & M1 is Negative & M2 is_less_than M1 implies a*M1
is_less_than b*M2
proof
assume that
A1: a<0 & b<=a and
A2: M1 is Negative & M2 is_less_than M1;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)<0 & M2*(i,j)<M1*(i,j) by A2,A4,A3;
then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:70;
then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;
theorem
a>=0 & a<b & M1 is Nonnegative & M1 is_less_than M2 implies a*M1
is_less_than b*M2
proof
assume that
A1: a>=0 & a<b and
A2: M1 is Nonnegative & M1 is_less_than M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)>=0 & M1*(i,j)<M2*(i,j) by A2,A3;
then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:96;
then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;
theorem
a>=0 & a<b & M1 is Positive & M1 is_less_or_equal_with M2 implies a*M1
is_less_than b*M2
proof
assume that
A1: a>=0 & a<b and
A2: M1 is Positive & M1 is_less_or_equal_with M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)>0 & M1*(i,j)<=M2*(i,j) by A2,A3;
then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:97;
then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;
theorem
a>0 & a<=b & M1 is Positive & M1 is_less_than M2 implies a*M1
is_less_than b*M2
proof
assume that
A1: a>0 & a<=b and
A2: M1 is Positive & M1 is_less_than M2;
A3: Indices (a*M1) = Indices M1 by MATRIXR1:28;
A4: Indices M1 = [:Seg n, Seg n:] & Indices M2 = [:Seg n, Seg n:] by
MATRIX_0:24;
for i,j st [i,j] in Indices (a*M1) holds (a*M1)*(i,j)<(b*M2)*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices (a*M1);
then M1*(i,j)>0 & M1*(i,j)<M2*(i,j) by A2,A3;
then a*(M1*(i,j))<b*(M2*(i,j)) by A1,XREAL_1:98;
then (a*M1)*(i,j)<b*(M2*(i,j)) by A3,A5,Th4;
hence thesis by A4,A3,A5,Th4;
end;
hence thesis;
end;