:: Some Special Matrices of Real Elements and Their Properties
:: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue
::
:: Received October 19, 2006
:: Copyright (c) 2006-2011 Association of Mizar Users


begin

definition
let M be Matrix of REAL;
attr M is Positive means :Def1: :: MATRIX10:def 1
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) > 0 ;
attr M is Negative means :Def2: :: MATRIX10:def 2
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) < 0 ;
attr M is Nonpositive means :Def3: :: MATRIX10:def 3
 for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 0 ;
attr M 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;
pred M1 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);
pred M1 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)) ) )
proof end;
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
proof end;
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
proof end;
end;

definition
let n be Nat;
let M1, M2 be Matrix of n, REAL ;
:: original: +
redefine func M1 + M2 -> Matrix of n, REAL ;
coherence
M1 + M2 is Matrix of n, REAL
proof end;
end;

definition
let n be Nat;
let M1, M2 be Matrix of n, REAL ;
:: original: -
redefine func M1 - M2 -> Matrix of n, REAL ;
coherence
M1 - M2 is Matrix of n, REAL
proof end;
end;

definition
let n be Nat;
let a be Element of REAL ;
let M be Matrix of n, REAL ;
:: original: *
redefine func a * M -> Matrix of n, REAL ;
coherence
a * M is Matrix of n, REAL
proof end;
end;

registration
cluster (1,1) --> 1 -> Positive Matrix of REAL;
coherence
for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Positive
proof end;
cluster (1,1) --> 1 -> Nonnegative Matrix of REAL;
coherence
for b1 being Matrix of REAL st b1 = (1,1) --> 1 holds
b1 is Nonnegative
proof end;
cluster (1,1) --> (- 1) -> Negative Matrix of REAL;
coherence
for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Negative
proof end;
cluster (1,1) --> (- 1) -> Nonpositive Matrix of REAL;
coherence
for b1 being Matrix of REAL st b1 = (1,1) --> (- 1) holds
b1 is Nonpositive
proof end;
end;

registration
cluster V16() V19( NAT ) V20(K234(REAL)) V21() FinSequence-like tabular Positive Nonnegative FinSequence of K234(REAL);
existence
ex b1 being Matrix of REAL st
( b1 is Positive & b1 is Nonnegative )
proof end;
cluster V16() V19( NAT ) V20(K234(REAL)) V21() FinSequence-like tabular Negative Nonpositive FinSequence of K234(REAL);
existence
ex b1 being Matrix of REAL st
( b1 is Negative & b1 is Nonpositive )
proof end;
end;

registration
let M be Positive Matrix of REAL;
cluster M @ -> Positive ;
coherence
M @ is Positive
proof end;
end;

registration
let M be Negative Matrix of REAL;
cluster M @ -> Negative ;
coherence
M @ is Negative
proof end;
end;

registration
let M be Nonpositive Matrix of REAL;
cluster M @ -> Nonpositive ;
coherence
M @ is Nonpositive
proof end;
end;

registration
let M be Nonnegative Matrix of REAL;
cluster M @ -> Nonnegative ;
coherence
M @ is Nonnegative
proof end;
end;

registration
let n be Nat;
cluster (n,n) --> 1 -> Positive Matrix of n, REAL ;
coherence
for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Positive
proof end;
cluster (n,n) --> (- 1) -> Negative Matrix of n, REAL ;
coherence
for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Negative
proof end;
cluster (n,n) --> (- 1) -> Nonpositive Matrix of n, REAL ;
coherence
for b1 being Matrix of n, REAL st b1 = (n,n) --> (- 1) holds
b1 is Nonpositive
proof end;
cluster (n,n) --> 1 -> Nonnegative Matrix of n, REAL ;
coherence
for b1 being Matrix of n, REAL st b1 = (n,n) --> 1 holds
b1 is Nonnegative
proof end;
end;

registration
let n be Nat;
cluster V16() V19( NAT ) V20(K234(REAL)) V21() FinSequence-like tabular Positive Nonnegative Matrix of n,n, REAL ;
existence
ex b1 being Matrix of n, REAL st
( b1 is Positive & b1 is Nonnegative )
proof end;
cluster V16() V19( NAT ) V20(K234(REAL)) V21() FinSequence-like tabular Negative Nonpositive Matrix of n,n, REAL ;
existence
ex b1 being Matrix of n, REAL st
( b1 is Negative & b1 is Nonpositive )
proof end;
end;

Lm1: for n being Nat
for M1, M2 being Matrix of n, REAL holds
( len M1 = len M2 & width M1 = width M2 )
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

theorem Th5: :: MATRIX10:5
for n being Nat
for M being Matrix of n, REAL holds Indices M = Indices |:M:|
proof end;

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:|
proof end;

theorem :: MATRIX10:7
for n being Nat
for M being Matrix of n, REAL st M is Negative holds
- M is Positive
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

theorem :: MATRIX10:16
for n being Nat
for M being Matrix of n, REAL st M is Positive holds
- M is Negative
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

theorem :: MATRIX10:24
for n being Nat
for M being Matrix of n, REAL st M is Nonnegative holds
- M is Nonpositive
proof end;

theorem :: MATRIX10:25
for n being Nat
for M being Matrix of n, REAL st M is Negative holds
M is Nonpositive
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

theorem :: MATRIX10:33
for n being Nat
for M being Matrix of n, REAL holds |:M:| is Nonnegative
proof end;

theorem :: MATRIX10:34
for n being Nat
for M1 being Matrix of n, REAL st M1 is Positive holds
M1 is Nonnegative
proof end;

theorem :: MATRIX10:35
for n being Nat
for M being Matrix of n, REAL st M is Nonpositive holds
- M is Nonnegative
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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:|
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;