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

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 :: 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 :: MATRIX10:def 6
for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) <= M2 * (i,j);

end;

:: deftheorem 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 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) = |.(M * (i,j)).| ) );

existence
ex b₁ being Matrix of REAL st
( len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = |.(M * (i,j)).| ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of REAL st len b₁ = len M & width b₁ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₁ * (i,j) = |.(M * (i,j)).| ) & len b₂ = len M & width b₂ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (i,j) = |.(M * (i,j)).| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines |: MATRIX10:def 7 :
for M, b₂ being Matrix of REAL holds
( b₂ = |:M:| iff ( len b₂ = len M & width b₂ = width M & ( for i, j being Nat st [i,j] in Indices M holds
b₂ * (i,j) = |.(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 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 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;

Lm1: 1 in REAL
by XREAL_0:def 1;

Lm2: - 1 in REAL
by XREAL_0:def 1;

registration

let n be Nat;

cluster (n,n) --> 1 -> Positive for Matrix of n,REAL;

coherence
for b₁ being Matrix of n,REAL st b₁ = (n,n) --> 1 holds
b₁ is Positive by MATRIX_0:46, Lm1;

cluster (n,n) --> (- 1) -> Negative for Matrix of n,REAL;

coherence
for b₁ being Matrix of n,REAL st b₁ = (n,n) --> (- 1) holds
b₁ is Negative

proof end;

cluster (n,n) --> (- 1) -> Nonpositive for Matrix of n,REAL;

coherence
for b₁ being Matrix of n,REAL st b₁ = (n,n) --> (- 1) holds
b₁ is Nonpositive by MATRIX_0:46, Lm2;

cluster (n,n) --> 1 -> Nonnegative for Matrix of n,REAL;

coherence
for b₁ being Matrix of n,REAL st b₁ = (n,n) --> 1 holds
b₁ is Nonnegative by MATRIX_0:46, Lm1;

end;

registration

let n be Nat;

cluster V4() V7( NAT ) V8(K228(REAL)) V23() FinSequence-like tabular V125( REAL ,n,n) Positive Nonnegative for FinSequence of K228(REAL);

existence
ex b₁ being Matrix of n,REAL st
( b₁ is Positive & b₁ is Nonnegative )

proof end;

cluster V4() V7( NAT ) V8(K228(REAL)) V23() FinSequence-like tabular V125( REAL ,n,n) Negative Nonpositive for FinSequence of K228(REAL);

existence
ex b₁ being Matrix of n,REAL st
( b₁ is Negative & b₁ is Nonpositive )

proof end;

end;

registration

cluster V4() V7( NAT ) V8(K228(REAL)) V23() FinSequence-like tabular Positive Nonnegative for FinSequence of K228(REAL);

existence
ex b₁ being Matrix of REAL st
( b₁ is Positive & b₁ is Nonnegative )

proof end;

cluster V4() V7( NAT ) V8(K228(REAL)) V23() FinSequence-like tabular Negative Nonpositive for FinSequence of K228(REAL);

existence
ex b₁ being Matrix of REAL st
( b₁ is Negative & b₁ 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;

Lm3: 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 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 Real
for n being Nat
for M being Matrix of n,REAL holds |:(a * M):| = |.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 M1, M2 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 M1, M2 being Matrix of n,REAL st M2 is_less_than M1 holds
M1 - M2 is Positive

proof end;

theorem :: MATRIX10:14

for a being 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 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 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 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 ;

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

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 M1, M2 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 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 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 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 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 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;

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 ;

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, M2, M3 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 M1, M2 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, M2, M3 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, M2, M3 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, M2, M3 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 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 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 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 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 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 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 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 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 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 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 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 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;