:: Some Special Matrices of Real Elements and Their Properties :: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue :: :: Received October 19, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin definition let M be Matrix of REAL; attrM is Positive means :Def1: :: MATRIX10:def 1 for i, j being Nat st [i,j] in Indices M holds M * (i,j) > 0 ; attrM is Negative means :Def2: :: MATRIX10:def 2 for i, j being Nat st [i,j] in Indices M holds M * (i,j) < 0 ; attrM is Nonpositive means :Def3: :: MATRIX10:def 3 for i, j being Nat st [i,j] in Indices M holds M * (i,j) <= 0 ; attrM is Nonnegative means :Def4: :: MATRIX10:def 4 for i, j being Nat st [i,j] in Indices M holds M * (i,j) >= 0 ; end; :: deftheorem Def1 defines Positive MATRIX10:def_1_:_ for M being Matrix of REAL holds ( M is Positive iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) > 0 ); :: deftheorem Def2 defines Negative MATRIX10:def_2_:_ for M being Matrix of REAL holds ( M is Negative iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) < 0 ); :: deftheorem Def3 defines Nonpositive MATRIX10:def_3_:_ for M being Matrix of REAL holds ( M is Nonpositive iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) <= 0 ); :: deftheorem Def4 defines Nonnegative MATRIX10:def_4_:_ for M being Matrix of REAL holds ( M is Nonnegative iff for i, j being Nat st [i,j] in Indices M holds M * (i,j) >= 0 ); definition let M1, M2 be Matrix of REAL; predM1 is_less_than M2 means :Def5: :: MATRIX10:def 5 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) < M2 * (i,j); predM1 is_less_or_equal_with M2 means :Def6: :: MATRIX10:def 6 for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j); end; :: deftheorem Def5 defines is_less_than MATRIX10:def_5_:_ for M1, M2 being Matrix of REAL holds ( M1 is_less_than M2 iff for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) < M2 * (i,j) ); :: deftheorem Def6 defines is_less_or_equal_with MATRIX10:def_6_:_ for M1, M2 being Matrix of REAL holds ( M1 is_less_or_equal_with M2 iff for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) <= M2 * (i,j) ); definition let M be Matrix of REAL; func|:M:| -> Matrix of REAL means :Def7: :: MATRIX10:def 7 ( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds it * (i,j) = abs (M * (i,j)) ) ); existence ex b1 being Matrix of REAL st ( len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds b1 * (i,j) = abs (M * (i,j)) ) ) proofend; uniqueness for b1, b2 being Matrix of REAL st len b1 = len M & width b1 = width M & ( for i, j being Nat st [i,j] in Indices M holds b1 * (i,j) = abs (M * (i,j)) ) & len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds b2 * (i,j) = abs (M * (i,j)) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines |: MATRIX10:def_7_:_ for M, b2 being Matrix of REAL holds ( b2 = |:M:| iff ( len b2 = len M & width b2 = width M & ( for i, j being Nat st [i,j] in Indices M holds b2 * (i,j) = abs (M * (i,j)) ) ) ); definition let n be Nat; let M be Matrix of n, REAL ; :: original:- redefine func - M -> Matrix of n, REAL ; coherence - M is Matrix of n, REAL proofend; end; definition let n be Nat; let M1, M2 be Matrix of n, REAL ; :: original:+ redefine funcM1 + M2 -> Matrix of n, REAL ; coherence M1 + M2 is Matrix of n, REAL proofend; end; definition let n be Nat; let M1, M2 be Matrix of n, REAL ; :: original:- redefine funcM1 - M2 -> Matrix of n, REAL ; coherence M1 - M2 is Matrix of n, REAL proofend; end; definition let n be Nat; let a be Element of REAL ; let M be Matrix of n, REAL ; :: original:* redefine funca * M -> Matrix of n, REAL ; coherence a * M is Matrix of n, REAL proofend; end; registration cluster(1,1) --> 1 -> Positive for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Positive proofend; cluster(1,1) --> 1 -> Nonnegative for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds b1 is Nonnegative proofend; cluster(1,1) --> (- 1) -> Negative for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Negative proofend; cluster(1,1) --> (- 1) -> Nonpositive for Matrix of REAL; coherence for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds b1 is Nonpositive proofend; end; registration clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for FinSequence of K291(REAL); existence ex b1 being Matrix of REAL st ( b1 is Positive & b1 is Nonnegative ) proofend; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for FinSequence of K291(REAL); existence ex b1 being Matrix of REAL st ( b1 is Negative & b1 is Nonpositive ) proofend; end; registration let M be Positive Matrix of REAL; clusterM @ -> Positive ; coherence M @ is Positive proofend; end; registration let M be Negative Matrix of REAL; clusterM @ -> Negative ; coherence M @ is Negative proofend; end; registration let M be Nonpositive Matrix of REAL; clusterM @ -> Nonpositive ; coherence M @ is Nonpositive proofend; end; registration let M be Nonnegative Matrix of REAL; clusterM @ -> Nonnegative ; coherence M @ is Nonnegative proofend; end; registration let n be Nat; cluster(n,n) --> 1 -> Positive for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Positive proofend; cluster(n,n) --> (- 1) -> Negative for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Negative proofend; cluster(n,n) --> (- 1) -> Nonpositive for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds b1 is Nonpositive proofend; cluster(n,n) --> 1 -> Nonnegative for Matrix of n, REAL ; coherence for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds b1 is Nonnegative proofend; end; registration let n be Nat; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Positive Nonnegative for Matrix of n,n, REAL ; existence ex b1 being Matrix of n, REAL st ( b1 is Positive & b1 is Nonnegative ) proofend; clusterV16() V19( NAT ) V20(K291(REAL)) V21() FinSequence-like tabular Negative Nonpositive for Matrix of n,n, REAL ; existence ex b1 being Matrix of n, REAL st ( b1 is Negative & b1 is Nonpositive ) proofend; end; Lm1: for n being Nat for M1, M2 being Matrix of n, REAL holds ( len M1 = len M2 & width M1 = width M2 ) proofend; theorem :: MATRIX10:1 for x1 being Element of F_Real for x2 being Real st x1 = x2 holds - x1 = - x2 ; theorem Th2: :: MATRIX10:2 for i, j being Nat for M being Matrix of REAL st [i,j] in Indices M holds (- M) * (i,j) = - (M * (i,j)) proofend; theorem Th3: :: MATRIX10:3 for i, j being Nat for M1, M2 being 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)) proofend; theorem Th4: :: MATRIX10:4 for a being Element of REAL for i, j being Nat for M being Matrix of REAL st [i,j] in Indices M holds (a * M) * (i,j) = a * (M * (i,j)) proofend; theorem Th5: :: MATRIX10:5 for n being Nat for M being Matrix of n, REAL holds Indices M = Indices |:M:| proofend; theorem :: MATRIX10:6 for a being Element of REAL for n being Nat for M being Matrix of n, REAL holds |:(a * M):| = (abs a) * |:M:| proofend; theorem :: MATRIX10:7 for n being Nat for M being Matrix of n, REAL st M is Negative holds - M is Positive proofend; theorem :: MATRIX10:8 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Positive holds M1 + M2 is Positive proofend; theorem :: MATRIX10:9 for n being Nat for M2, M1 being Matrix of n, REAL st - M2 is_less_than M1 holds M1 + M2 is Positive proofend; theorem :: MATRIX10:10 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Positive holds M1 + M2 is Positive proofend; theorem :: MATRIX10:11 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| holds M1 + M2 is Positive proofend; theorem :: MATRIX10:12 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M1 - M2 is Positive proofend; theorem :: MATRIX10:13 for n being Nat for M2, M1 being Matrix of n, REAL st M2 is_less_than M1 holds M1 - M2 is Positive proofend; theorem :: MATRIX10:14 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a > 0 & M is Positive holds a * M is Positive proofend; theorem :: MATRIX10:15 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a < 0 & M is Negative holds a * M is Positive proofend; theorem :: MATRIX10:16 for n being Nat for M being Matrix of n, REAL st M is Positive holds - M is Negative proofend; theorem :: MATRIX10:17 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative & M2 is Negative holds M1 + M2 is Negative proofend; theorem :: MATRIX10:18 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than - M2 holds M1 + M2 is Negative proofend; theorem :: MATRIX10:19 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| holds M1 + M2 is Negative proofend; theorem :: MATRIX10:20 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 - M2 is Negative proofend; theorem :: MATRIX10:21 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive & M2 is Negative holds M2 - M1 is Negative proofend; theorem :: MATRIX10:22 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a < 0 & M is Positive holds a * M is Negative proofend; theorem :: MATRIX10:23 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a > 0 & M is Negative holds a * M is Negative proofend; theorem :: MATRIX10:24 for n being Nat for M being Matrix of n, REAL st M is Nonnegative holds - M is Nonpositive proofend; theorem :: MATRIX10:25 for n being Nat for M being Matrix of n, REAL st M is Negative holds M is Nonpositive proofend; theorem :: MATRIX10:26 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive & M2 is Nonpositive holds M1 + M2 is Nonpositive proofend; theorem :: MATRIX10:27 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M1 + M2 is Nonpositive proofend; theorem :: MATRIX10:28 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M2 is Nonpositive proofend; theorem :: MATRIX10:29 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Positive holds a * M is Nonpositive proofend; theorem :: MATRIX10:30 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Negative holds a * M is Nonpositive proofend; theorem :: MATRIX10:31 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonpositive holds a * M is Nonpositive proofend; theorem :: MATRIX10:32 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonnegative holds a * M is Nonpositive proofend; theorem :: MATRIX10:33 for n being Nat for M being Matrix of n, REAL holds |:M:| is Nonnegative proofend; theorem :: MATRIX10:34 for n being Nat for M1 being Matrix of n, REAL st M1 is Positive holds M1 is Nonnegative proofend; theorem :: MATRIX10:35 for n being Nat for M being Matrix of n, REAL st M is Nonpositive holds - M is Nonnegative proofend; theorem Th36: :: MATRIX10:36 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative & M2 is Nonnegative holds M1 + M2 is Nonnegative proofend; theorem :: MATRIX10:37 for n being Nat for M1, M2 being Matrix of n, REAL st - M1 is_less_or_equal_with M2 holds M1 + M2 is Nonnegative proofend; theorem :: MATRIX10:38 for n being Nat for M2, M1 being Matrix of n, REAL st M2 is_less_or_equal_with M1 holds M1 - M2 is Nonnegative proofend; theorem :: MATRIX10:39 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Positive holds a * M is Nonnegative proofend; theorem :: MATRIX10:40 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Negative holds a * M is Nonnegative proofend; theorem :: MATRIX10:41 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a <= 0 & M is Nonpositive holds a * M is Nonnegative proofend; theorem Th42: :: MATRIX10:42 for a being Element of REAL for n being Nat for M being Matrix of n, REAL st a >= 0 & M is Nonnegative holds a * M is Nonnegative proofend; theorem :: MATRIX10:43 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative holds (a * M1) + (b * M2) is Nonnegative proofend; begin theorem :: MATRIX10:44 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 holds M1 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:45 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 & M2 is_less_than M3 holds M1 is_less_than M3 proofend; theorem :: MATRIX10:46 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_than M4 holds M1 + M3 is_less_than M2 + M4 proofend; theorem :: MATRIX10:47 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M1 + M3 is_less_than M2 + M3 proofend; theorem :: MATRIX10:48 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_than M2 holds M3 - M2 is_less_than M3 - M1 proofend; theorem :: MATRIX10:49 for n being Nat for M1, M2 being Matrix of n, REAL holds |:(M1 + M2):| is_less_or_equal_with |:M1:| + |:M2:| proofend; theorem :: MATRIX10:50 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M1 - M3 is_less_or_equal_with M2 - M3 proofend; theorem :: MATRIX10:51 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 - M3 is_less_or_equal_with M2 - M3 holds M1 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:52 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is_less_or_equal_with M2 - M3 holds M3 is_less_or_equal_with M2 - M1 proofend; theorem :: MATRIX10:53 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 holds M1 - M3 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:54 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_than M2 & M3 is_less_or_equal_with M4 holds M1 - M4 is_less_than M2 - M3 proofend; theorem :: MATRIX10:55 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & M3 is_less_than M4 holds M1 - M4 is_less_than M2 - M3 proofend; theorem :: MATRIX10:56 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M1 - M3 is_less_or_equal_with M2 - M4 proofend; theorem :: MATRIX10:57 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M2 is_less_or_equal_with M3 - M1 proofend; theorem :: MATRIX10:58 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 - M4 holds M4 - M3 is_less_or_equal_with M2 - M1 proofend; theorem :: MATRIX10:59 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 holds M1 is_less_or_equal_with M3 - M2 proofend; theorem :: MATRIX10:60 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 + M4 holds M1 - M3 is_less_or_equal_with M4 - M2 proofend; theorem :: MATRIX10:61 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 + M2 is_less_or_equal_with M3 - M4 holds M1 + M4 is_less_or_equal_with M3 - M2 proofend; theorem :: MATRIX10:62 for n being Nat for M1, M2, M3, M4 being Matrix of n, REAL st M1 - M2 is_less_or_equal_with M3 + M4 holds M1 - M4 is_less_or_equal_with M3 + M2 proofend; theorem :: MATRIX10:63 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds - M2 is_less_or_equal_with - M1 proofend; theorem :: MATRIX10:64 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with - M2 holds M2 is_less_or_equal_with - M1 proofend; theorem :: MATRIX10:65 for n being Nat for M2, M1 being Matrix of n, REAL st - M2 is_less_or_equal_with M1 holds - M1 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:66 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 is_less_than M2 + M1 proofend; theorem :: MATRIX10:67 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative holds M1 + M2 is_less_than M2 proofend; theorem :: MATRIX10:68 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 is_less_or_equal_with M1 + M2 proofend; theorem :: MATRIX10:69 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M1 + M2 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:70 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:71 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Nonpositive & M3 is_less_than M2 holds M3 + M1 is_less_than M2 proofend; theorem :: MATRIX10:72 for n being Nat for M1, M3, M2 being Matrix of n, REAL st M1 is Negative & M3 is_less_or_equal_with M2 holds M3 + M1 is_less_than M2 proofend; theorem :: MATRIX10:73 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M1 + M3 proofend; theorem :: MATRIX10:74 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Positive & M2 is_less_or_equal_with M3 holds M2 is_less_than M1 + M3 proofend; theorem :: MATRIX10:75 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 is_less_than M1 + M3 proofend; theorem :: MATRIX10:76 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonnegative holds M2 - M1 is_less_or_equal_with M2 proofend; theorem :: MATRIX10:77 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Positive holds M2 - M1 is_less_than M2 proofend; theorem :: MATRIX10:78 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Nonpositive holds M2 is_less_or_equal_with M2 - M1 proofend; theorem :: MATRIX10:79 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is Negative holds M2 is_less_than M2 - M1 proofend; theorem :: MATRIX10:80 for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 holds M2 - M1 is Nonnegative proofend; theorem :: MATRIX10:81 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonnegative & M2 is_less_than M3 holds M2 - M1 is_less_than M3 proofend; theorem :: MATRIX10:82 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_or_equal_with M3 holds M2 is_less_or_equal_with M3 - M1 proofend; theorem :: MATRIX10:83 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Nonpositive & M2 is_less_than M3 holds M2 is_less_than M3 - M1 proofend; theorem :: MATRIX10:84 for n being Nat for M1, M2, M3 being Matrix of n, REAL st M1 is Negative & M2 is_less_or_equal_with M3 holds M2 is_less_than M3 - M1 proofend; theorem :: MATRIX10:85 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a > 0 holds a * M1 is_less_than a * M2 proofend; theorem :: MATRIX10:86 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 proofend; theorem :: MATRIX10:87 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a < 0 holds a * M2 is_less_than a * M1 proofend; theorem :: MATRIX10:88 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_than M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 proofend; theorem :: MATRIX10:89 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a >= 0 holds a * M1 is_less_or_equal_with a * M2 proofend; theorem :: MATRIX10:90 for a being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st M1 is_less_or_equal_with M2 & a <= 0 holds a * M2 is_less_or_equal_with a * M1 proofend; theorem :: MATRIX10:91 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 holds a * M1 is_less_or_equal_with b * M2 proofend; theorem :: MATRIX10:92 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 holds a * M1 is_less_or_equal_with b * M2 proofend; theorem :: MATRIX10:93 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 holds a * M1 is_less_than b * M2 proofend; theorem :: MATRIX10:94 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 holds a * M1 is_less_than b * M2 proofend; theorem :: MATRIX10:95 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 holds a * M1 is_less_than b * M2 proofend; theorem :: MATRIX10:96 for a, b being Element of REAL for n being Nat for M1, M2 being Matrix of n, REAL st a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 holds a * M1 is_less_than b * M2 proofend;