:: by Xiquan Liang , Fuguo Ge and Xiaopeng Yue

::

:: Received October 19, 2006

:: Copyright (c) 2006-2019 Association of Mizar Users

definition

let M be Matrix of REAL;

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

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 ;

for i, j being Nat st [i,j] in Indices M holds

M * (i,j) < 0 ;

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

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

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

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

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;

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

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

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;

ex b_{1} being Matrix of REAL st

( len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = |.(M * (i,j)).| ) )

for b_{1}, b_{2} being Matrix of REAL st len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = |.(M * (i,j)).| ) & len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = |.(M * (i,j)).| ) holds

b_{1} = b_{2}

end;
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 ( 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)).| ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines |: MATRIX10:def 7 :

for M, b_{2} being Matrix of REAL holds

( b_{2} = |:M:| iff ( len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = |.(M * (i,j)).| ) ) );

for M, b

( b

b

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

end;
let M be Matrix of n,REAL;

:: original: -

redefine func - M -> Matrix of n,REAL;

coherence

- M is Matrix of n,REAL

proof 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

end;
let M be Matrix of n,REAL;

:: original: |:

redefine func |:M:| -> Matrix of n,REAL;

coherence

|:M:| is Matrix of n,REAL

proof 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

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

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

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

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

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

Lm1: 1 in REAL

by XREAL_0:def 1;

Lm2: - 1 in REAL

by XREAL_0:def 1;

registration

let n be Nat;

coherence

for b_{1} being Matrix of n,REAL st b_{1} = (n,n) --> 1 holds

b_{1} is Positive
by MATRIX_0:46, Lm1;

coherence

for b_{1} being Matrix of n,REAL st b_{1} = (n,n) --> (- 1) holds

b_{1} is Negative

for b_{1} being Matrix of n,REAL st b_{1} = (n,n) --> (- 1) holds

b_{1} is Nonpositive
by MATRIX_0:46, Lm2;

coherence

for b_{1} being Matrix of n,REAL st b_{1} = (n,n) --> 1 holds

b_{1} is Nonnegative
by MATRIX_0:46, Lm1;

end;
coherence

for b

b

coherence

for b

b

proof end;

coherence for b

b

coherence

for b

b

registration

let n be Nat;

ex b_{1} being Matrix of n,REAL st

( b_{1} is Positive & b_{1} is Nonnegative )

ex b_{1} being Matrix of n,REAL st

( b_{1} is Negative & b_{1} is Nonpositive )

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

existence ex b

( b

proof end;

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

existence ex b

( b

proof end;

registration

ex b_{1} being Matrix of REAL st

( b_{1} is Positive & b_{1} is Nonnegative )

ex b_{1} being Matrix of REAL st

( b_{1} is Negative & b_{1} is Nonpositive )
end;

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

existence ex b

( b

proof end;

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

existence ex b

( b

proof end;

registration
end;

registration
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

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

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

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

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

for M1, M2 being Matrix of n,REAL st M1 is Positive & M2 is Positive 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

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

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

for M1, M2 being Matrix of n,REAL st M1 is Positive & M2 is Negative 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

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

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

for M1, M2 being Matrix of n,REAL st M1 is Negative & M2 is Negative 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

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

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

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

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:25

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

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

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

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

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

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

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

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:34

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

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

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

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

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

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

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

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

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 ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;