matrix10.miz



    begin

    reserve a,b for Real,

i,j,n for Nat,

M,M1,M2,M3,M4 for Matrix of n, REAL ;

    definition

      let M be Matrix of REAL ;

      :: MATRIX10:def1

      attr M is Positive means

      : Def1: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) > 0 ;

      :: MATRIX10:def2

      attr M is Negative means

      : Def2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) < 0 ;

      :: MATRIX10:def3

      attr M is Nonpositive means

      : Def3: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) <= 0 ;

      :: MATRIX10:def4

      attr M is Nonnegative means

      : Def4: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 ;

    end

    definition

      let M1,M2 be Matrix of REAL ;

      :: MATRIX10:def5

      pred M1 is_less_than M2 means for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) < (M2 * (i,j));

      :: MATRIX10:def6

      pred M1 is_less_or_equal_with M2 means for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) <= (M2 * (i,j));

    end

    definition

      let M be Matrix of REAL ;

      :: MATRIX10:def7

      func |:M:| -> Matrix of REAL means

      : Def7: ( len it ) = ( len M) & ( width it ) = ( width M) & for i, j holds [i, j] in ( Indices M) implies (it * (i,j)) = |.(M * (i,j)).|;

      existence

      proof

        deffunc F( Nat, Nat) = ( In ( |.(M * ($1,$2)).|, REAL ));

        consider M1 be Matrix of ( len M), ( width M), REAL such that

         A1: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take M1;

        

         A2: ( len M1) = ( len M) by MATRIX_0:def 2;

         A3:

        now

          per cases ;

            case

             A4: ( len M) = 0 ;

            then ( width M1) = 0 by A2, MATRIX_0:def 3;

            hence ( width M1) = ( width M) by A4, MATRIX_0:def 3;

          end;

            case ( len M) > 0 ;

            hence ( width M1) = ( width M) by MATRIX_0: 23;

          end;

        end;

        thus ( len M1) = ( len M) & ( width M1) = ( width M) by A3, A2;

        let i, j;

        assume

         A5: [i, j] in ( Indices M);

        ( dom M) = ( dom M1) by A2, FINSEQ_3: 29;

        

        hence (M1 * (i,j)) = ( In ( |.(M * (i,j)).|, REAL )) by A1, A3, A5

        .= |.(M * (i,j)).|;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of REAL ;

        assume that

         A6: ( len M1) = ( len M) and

         A7: ( width M1) = ( width M) and

         A8: for i, j st [i, j] in ( Indices M) holds (M1 * (i,j)) = |.(M * (i,j)).| and

         A9: ( len M2) = ( len M) & ( width M2) = ( width M) and

         A10: for i, j st [i, j] in ( Indices M) holds (M2 * (i,j)) = |.(M * (i,j)).|;

        now

          let i, j;

          assume

           A11: [i, j] in ( Indices M1);

          

           A12: ( dom M1) = ( dom M) by A6, FINSEQ_3: 29;

          

          hence (M1 * (i,j)) = |.(M * (i,j)).| by A7, A8, A11

          .= (M2 * (i,j)) by A7, A10, A11, A12;

        end;

        hence thesis by A6, A7, A9, MATRIX_0: 21;

      end;

    end

    definition

      let n;

      let M;

      :: original: -

      redefine

      func - M -> Matrix of n, REAL ;

      coherence

      proof

        ( len M) = n by MATRIX_0: 24;

        then

         A1: ( len ( - M)) = n by MATRIX_3:def 2;

        ( width M) = n by MATRIX_0: 24;

        then ( width ( - M)) = n by MATRIX_3:def 2;

        hence thesis by A1, MATRIX_0: 51;

      end;

    end

    definition

      let n;

      let M;

      :: original: |:

      redefine

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

      coherence

      proof

        ( len M) = n by MATRIX_0: 24;

        then

         A1: ( len |:M:|) = n by Def7;

        ( width M) = n by MATRIX_0: 24;

        then ( width |:M:|) = n by Def7;

        hence thesis by A1, MATRIX_0: 51;

      end;

    end

    definition

      let n;

      let M1, M2;

      :: original: +

      redefine

      func M1 + M2 -> Matrix of n, REAL ;

      coherence

      proof

        

         A1: ( width M2) = n by MATRIX_0: 24;

        ( width M1) = n by MATRIX_0: 24;

        then ( len (M1 + M2)) = ( len M1) & ( width (M1 + M2)) = ( width M2) by A1, MATRIX_3:def 3;

        hence thesis by A1, MATRIX_0: 24, MATRIX_0: 51;

      end;

    end

    definition

      let n;

      let M1, M2;

      :: original: -

      redefine

      func M1 - M2 -> Matrix of n, REAL ;

      coherence

      proof

        ( len (M1 + ( - M2))) = ( len M1) by MATRIX_3:def 3;

        hence thesis by MATRIX_4:def 1;

      end;

    end

    definition

      let n;

      let a be Real;

      let M;

      :: original: *

      redefine

      func a * M -> Matrix of n, REAL ;

      coherence

      proof

        

         A1: ( width (a * M)) = ( width M) by MATRIXR1: 27;

        ( width M) = n & ( len (a * M)) = ( len M) by MATRIXR1: 27, MATRIX_0: 24;

        hence thesis by A1, MATRIX_0: 24, MATRIX_0: 51;

      end;

    end

    

     Lm1: 1 in REAL by XREAL_0:def 1;

    

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

    registration

      let n;

      cluster ((n,n) --> 1) -> Positive;

      coherence by MATRIX_0: 46, Lm1;

      cluster ((n,n) --> ( - 1)) -> Negative;

      coherence

      proof

        let M be Matrix of n, REAL such that

         A1: M = ((n,n) --> ( - 1));

        let i, j;

        assume [i, j] in ( Indices M);

        then (M * (i,j)) = ( - 1) by A1, MATRIX_0: 46, Lm2;

        hence thesis;

      end;

      cluster ((n,n) --> ( - 1)) -> Nonpositive;

      coherence by MATRIX_0: 46, Lm2;

      cluster ((n,n) --> 1) -> Nonnegative;

      coherence by MATRIX_0: 46, Lm1;

    end

    registration

      let n;

      cluster Positive Nonnegative for Matrix of n, REAL ;

      existence

      proof

        take ((n,n) --> ( In (1, REAL )));

        thus thesis;

      end;

      cluster Negative Nonpositive for Matrix of n, REAL ;

      existence

      proof

        take ((n,n) --> ( - ( In (1, REAL ))));

        thus thesis;

      end;

    end

    registration

      cluster Positive Nonnegative for Matrix of REAL ;

      existence

      proof

        take ((1,1) --> ( In (1, REAL )));

        thus thesis;

      end;

      cluster Negative Nonpositive for Matrix of REAL ;

      existence

      proof

        take ((1,1) --> ( - ( In (1, REAL ))));

        thus thesis;

      end;

    end

    registration

      let M be Positive Matrix of REAL ;

      cluster (M @ ) -> Positive;

      coherence

      proof

        for i, j st [i, j] in ( Indices (M @ )) holds ((M @ ) * (i,j)) > 0

        proof

          let i, j;

          assume [i, j] in ( Indices (M @ ));

          then

           A1: [j, i] in ( Indices M) by MATRIX_0:def 6;

          then ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

          hence thesis by A1, Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let M be Negative Matrix of REAL ;

      cluster (M @ ) -> Negative;

      coherence

      proof

        for i, j st [i, j] in ( Indices (M @ )) holds ((M @ ) * (i,j)) < 0

        proof

          let i, j;

          assume [i, j] in ( Indices (M @ ));

          then

           A1: [j, i] in ( Indices M) by MATRIX_0:def 6;

          then ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

          hence thesis by A1, Def2;

        end;

        hence thesis;

      end;

    end

    registration

      let M be Nonpositive Matrix of REAL ;

      cluster (M @ ) -> Nonpositive;

      coherence

      proof

        for i, j st [i, j] in ( Indices (M @ )) holds ((M @ ) * (i,j)) <= 0

        proof

          let i, j;

          assume [i, j] in ( Indices (M @ ));

          then

           A1: [j, i] in ( Indices M) by MATRIX_0:def 6;

          then ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

          hence thesis by A1, Def3;

        end;

        hence thesis;

      end;

    end

    registration

      let M be Nonnegative Matrix of REAL ;

      cluster (M @ ) -> Nonnegative;

      coherence

      proof

        for i, j st [i, j] in ( Indices (M @ )) holds ((M @ ) * (i,j)) >= 0

        proof

          let i, j;

          assume [i, j] in ( Indices (M @ ));

          then

           A1: [j, i] in ( Indices M) by MATRIX_0:def 6;

          then ((M @ ) * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

          hence thesis by A1, Def4;

        end;

        hence thesis;

      end;

    end

    

     Lm3: ( len M1) = ( len M2) & ( width M1) = ( width M2)

    proof

      ( width M1) = n & ( len M1) = n by MATRIX_0: 24;

      hence thesis by MATRIX_0: 24;

    end;

    theorem :: MATRIX10:1

    for x1 be Element of F_Real holds for x2 be Real st x1 = x2 holds ( - x1) = ( - x2);

    theorem :: MATRIX10:2

    

     Th2: for M be Matrix of REAL st [i, j] in ( Indices M) holds (( - M) * (i,j)) = ( - (M * (i,j)))

    proof

      let M be Matrix of REAL ;

      assume [i, j] in ( Indices M);

      then (( - M) * (i,j)) = ( - (( MXR2MXF M) * (i,j))) by MATRIX_3:def 2, VECTSP_1:def 5;

      hence thesis by VECTSP_1:def 5;

    end;

    theorem :: MATRIX10:3

    

     Th3: for M1,M2 be Matrix of REAL st ( len M1) = ( len M2) & ( width M1) = ( width M2) & [i, j] in ( Indices M1) holds ((M1 - M2) * (i,j)) = ((M1 * (i,j)) - (M2 * (i,j)))

    proof

      let M1,M2 be Matrix of REAL ;

      assume that

       A1: ( len M1) = ( len M2) and

       A2: ( width M1) = ( width M2) and

       A3: [i, j] in ( Indices M1);

      

       A4: 1 <= j & j <= ( width M2) by A2, A3, MATRIXC1: 1;

      1 <= i & i <= ( len M2) by A1, A3, MATRIXC1: 1;

      then

       A5: [i, j] in ( Indices ( MXR2MXF M2)) by A4, MATRIXC1: 1;

      ((M1 - M2) * (i,j)) = ((( MXR2MXF M1) + ( - ( MXR2MXF M2))) * (i,j)) by MATRIX_4:def 1, VECTSP_1:def 5

      .= ((( MXR2MXF M1) * (i,j)) + (( - ( MXR2MXF M2)) * (i,j))) by A3, MATRIX_3:def 3

      .= ((( MXR2MXF M1) * (i,j)) + ( - (( MXR2MXF M2) * (i,j)))) by A5, MATRIX_3:def 2;

      hence thesis by VECTSP_1:def 5;

    end;

    theorem :: MATRIX10:4

    

     Th4: for M be Matrix of REAL st [i, j] in ( Indices M) holds ((a * M) * (i,j)) = (a * (M * (i,j)))

    proof

      let M be Matrix of REAL ;

      a in REAL by XREAL_0:def 1;

      then

      reconsider aa = a as Element of F_Real by VECTSP_1:def 5;

      

       A1: ( MXR2MXF (a * M)) = ( MXR2MXF ( MXF2MXR (aa * ( MXR2MXF M)))) by MATRIXR1:def 7

      .= (aa * ( MXR2MXF M));

      assume [i, j] in ( Indices M);

      then ((a * M) * (i,j)) = (aa * (( MXR2MXF M) * (i,j))) by A1, MATRIX_3:def 5, VECTSP_1:def 5;

      hence thesis by VECTSP_1:def 5;

    end;

    theorem :: MATRIX10:5

    

     Th5: ( Indices M) = ( Indices |:M:|)

    proof

      

       A1: ( Seg ( len M)) = ( dom M) by FINSEQ_1:def 3;

      ( len |:M:|) = ( len M) & ( width |:M:|) = ( width M) by Def7;

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: MATRIX10:6

     |:(a * M):| = ( |.a.| * |:M:|)

    proof

      

       A1: ( len (a * M)) = ( len M) & ( width (a * M)) = ( width M) by MATRIXR1: 27;

      ( len ( |.a.| * |:M:|)) = ( len |:M:|) by MATRIXR1: 27;

      then

       A2: ( len ( |.a.| * |:M:|)) = ( len M) by Def7;

      

       A3: for i, j st [i, j] in ( Indices |:(a * M):|) holds ( |:(a * M):| * (i,j)) = (( |.a.| * |:M:|) * (i,j))

      proof

        

         A4: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

        

         A5: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

        let i, j;

        assume

         A6: [i, j] in ( Indices |:(a * M):|);

        

         A7: ( Indices |:M:|) = ( Indices M) by Th5;

        

         A8: ( Indices |:(a * M):|) = ( Indices (a * M)) by Th5;

        

        then

         A9: ( |:(a * M):| * (i,j)) = |.((a * M) * (i,j)).| by A6, Def7

        .= |.(a * (M * (i,j))).| by A6, A8, A4, Th4

        .= ( |.a.| * |.(M * (i,j)).|) by COMPLEX1: 65;

        (( |.a.| * |:M:|) * (i,j)) = ( |.a.| * ( |:M:| * (i,j))) by A6, A8, A5, Th4, A7

        .= ( |:(a * M):| * (i,j)) by A6, A8, A9, A5, Def7;

        hence thesis;

      end;

      ( width ( |.a.| * |:M:|)) = ( width |:M:|) by MATRIXR1: 27;

      then

       A10: ( width ( |.a.| * |:M:|)) = ( width M) by Def7;

      ( len |:(a * M):|) = ( len (a * M)) & ( width |:(a * M):|) = ( width (a * M)) by Def7;

      hence thesis by A1, A2, A10, A3, MATRIX_0: 21;

    end;

    theorem :: MATRIX10:7

    M is Negative implies ( - M) is Positive

    proof

      

       A1: ( Indices M) = [:( Seg n), ( Seg n):] & ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M is Negative;

      for i, j st [i, j] in ( Indices ( - M)) holds (( - M) * (i,j)) > 0

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices ( - M));

        then (M * (i,j)) < 0 by A2, A1;

        then ( - (M * (i,j))) > 0 by XREAL_1: 58;

        hence thesis by A1, A3, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:8

    M1 is Positive & M2 is Positive implies (M1 + M2) is Positive

    proof

      

       A1: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Positive & M2 is Positive;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) > 0 & (M2 * (i,j)) > 0 by A3, A1, A2;

        then ((M1 * (i,j)) + (M2 * (i,j))) > 0 ;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:9

    ( - M2) is_less_than M1 implies (M1 + M2) is Positive

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices ( - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A5: ( - M2) is_less_than M1;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M1 + M2));

        then (( - M2) * (i,j)) < (M1 * (i,j)) by A5, A3, A4;

        then ( - (M2 * (i,j))) < (M1 * (i,j)) by A2, A4, A6, Th2;

        then ((M1 * (i,j)) + (M2 * (i,j))) > 0 by XREAL_1: 62;

        hence thesis by A1, A4, A6, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:10

    M1 is Nonnegative & M2 is Positive implies (M1 + M2) is Positive

    proof

      

       A1: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Nonnegative & M2 is Positive;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) >= 0 & (M2 * (i,j)) > 0 by A3, A1, A2;

        then ((M1 * (i,j)) + (M2 * (i,j))) > 0 ;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:11

    M1 is Positive & M2 is Negative & |:M2:| is_less_than |:M1:| implies (M1 + M2) is Positive

    proof

      assume that

       A1: M1 is Positive and

       A2: M2 is Negative and

       A3: |:M2:| is_less_than |:M1:|;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices (M1 + M2));

        then [i, j] in ( Indices |:M2:|) by A4, A5, Th5;

        then ( |:M2:| * (i,j)) < ( |:M1:| * (i,j)) by A3;

        then |.(M2 * (i,j)).| < ( |:M1:| * (i,j)) by A4, A5, A7, Def7;

        then |.(M2 * (i,j)).| < |.(M1 * (i,j)).| by A6, A5, A7, Def7;

        then

         A8: ( |.(M1 * (i,j)).| - |.(M2 * (i,j)).|) > 0 by XREAL_1: 50;

        (M2 * (i,j)) < 0 by A2, A4, A5, A7;

        then

         A9: ( - (M2 * (i,j))) = |.(M2 * (i,j)).| by ABSVALUE:def 1;

        (M1 * (i,j)) > 0 by A1, A6, A5, A7;

        then (M1 * (i,j)) = |.(M1 * (i,j)).| by ABSVALUE:def 1;

        then ((M1 * (i,j)) + (M2 * (i,j))) > 0 by A9, A8;

        hence thesis by A6, A5, A7, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:12

    M1 is Positive & M2 is Negative implies (M1 - M2) is Positive

    proof

      assume

       A1: M1 is Positive & M2 is Negative;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M2)) holds ((M1 - M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 - M2));

        then (M1 * (i,j)) > 0 & (M2 * (i,j)) < 0 by A1, A2, A3;

        then ((M1 * (i,j)) - (M2 * (i,j))) > ( 0 - 0 );

        hence thesis by A3, A4, A5, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:13

    M2 is_less_than M1 implies (M1 - M2) is Positive

    proof

      assume

       A1: M2 is_less_than M1;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M1) = ( width M2) by Lm3;

      

       A4: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M1) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 - M2)) holds ((M1 - M2) * (i,j)) > 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M1 - M2));

        then (M1 * (i,j)) > (M2 * (i,j)) by A1, A2, A4;

        then ((M1 * (i,j)) - (M2 * (i,j))) > 0 by XREAL_1: 50;

        hence thesis by A4, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:14

    a > 0 & M is Positive implies (a * M) is Positive

    proof

      assume that

       A1: a > 0 and

       A2: M is Positive;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) > 0

      proof

        let i, j;

        assume [i, j] in ( Indices (a * M));

        then

         A3: [i, j] in ( Indices M) by MATRIXR1: 28;

        then (M * (i,j)) > 0 by A2;

        then (a * (M * (i,j))) > 0 by A1, XREAL_1: 129;

        hence thesis by A3, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:15

    a < 0 & M is Negative implies (a * M) is Positive

    proof

      assume that

       A1: a < 0 and

       A2: M is Negative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) > 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) < 0 by A2, A3;

        then (a * (M * (i,j))) > 0 by A1, XREAL_1: 130;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:16

    M is Positive implies ( - M) is Negative

    proof

      

       A1: ( Indices M) = [:( Seg n), ( Seg n):] & ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M is Positive;

      for i, j st [i, j] in ( Indices ( - M)) holds (( - M) * (i,j)) < 0

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices ( - M));

        then (M * (i,j)) > 0 by A2, A1;

        then (( - 1) * (M * (i,j))) < ( 0 * ( - 1)) by XREAL_1: 69;

        then ( - (M * (i,j))) < 0 ;

        hence thesis by A1, A3, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:17

    M1 is Negative & M2 is Negative implies (M1 + M2) is Negative

    proof

      assume that

       A1: M1 is Negative and

       A2: M2 is Negative;

      

       A3: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) < 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) < 0 by A1, A3, A4;

        then ((M1 * (i,j)) + (M2 * (i,j))) < (M2 * (i,j)) by XREAL_1: 30;

        then ((M1 * (i,j)) + (M2 * (i,j))) < 0 by A2, A5, A4, A6;

        hence thesis by A3, A4, A6, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:18

    M1 is_less_than ( - M2) implies (M1 + M2) is Negative

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: M1 is_less_than ( - M2);

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) < 0

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) < (( - M2) * (i,j)) by A4, A1, A3;

        then (M1 * (i,j)) < ( - (M2 * (i,j))) by A2, A3, A5, Th2;

        then ((M1 * (i,j)) + (M2 * (i,j))) < 0 by XREAL_1: 61;

        hence thesis by A1, A3, A5, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:19

    M1 is Positive & M2 is Negative & |:M1:| is_less_than |:M2:| implies (M1 + M2) is Negative

    proof

      assume that

       A1: M1 is Positive and

       A2: M2 is Negative and

       A3: |:M1:| is_less_than |:M2:|;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) < 0

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices (M1 + M2));

        then [i, j] in ( Indices |:M1:|) by A4, A5, Th5;

        then ( |:M1:| * (i,j)) < ( |:M2:| * (i,j)) by A3;

        then |.(M1 * (i,j)).| < ( |:M2:| * (i,j)) by A4, A5, A7, Def7;

        then |.(M1 * (i,j)).| < |.(M2 * (i,j)).| by A6, A5, A7, Def7;

        then

         A8: ( |.(M1 * (i,j)).| - |.(M2 * (i,j)).|) < ( |.(M2 * (i,j)).| - |.(M2 * (i,j)).|) by XREAL_1: 9;

        (M2 * (i,j)) < 0 by A2, A6, A5, A7;

        then

         A9: ( - (M2 * (i,j))) = |.(M2 * (i,j)).| by ABSVALUE:def 1;

        (M1 * (i,j)) > 0 by A1, A4, A5, A7;

        then |.(M1 * (i,j)).| = (M1 * (i,j)) by ABSVALUE:def 1;

        then ((M1 * (i,j)) + (M2 * (i,j))) = ( |.(M1 * (i,j)).| - |.(M2 * (i,j)).|) by A9;

        hence thesis by A4, A5, A7, A8, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:20

    M1 is_less_than M2 implies (M1 - M2) is Negative

    proof

      assume

       A1: M1 is_less_than M2;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M2)) holds ((M1 - M2) * (i,j)) < 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M1 - M2));

        then (M1 * (i,j)) < (M2 * (i,j)) by A1, A2;

        then ((M1 * (i,j)) - (M2 * (i,j))) < 0 by XREAL_1: 49;

        hence thesis by A2, A3, A4, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:21

    M1 is Positive & M2 is Negative implies (M2 - M1) is Negative

    proof

      assume

       A1: M1 is Positive & M2 is Negative;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M2) = [:( Seg n), ( Seg n):] & ( Indices (M2 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M2 - M1)) holds ((M2 - M1) * (i,j)) < 0

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M2 - M1));

        then (M1 * (i,j)) > 0 & (M2 * (i,j)) < 0 by A1, A2, A3;

        then ((M2 * (i,j)) - (M1 * (i,j))) < 0 ;

        hence thesis by A3, A4, A5, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:22

    a < 0 & M is Positive implies (a * M) is Negative

    proof

      assume that

       A1: a < 0 and

       A2: M is Positive;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) < 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) > 0 by A2, A3;

        then (a * (M * (i,j))) < 0 by A1, XREAL_1: 132;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:23

    a > 0 & M is Negative implies (a * M) is Negative

    proof

      assume that

       A1: a > 0 and

       A2: M is Negative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) < 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) < 0 by A2, A3;

        then (a * (M * (i,j))) < 0 by A1, XREAL_1: 132;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:24

    M is Nonnegative implies ( - M) is Nonpositive

    proof

      

       A1: ( Indices M) = [:( Seg n), ( Seg n):] & ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M is Nonnegative;

      for i, j st [i, j] in ( Indices ( - M)) holds (( - M) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices ( - M));

        then (M * (i,j)) >= 0 by A2, A1;

        then ( - (M * (i,j))) <= 0 ;

        hence thesis by A1, A3, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:25

    M is Negative implies M is Nonpositive;

    theorem :: MATRIX10:26

    M1 is Nonpositive & M2 is Nonpositive implies (M1 + M2) is Nonpositive

    proof

      assume that

       A1: M1 is Nonpositive and

       A2: M2 is Nonpositive;

      

       A3: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) <= 0 by A1, A3, A4;

        then

         A7: ((M1 * (i,j)) + (M2 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 32;

        (M2 * (i,j)) <= 0 by A2, A5, A4, A6;

        hence thesis by A3, A4, A6, A7, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:27

    M1 is_less_or_equal_with ( - M2) implies (M1 + M2) is Nonpositive

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: M1 is_less_or_equal_with ( - M2);

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) <= (( - M2) * (i,j)) by A4, A1, A3;

        then (M1 * (i,j)) <= ( - (M2 * (i,j))) by A2, A3, A5, Th2;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= 0 by XREAL_1: 59;

        hence thesis by A1, A3, A5, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:28

    M1 is_less_or_equal_with M2 implies (M1 - M2) is Nonpositive

    proof

      assume

       A1: M1 is_less_or_equal_with M2;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M2)) holds ((M1 - M2) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M1 - M2));

        then (M1 * (i,j)) <= (M2 * (i,j)) by A1, A2;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= 0 by XREAL_1: 47;

        hence thesis by A2, A3, A4, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:29

    a <= 0 & M is Positive implies (a * M) is Nonpositive

    proof

      assume that

       A1: a <= 0 and

       A2: M is Positive;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) > 0 by A2, A3;

        then (a * (M * (i,j))) <= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:30

    a >= 0 & M is Negative implies (a * M) is Nonpositive

    proof

      assume that

       A1: a >= 0 and

       A2: M is Negative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) < 0 by A2, A3;

        then (a * (M * (i,j))) <= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:31

    a >= 0 & M is Nonpositive implies (a * M) is Nonpositive

    proof

      assume that

       A1: a >= 0 and

       A2: M is Nonpositive;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) <= 0 by A2, A3;

        then (a * (M * (i,j))) <= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:32

    a <= 0 & M is Nonnegative implies (a * M) is Nonpositive

    proof

      assume that

       A1: a <= 0 and

       A2: M is Nonnegative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) <= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) >= 0 by A2, A3;

        then (a * (M * (i,j))) <= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:33

     |:M:| is Nonnegative

    proof

      for i, j st [i, j] in ( Indices |:M:|) holds ( |:M:| * (i,j)) >= 0

      proof

        let i, j;

        assume

         A1: [i, j] in ( Indices |:M:|);

        ( Indices |:M:|) = ( Indices M) by Th5;

        then ( |:M:| * (i,j)) = |.(M * (i,j)).| by A1, Def7;

        hence thesis by COMPLEX1: 46;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:34

    M1 is Positive implies M1 is Nonnegative;

    theorem :: MATRIX10:35

    M is Nonpositive implies ( - M) is Nonnegative

    proof

      

       A1: ( Indices M) = [:( Seg n), ( Seg n):] & ( Indices ( - M)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M is Nonpositive;

      for i, j st [i, j] in ( Indices ( - M)) holds (( - M) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices ( - M));

        then (M * (i,j)) <= 0 by A2, A1;

        then ( - (M * (i,j))) >= 0 ;

        hence thesis by A1, A3, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:36

    

     Th36: M1 is Nonnegative & M2 is Nonnegative implies (M1 + M2) is Nonnegative

    proof

      

       A1: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Nonnegative & M2 is Nonnegative;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) >= 0 & (M2 * (i,j)) >= 0 by A3, A1, A2;

        then ((M1 * (i,j)) + (M2 * (i,j))) >= 0 ;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:37

    ( - M1) is_less_or_equal_with M2 implies (M1 + M2) is Nonnegative

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices ( - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: ( - M1) is_less_or_equal_with M2;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 + M2));

        then (( - M1) * (i,j)) <= (M2 * (i,j)) by A4, A2, A3;

        then ( - (M1 * (i,j))) <= (M2 * (i,j)) by A1, A3, A5, Th2;

        then ((M1 * (i,j)) + (M2 * (i,j))) >= 0 by XREAL_1: 60;

        hence thesis by A1, A3, A5, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:38

    M2 is_less_or_equal_with M1 implies (M1 - M2) is Nonnegative

    proof

      assume

       A1: M2 is_less_or_equal_with M1;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M1) = ( width M2) by Lm3;

      

       A4: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M1) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M1 - M2)) holds ((M1 - M2) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M1 - M2));

        then (M1 * (i,j)) >= (M2 * (i,j)) by A1, A2, A4;

        then ((M1 * (i,j)) - (M2 * (i,j))) >= 0 by XREAL_1: 48;

        hence thesis by A4, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:39

    a >= 0 & M is Positive implies (a * M) is Nonnegative

    proof

      assume that

       A1: a >= 0 and

       A2: M is Positive;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) >= 0

      proof

        let i, j;

        assume [i, j] in ( Indices (a * M));

        then

         A3: [i, j] in ( Indices M) by MATRIXR1: 28;

        then (M * (i,j)) > 0 by A2;

        then (a * (M * (i,j))) >= 0 by A1;

        hence thesis by A3, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:40

    a <= 0 & M is Negative implies (a * M) is Nonnegative

    proof

      assume that

       A1: a <= 0 and

       A2: M is Negative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) < 0 by A2, A3;

        then (a * (M * (i,j))) >= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:41

    a <= 0 & M is Nonpositive implies (a * M) is Nonnegative

    proof

      assume that

       A1: a <= 0 and

       A2: M is Nonpositive;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) <= 0 by A2, A3;

        then (a * (M * (i,j))) >= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:42

    

     Th42: a >= 0 & M is Nonnegative implies (a * M) is Nonnegative

    proof

      assume that

       A1: a >= 0 and

       A2: M is Nonnegative;

      

       A3: ( Indices (a * M)) = ( Indices M) by MATRIXR1: 28;

      for i, j st [i, j] in ( Indices (a * M)) holds ((a * M) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (a * M));

        then (M * (i,j)) >= 0 by A2, A3;

        then (a * (M * (i,j))) >= 0 by A1;

        hence thesis by A3, A4, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:43

    a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative implies ((a * M1) + (b * M2)) is Nonnegative

    proof

      assume a >= 0 & b >= 0 & M1 is Nonnegative & M2 is Nonnegative;

      then (a * M1) is Nonnegative & (b * M2) is Nonnegative by Th42;

      hence thesis by Th36;

    end;

    begin

    theorem :: MATRIX10:44

    M1 is_less_than M2 implies M1 is_less_or_equal_with M2;

    theorem :: MATRIX10:45

    M1 is_less_than M2 & M2 is_less_than M3 implies M1 is_less_than M3

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is_less_than M2 & M2 is_less_than M3;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) < (M3 * (i,j))

      proof

        let i, j;

        assume [i, j] in ( Indices M1);

        then (M1 * (i,j)) < (M2 * (i,j)) & (M2 * (i,j)) < (M3 * (i,j)) by A2, A1;

        hence thesis by XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:46

    M1 is_less_than M2 & M3 is_less_than M4 implies (M1 + M3) is_less_than (M2 + M4)

    proof

      

       A1: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: M1 is_less_than M2 & M3 is_less_than M4;

      for i, j st [i, j] in ( Indices (M1 + M3)) holds ((M1 + M3) * (i,j)) < ((M2 + M4) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 + M3));

        then

         A6: ((M1 + M3) * (i,j)) = ((M1 * (i,j)) + (M3 * (i,j))) & ((M2 * (i,j)) + (M4 * (i,j))) = ((M2 + M4) * (i,j)) by A1, A3, MATRIXR1: 25;

        (M1 * (i,j)) < (M2 * (i,j)) & (M3 * (i,j)) < (M4 * (i,j)) by A4, A2, A3, A5;

        hence thesis by A6, XREAL_1: 8;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:47

    M1 is_less_than M2 implies (M1 + M3) is_less_than (M2 + M3)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 + M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: M1 is_less_than M2;

      for i, j st [i, j] in ( Indices (M1 + M3)) holds ((M1 + M3) * (i,j)) < ((M2 + M3) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M1 + M3));

        then (M1 * (i,j)) < (M2 * (i,j)) by A4, A1, A3;

        then ((M1 * (i,j)) + (M3 * (i,j))) < ((M2 * (i,j)) + (M3 * (i,j))) by XREAL_1: 8;

        then ((M1 + M3) * (i,j)) < ((M2 * (i,j)) + (M3 * (i,j))) by A1, A3, A5, MATRIXR1: 25;

        hence thesis by A2, A3, A5, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:48

    M1 is_less_than M2 implies (M3 - M2) is_less_than (M3 - M1)

    proof

      assume

       A1: M1 is_less_than M2;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M3 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( width M2) = ( width M3) by Lm3;

      

       A5: ( Indices M3) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      

       A6: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      

       A7: for i, j st [i, j] in ( Indices (M3 - M1)) holds ((M3 - M2) * (i,j)) < ((M3 - M1) * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (M3 - M1));

        then (M1 * (i,j)) < (M2 * (i,j)) by A1, A2, A3;

        then ((M3 * (i,j)) - (M2 * (i,j))) < ((M3 * (i,j)) - (M1 * (i,j))) by XREAL_1: 15;

        then ((M3 - M2) * (i,j)) < ((M3 * (i,j)) - (M1 * (i,j))) by A3, A5, A4, A8, Th3;

        hence thesis by A3, A6, A5, A4, A8, Th3;

      end;

      ( Indices (M3 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      hence thesis by A3, A7;

    end;

    theorem :: MATRIX10:49

     |:(M1 + M2):| is_less_or_equal_with ( |:M1:| + |:M2:|)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices |:(M1 + M2):|) holds ( |:(M1 + M2):| * (i,j)) <= (( |:M1:| + |:M2:|) * (i,j))

      proof

        let i, j;

        assume [i, j] in ( Indices |:(M1 + M2):|);

        then

         A4: [i, j] in ( Indices (M1 + M2)) by Th5;

        then [i, j] in ( Indices |:M1:|) by A1, A2, Th5;

        

        then

         A5: (( |:M1:| + |:M2:|) * (i,j)) = (( |:M1:| * (i,j)) + ( |:M2:| * (i,j))) by MATRIXR1: 25

        .= ( |.(M1 * (i,j)).| + ( |:M2:| * (i,j))) by A1, A2, A4, Def7

        .= ( |.(M1 * (i,j)).| + |.(M2 * (i,j)).|) by A3, A2, A4, Def7;

        ( |:(M1 + M2):| * (i,j)) = |.((M1 + M2) * (i,j)).| by A4, Def7

        .= |.((M1 * (i,j)) + (M2 * (i,j))).| by A1, A2, A4, MATRIXR1: 25;

        hence thesis by A5, COMPLEX1: 56;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:50

    M1 is_less_or_equal_with M2 implies (M1 - M3) is_less_or_equal_with (M2 - M3)

    proof

      assume

       A1: M1 is_less_or_equal_with M2;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      

       A5: ( Indices (M1 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M3)) holds ((M1 - M3) * (i,j)) <= ((M2 - M3) * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices (M1 - M3));

        then (M1 * (i,j)) <= (M2 * (i,j)) by A1, A2, A5;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= ((M2 * (i,j)) - (M3 * (i,j))) by XREAL_1: 9;

        then ((M1 - M3) * (i,j)) <= ((M2 * (i,j)) - (M3 * (i,j))) by A2, A5, A6, A7, Th3;

        hence thesis by A5, A4, A3, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:51

    (M1 - M3) is_less_or_equal_with (M2 - M3) implies M1 is_less_or_equal_with M2

    proof

      assume

       A1: (M1 - M3) is_less_or_equal_with (M2 - M3);

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      

       A5: ( Indices (M1 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M1);

        then ((M1 - M3) * (i,j)) <= ((M2 - M3) * (i,j)) by A1, A2, A5;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= ((M2 - M3) * (i,j)) by A6, A7, Th3;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= ((M2 * (i,j)) - (M3 * (i,j))) by A2, A4, A3, A7, Th3;

        then (((M1 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j))) <= (((M2 * (i,j)) - (M3 * (i,j))) + (M3 * (i,j))) by XREAL_1: 6;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:52

    M1 is_less_or_equal_with (M2 - M3) implies M3 is_less_or_equal_with (M2 - M1)

    proof

      assume

       A1: M1 is_less_or_equal_with (M2 - M3);

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( len M2) = ( len M3) & ( width M2) = ( width M3) by Lm3;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices M3) holds (M3 * (i,j)) <= ((M2 - M1) * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M3);

        then (M1 * (i,j)) <= ((M2 - M3) * (i,j)) by A1, A2, A3;

        then (M1 * (i,j)) <= ((M2 * (i,j)) - (M3 * (i,j))) by A5, A3, A4, A7, Th3;

        then (M3 * (i,j)) <= ((M2 * (i,j)) - (M1 * (i,j))) by XREAL_1: 11;

        hence thesis by A5, A3, A6, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:53

    (M1 - M2) is_less_or_equal_with M3 implies (M1 - M3) is_less_or_equal_with M2

    proof

      assume

       A1: (M1 - M2) is_less_or_equal_with M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      

       A4: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices (M1 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M3)) holds ((M1 - M3) * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices (M1 - M3));

        then ((M1 - M2) * (i,j)) <= (M3 * (i,j)) by A1, A4, A5;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= (M3 * (i,j)) by A2, A5, A6, A7, Th3;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 12;

        hence thesis by A2, A5, A3, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:54

    M1 is_less_than M2 & M3 is_less_or_equal_with M4 implies (M1 - M4) is_less_than (M2 - M3)

    proof

      assume

       A1: M1 is_less_than M2 & M3 is_less_or_equal_with M4;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      

       A4: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( width M2) = ( width M3) by Lm3;

      

       A6: ( Indices (M1 - M4)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( len M1) = ( len M4) & ( width M1) = ( width M4) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M4)) holds ((M1 - M4) * (i,j)) < ((M2 - M3) * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (M1 - M4));

        then (M1 * (i,j)) < (M2 * (i,j)) & (M3 * (i,j)) <= (M4 * (i,j)) by A1, A2, A4, A6;

        then ((M1 * (i,j)) - (M4 * (i,j))) < ((M2 * (i,j)) - (M3 * (i,j))) by XREAL_1: 14;

        then ((M1 - M4) * (i,j)) < ((M2 * (i,j)) - (M3 * (i,j))) by A2, A6, A7, A8, Th3;

        hence thesis by A6, A3, A5, A8, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:55

    M1 is_less_or_equal_with M2 & M3 is_less_than M4 implies (M1 - M4) is_less_than (M2 - M3)

    proof

      assume

       A1: M1 is_less_or_equal_with M2 & M3 is_less_than M4;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      

       A4: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( width M2) = ( width M3) by Lm3;

      

       A6: ( Indices (M1 - M4)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( len M1) = ( len M4) & ( width M1) = ( width M4) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M4)) holds ((M1 - M4) * (i,j)) < ((M2 - M3) * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (M1 - M4));

        then (M1 * (i,j)) <= (M2 * (i,j)) & (M3 * (i,j)) < (M4 * (i,j)) by A1, A2, A4, A6;

        then ((M1 * (i,j)) - (M4 * (i,j))) < ((M2 * (i,j)) - (M3 * (i,j))) by XREAL_1: 15;

        then ((M1 - M4) * (i,j)) < ((M2 * (i,j)) - (M3 * (i,j))) by A2, A6, A7, A8, Th3;

        hence thesis by A6, A3, A5, A8, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:56

    (M1 - M2) is_less_or_equal_with (M3 - M4) implies (M1 - M3) is_less_or_equal_with (M2 - M4)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      

       A7: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      

       A8: ( len M3) = ( len M4) & ( width M3) = ( width M4) by Lm3;

      assume

       A9: (M1 - M2) is_less_or_equal_with (M3 - M4);

      for i, j st [i, j] in ( Indices (M1 - M3)) holds ((M1 - M3) * (i,j)) <= ((M2 - M4) * (i,j))

      proof

        let i, j;

        assume

         A10: [i, j] in ( Indices (M1 - M3));

        then ((M1 - M2) * (i,j)) <= ((M3 - M4) * (i,j)) by A9, A2, A3;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 - M4) * (i,j)) by A1, A3, A6, A10, Th3;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 * (i,j)) - (M4 * (i,j))) by A4, A3, A8, A10, Th3;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= ((M2 * (i,j)) - (M4 * (i,j))) by XREAL_1: 16;

        then ((M1 - M3) * (i,j)) <= ((M2 * (i,j)) - (M4 * (i,j))) by A1, A3, A7, A10, Th3;

        hence thesis by A5, A3, A6, A8, A7, A10, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:57

    (M1 - M2) is_less_or_equal_with (M3 - M4) implies (M4 - M2) is_less_or_equal_with (M3 - M1)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices M4) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices (M4 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      

       A7: ( len M3) = ( len M4) & ( width M3) = ( width M4) by Lm3;

      

       A8: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      assume

       A9: (M1 - M2) is_less_or_equal_with (M3 - M4);

      for i, j st [i, j] in ( Indices (M4 - M2)) holds ((M4 - M2) * (i,j)) <= ((M3 - M1) * (i,j))

      proof

        let i, j;

        assume

         A10: [i, j] in ( Indices (M4 - M2));

        then ((M1 - M2) * (i,j)) <= ((M3 - M4) * (i,j)) by A9, A3, A5;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 - M4) * (i,j)) by A1, A5, A8, A10, Th3;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 * (i,j)) - (M4 * (i,j))) by A2, A5, A7, A10, Th3;

        then ((M4 * (i,j)) - (M2 * (i,j))) <= ((M3 * (i,j)) - (M1 * (i,j))) by XREAL_1: 17;

        then ((M4 - M2) * (i,j)) <= ((M3 * (i,j)) - (M1 * (i,j))) by A4, A5, A8, A7, A6, A10, Th3;

        hence thesis by A2, A5, A6, A10, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:58

    (M1 - M2) is_less_or_equal_with (M3 - M4) implies (M4 - M3) is_less_or_equal_with (M2 - M1)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M4) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices (M4 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( len M3) = ( len M4) & ( width M3) = ( width M4) by Lm3;

      

       A8: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      assume

       A9: (M1 - M2) is_less_or_equal_with (M3 - M4);

      for i, j st [i, j] in ( Indices (M4 - M3)) holds ((M4 - M3) * (i,j)) <= ((M2 - M1) * (i,j))

      proof

        let i, j;

        assume

         A10: [i, j] in ( Indices (M4 - M3));

        then ((M1 - M2) * (i,j)) <= ((M3 - M4) * (i,j)) by A9, A5, A6;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 - M4) * (i,j)) by A1, A6, A8, A10, Th3;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 * (i,j)) - (M4 * (i,j))) by A4, A6, A7, A10, Th3;

        then ((M4 * (i,j)) - (M3 * (i,j))) <= ((M2 * (i,j)) - (M1 * (i,j))) by XREAL_1: 18;

        then ((M4 - M3) * (i,j)) <= ((M2 * (i,j)) - (M1 * (i,j))) by A3, A6, A7, A10, Th3;

        hence thesis by A2, A6, A8, A10, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:59

    (M1 + M2) is_less_or_equal_with M3 implies M1 is_less_or_equal_with (M3 - M2)

    proof

      assume

       A1: (M1 + M2) is_less_or_equal_with M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M3) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M3) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) <= ((M3 - M2) * (i,j))

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices M1);

        then ((M1 + M2) * (i,j)) <= (M3 * (i,j)) by A1, A2, A4;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= (M3 * (i,j)) by A6, MATRIXR1: 25;

        then (M1 * (i,j)) <= ((M3 * (i,j)) - (M2 * (i,j))) by XREAL_1: 19;

        hence thesis by A2, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:60

    (M1 + M2) is_less_or_equal_with (M3 + M4) implies (M1 - M3) is_less_or_equal_with (M4 - M2)

    proof

      assume

       A1: (M1 + M2) is_less_or_equal_with (M3 + M4);

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M4) by Lm3;

      

       A4: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M4) = [:( Seg n), ( Seg n):] & ( len M2) = ( len M4) by Lm3, MATRIX_0: 24;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( Indices (M1 - M3)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A8: ( len M1) = ( len M3) & ( width M1) = ( width M3) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M3)) holds ((M1 - M3) * (i,j)) <= ((M4 - M2) * (i,j))

      proof

        let i, j;

        assume

         A9: [i, j] in ( Indices (M1 - M3));

        then ((M1 + M2) * (i,j)) <= ((M3 + M4) * (i,j)) by A1, A4, A7;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= ((M3 + M4) * (i,j)) by A2, A7, A9, MATRIXR1: 25;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= ((M3 * (i,j)) + (M4 * (i,j))) by A6, A7, A9, MATRIXR1: 25;

        then ((M1 * (i,j)) - (M3 * (i,j))) <= ((M4 * (i,j)) - (M2 * (i,j))) by XREAL_1: 21;

        then ((M1 - M3) * (i,j)) <= ((M4 * (i,j)) - (M2 * (i,j))) by A2, A7, A8, A9, Th3;

        hence thesis by A7, A5, A3, A9, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:61

    (M1 + M2) is_less_or_equal_with (M3 - M4) implies (M1 + M4) is_less_or_equal_with (M3 - M2)

    proof

      assume

       A1: (M1 + M2) is_less_or_equal_with (M3 - M4);

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices (M1 + M4)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( len M2) = ( len M3) & ( width M2) = ( width M3) by Lm3;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( len M3) = ( len M4) & ( width M3) = ( width M4) by Lm3;

      for i, j st [i, j] in ( Indices (M1 + M4)) holds ((M1 + M4) * (i,j)) <= ((M3 - M2) * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (M1 + M4));

        then ((M1 + M2) * (i,j)) <= ((M3 - M4) * (i,j)) by A1, A3, A4;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= ((M3 - M4) * (i,j)) by A2, A4, A8, MATRIXR1: 25;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= ((M3 * (i,j)) - (M4 * (i,j))) by A6, A4, A7, A8, Th3;

        then ((M1 * (i,j)) + (M4 * (i,j))) <= ((M3 * (i,j)) - (M2 * (i,j))) by XREAL_1: 22;

        then ((M1 + M4) * (i,j)) <= ((M3 * (i,j)) - (M2 * (i,j))) by A2, A4, A8, MATRIXR1: 25;

        hence thesis by A6, A4, A5, A8, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:62

    (M1 - M2) is_less_or_equal_with (M3 + M4) implies (M1 - M4) is_less_or_equal_with (M3 + M2)

    proof

      assume

       A1: (M1 - M2) is_less_or_equal_with (M3 + M4);

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices (M1 - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices (M1 - M4)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A7: ( len M1) = ( len M4) & ( width M1) = ( width M4) by Lm3;

      for i, j st [i, j] in ( Indices (M1 - M4)) holds ((M1 - M4) * (i,j)) <= ((M3 + M2) * (i,j))

      proof

        let i, j;

        assume

         A8: [i, j] in ( Indices (M1 - M4));

        then ((M1 - M2) * (i,j)) <= ((M3 + M4) * (i,j)) by A1, A3, A4;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 + M4) * (i,j)) by A2, A4, A5, A8, Th3;

        then ((M1 * (i,j)) - (M2 * (i,j))) <= ((M3 * (i,j)) + (M4 * (i,j))) by A6, A4, A8, MATRIXR1: 25;

        then ((M1 * (i,j)) - (M4 * (i,j))) <= ((M3 * (i,j)) + (M2 * (i,j))) by XREAL_1: 23;

        then ((M1 - M4) * (i,j)) <= ((M3 * (i,j)) + (M2 * (i,j))) by A2, A4, A7, A8, Th3;

        hence thesis by A6, A4, A8, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:63

    M1 is_less_or_equal_with M2 implies ( - M2) is_less_or_equal_with ( - M1)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices ( - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A4: M1 is_less_or_equal_with M2;

      for i, j st [i, j] in ( Indices ( - M2)) holds (( - M2) * (i,j)) <= (( - M1) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices ( - M2));

        then (M1 * (i,j)) <= (M2 * (i,j)) by A4, A1, A3;

        then ( - (M2 * (i,j))) <= ( - (M1 * (i,j))) by XREAL_1: 24;

        then (( - M2) * (i,j)) <= ( - (M1 * (i,j))) by A2, A3, A5, Th2;

        hence thesis by A1, A3, A5, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:64

    M1 is_less_or_equal_with ( - M2) implies M2 is_less_or_equal_with ( - M1)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is_less_or_equal_with ( - M2);

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) <= (( - M1) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) <= (( - M2) * (i,j)) by A2, A1;

        then (M1 * (i,j)) <= ( - (M2 * (i,j))) by A3, Th2;

        then (M2 * (i,j)) <= ( - (M1 * (i,j))) by XREAL_1: 25;

        hence thesis by A1, A3, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:65

    ( - M2) is_less_or_equal_with M1 implies ( - M1) is_less_or_equal_with M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices ( - M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( Indices ( - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A5: ( - M2) is_less_or_equal_with M1;

      for i, j st [i, j] in ( Indices ( - M1)) holds (( - M1) * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices ( - M1));

        then (( - M2) * (i,j)) <= (M1 * (i,j)) by A5, A4, A3;

        then ( - (M2 * (i,j))) <= (M1 * (i,j)) by A2, A4, A6, Th2;

        then ( - (M1 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 26;

        hence thesis by A1, A4, A6, Th2;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:66

    M1 is Positive implies M2 is_less_than (M2 + M1)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Positive;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M2 + M1) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) > 0 by A2, A1;

        then (M2 * (i,j)) < ((M2 * (i,j)) + (M1 * (i,j))) by XREAL_1: 29;

        hence thesis by A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:67

    M1 is Negative implies (M1 + M2) is_less_than M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Negative;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) < (M2 * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) < 0 by A2, A1;

        then ((M1 * (i,j)) + (M2 * (i,j))) < (M2 * (i,j)) by XREAL_1: 30;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:68

    M1 is Nonnegative implies M2 is_less_or_equal_with (M1 + M2)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Nonnegative;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) <= ((M1 + M2) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) >= 0 by A2, A1;

        then (M2 * (i,j)) <= ((M1 * (i,j)) + (M2 * (i,j))) by XREAL_1: 31;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:69

    M1 is Nonpositive implies (M1 + M2) is_less_or_equal_with M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices (M1 + M2)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Nonpositive;

      for i, j st [i, j] in ( Indices (M1 + M2)) holds ((M1 + M2) * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices (M1 + M2));

        then (M1 * (i,j)) <= 0 by A2, A1;

        then ((M1 * (i,j)) + (M2 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 32;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:70

    M1 is Nonpositive & M3 is_less_or_equal_with M2 implies (M3 + M1) is_less_or_equal_with M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M3) = [:( Seg n), ( Seg n):] & ( Indices (M3 + M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Nonpositive & M3 is_less_or_equal_with M2;

      for i, j st [i, j] in ( Indices (M3 + M1)) holds ((M3 + M1) * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M3 + M1));

        then (M1 * (i,j)) <= 0 & (M3 * (i,j)) <= (M2 * (i,j)) by A3, A1, A2;

        then ((M3 * (i,j)) + (M1 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 35;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:71

    M1 is Nonpositive & M3 is_less_than M2 implies (M3 + M1) is_less_than M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M3) = [:( Seg n), ( Seg n):] & ( Indices (M3 + M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Nonpositive & M3 is_less_than M2;

      for i, j st [i, j] in ( Indices (M3 + M1)) holds ((M3 + M1) * (i,j)) < (M2 * (i,j))

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M3 + M1));

        then (M1 * (i,j)) <= 0 & (M3 * (i,j)) < (M2 * (i,j)) by A3, A1, A2;

        then ((M3 * (i,j)) + (M1 * (i,j))) < (M2 * (i,j)) by XREAL_1: 36;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:72

    M1 is Negative & M3 is_less_or_equal_with M2 implies (M3 + M1) is_less_than M2

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A2: ( Indices M3) = [:( Seg n), ( Seg n):] & ( Indices (M3 + M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A3: M1 is Negative & M3 is_less_or_equal_with M2;

      for i, j st [i, j] in ( Indices (M3 + M1)) holds ((M3 + M1) * (i,j)) < (M2 * (i,j))

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices (M3 + M1));

        then (M1 * (i,j)) < 0 & (M3 * (i,j)) <= (M2 * (i,j)) by A3, A1, A2;

        then ((M3 * (i,j)) + (M1 * (i,j))) < (M2 * (i,j)) by XREAL_1: 37;

        hence thesis by A2, A4, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:73

    M1 is Nonnegative & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with (M1 + M3)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Nonnegative & M2 is_less_or_equal_with M3;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) <= ((M1 + M3) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) >= 0 & (M2 * (i,j)) <= (M3 * (i,j)) by A2, A1;

        then (M2 * (i,j)) <= ((M1 * (i,j)) + (M3 * (i,j))) by XREAL_1: 38;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:74

    M1 is Positive & M2 is_less_or_equal_with M3 implies M2 is_less_than (M1 + M3)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Positive & M2 is_less_or_equal_with M3;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M1 + M3) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) > 0 & (M2 * (i,j)) <= (M3 * (i,j)) by A2, A1;

        then (M2 * (i,j)) < ((M1 * (i,j)) + (M3 * (i,j))) by XREAL_1: 39;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:75

    M1 is Nonnegative & M2 is_less_than M3 implies M2 is_less_than (M1 + M3)

    proof

      

       A1: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      assume

       A2: M1 is Nonnegative & M2 is_less_than M3;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M1 + M3) * (i,j))

      proof

        let i, j;

        assume

         A3: [i, j] in ( Indices M2);

        then (M1 * (i,j)) >= 0 & (M2 * (i,j)) < (M3 * (i,j)) by A2, A1;

        then (M2 * (i,j)) < ((M1 * (i,j)) + (M3 * (i,j))) by XREAL_1: 40;

        hence thesis by A1, A3, MATRIXR1: 25;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:76

    M1 is Nonnegative implies (M2 - M1) is_less_or_equal_with M2

    proof

      assume

       A1: M1 is Nonnegative;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M1) = ( width M2) by Lm3;

      

       A4: ( Indices (M2 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M2 - M1)) holds ((M2 - M1) * (i,j)) <= (M2 * (i,j))

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M2 - M1));

        then (M1 * (i,j)) >= 0 by A1, A2, A4;

        then ((M2 * (i,j)) - (M1 * (i,j))) <= (M2 * (i,j)) by XREAL_1: 43;

        hence thesis by A4, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:77

    M1 is Positive implies (M2 - M1) is_less_than M2

    proof

      assume

       A1: M1 is Positive;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M1) = ( width M2) by Lm3;

      

       A4: ( Indices (M2 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M2 - M1)) holds ((M2 - M1) * (i,j)) < (M2 * (i,j))

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M2 - M1));

        then (M1 * (i,j)) > 0 by A1, A2, A4;

        then ((M2 * (i,j)) - (M1 * (i,j))) < (M2 * (i,j)) by XREAL_1: 44;

        hence thesis by A4, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:78

    M1 is Nonpositive implies M2 is_less_or_equal_with (M2 - M1)

    proof

      assume

       A1: M1 is Nonpositive;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) <= ((M2 - M1) * (i,j))

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices M2);

        then (M1 * (i,j)) <= 0 by A1, A2;

        then (M2 * (i,j)) <= ((M2 * (i,j)) - (M1 * (i,j))) by XREAL_1: 45;

        hence thesis by A3, A4, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:79

    M1 is Negative implies M2 is_less_than (M2 - M1)

    proof

      assume

       A1: M1 is Negative;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M2 - M1) * (i,j))

      proof

        let i, j;

        assume

         A4: [i, j] in ( Indices M2);

        then (M1 * (i,j)) < 0 by A1, A2;

        then (M2 * (i,j)) < ((M2 * (i,j)) - (M1 * (i,j))) by XREAL_1: 46;

        hence thesis by A3, A4, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:80

    M1 is_less_or_equal_with M2 implies (M2 - M1) is Nonnegative

    proof

      assume

       A1: M1 is_less_or_equal_with M2;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M1) = ( width M2) by Lm3;

      

       A4: ( Indices (M2 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (M2 - M1)) holds ((M2 - M1) * (i,j)) >= 0

      proof

        let i, j;

        assume

         A6: [i, j] in ( Indices (M2 - M1));

        then (M1 * (i,j)) <= (M2 * (i,j)) by A1, A2, A4;

        then ((M2 * (i,j)) - (M1 * (i,j))) >= 0 by XREAL_1: 48;

        hence thesis by A4, A5, A3, A6, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:81

    M1 is Nonnegative & M2 is_less_than M3 implies (M2 - M1) is_less_than M3

    proof

      assume

       A1: M1 is Nonnegative & M2 is_less_than M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( Indices M2) = [:( Seg n), ( Seg n):] & ( Indices (M2 - M1)) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A4: ( len M1) = ( len M2) & ( width M1) = ( width M2) by Lm3;

      for i, j st [i, j] in ( Indices (M2 - M1)) holds ((M2 - M1) * (i,j)) < (M3 * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (M2 - M1));

        then (M1 * (i,j)) >= 0 & (M2 * (i,j)) < (M3 * (i,j)) by A1, A2, A3;

        then ((M2 * (i,j)) - (M1 * (i,j))) < (M3 * (i,j)) by XREAL_1: 51;

        hence thesis by A3, A4, A5, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:82

    M1 is Nonpositive & M2 is_less_or_equal_with M3 implies M2 is_less_or_equal_with (M3 - M1)

    proof

      assume

       A1: M1 is Nonpositive & M2 is_less_or_equal_with M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( width M1) = ( width M2) & ( len M2) = ( len M3) by Lm3;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) <= ((M3 - M1) * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M2);

        then (M1 * (i,j)) <= 0 & (M2 * (i,j)) <= (M3 * (i,j)) by A1, A2, A5;

        then (M2 * (i,j)) <= ((M3 * (i,j)) - (M1 * (i,j))) by XREAL_1: 52;

        hence thesis by A5, A6, A4, A3, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:83

    M1 is Nonpositive & M2 is_less_than M3 implies M2 is_less_than (M3 - M1)

    proof

      assume

       A1: M1 is Nonpositive & M2 is_less_than M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( width M1) = ( width M2) & ( len M2) = ( len M3) by Lm3;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M3 - M1) * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M2);

        then (M1 * (i,j)) <= 0 & (M2 * (i,j)) < (M3 * (i,j)) by A1, A2, A5;

        then (M2 * (i,j)) < ((M3 * (i,j)) - (M1 * (i,j))) by XREAL_1: 53;

        hence thesis by A5, A6, A4, A3, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:84

    M1 is Negative & M2 is_less_or_equal_with M3 implies M2 is_less_than (M3 - M1)

    proof

      assume

       A1: M1 is Negative & M2 is_less_or_equal_with M3;

      

       A2: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A3: ( width M2) = ( width M3) by Lm3;

      

       A4: ( width M1) = ( width M2) & ( len M2) = ( len M3) by Lm3;

      

       A5: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       A6: ( Indices M3) = [:( Seg n), ( Seg n):] & ( len M1) = ( len M2) by Lm3, MATRIX_0: 24;

      for i, j st [i, j] in ( Indices M2) holds (M2 * (i,j)) < ((M3 - M1) * (i,j))

      proof

        let i, j;

        assume

         A7: [i, j] in ( Indices M2);

        then (M1 * (i,j)) < 0 & (M2 * (i,j)) <= (M3 * (i,j)) by A1, A2, A5;

        then (M2 * (i,j)) < ((M3 * (i,j)) - (M1 * (i,j))) by XREAL_1: 54;

        hence thesis by A5, A6, A4, A3, A7, Th3;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:85

    M1 is_less_than M2 & a > 0 implies (a * M1) is_less_than (a * M2)

    proof

      assume that

       A1: M1 is_less_than M2 and

       A2: a > 0 ;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) < ((a * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) < (M2 * (i,j)) by A1, A3;

        then (a * (M1 * (i,j))) < (a * (M2 * (i,j))) by A2, XREAL_1: 68;

        then

         A6: ((a * M1) * (i,j)) < (a * (M2 * (i,j))) by A3, A5, Th4;

         [i, j] in ( Indices M2) by A4, A5, MATRIX_0: 24;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:86

    M1 is_less_than M2 & a >= 0 implies (a * M1) is_less_or_equal_with (a * M2)

    proof

      assume that

       A1: M1 is_less_than M2 and

       A2: a >= 0 ;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) <= ((a * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) < (M2 * (i,j)) by A1, A3;

        then (a * (M1 * (i,j))) <= (a * (M2 * (i,j))) by A2, XREAL_1: 64;

        then

         A6: ((a * M1) * (i,j)) <= (a * (M2 * (i,j))) by A3, A5, Th4;

         [i, j] in ( Indices M2) by A4, A5, MATRIX_0: 24;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:87

    M1 is_less_than M2 & a < 0 implies (a * M2) is_less_than (a * M1)

    proof

      assume that

       A1: M1 is_less_than M2 and

       A2: a < 0 ;

      

       A3: ( Indices (a * M2)) = ( Indices M2) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M2)) holds ((a * M2) * (i,j)) < ((a * M1) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M2));

        then

         A6: [i, j] in ( Indices M1) by A4, MATRIX_0: 24;

        then (M1 * (i,j)) < (M2 * (i,j)) by A1;

        then (a * (M2 * (i,j))) < (a * (M1 * (i,j))) by A2, XREAL_1: 69;

        then ((a * M2) * (i,j)) < (a * (M1 * (i,j))) by A3, A5, Th4;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:88

    M1 is_less_than M2 & a <= 0 implies (a * M2) is_less_or_equal_with (a * M1)

    proof

      assume that

       A1: M1 is_less_than M2 and

       A2: a <= 0 ;

      

       A3: ( Indices (a * M2)) = ( Indices M2) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M2)) holds ((a * M2) * (i,j)) <= ((a * M1) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M2));

        then

         A6: [i, j] in ( Indices M1) by A4, MATRIX_0: 24;

        then (M1 * (i,j)) < (M2 * (i,j)) by A1;

        then (a * (M2 * (i,j))) <= (a * (M1 * (i,j))) by A2, XREAL_1: 65;

        then ((a * M2) * (i,j)) <= (a * (M1 * (i,j))) by A3, A5, Th4;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:89

    M1 is_less_or_equal_with M2 & a >= 0 implies (a * M1) is_less_or_equal_with (a * M2)

    proof

      assume that

       A1: M1 is_less_or_equal_with M2 and

       A2: a >= 0 ;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) <= ((a * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) <= (M2 * (i,j)) by A1, A3;

        then (a * (M1 * (i,j))) <= (a * (M2 * (i,j))) by A2, XREAL_1: 64;

        then

         A6: ((a * M1) * (i,j)) <= (a * (M2 * (i,j))) by A3, A5, Th4;

         [i, j] in ( Indices M2) by A4, A5, MATRIX_0: 24;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:90

    M1 is_less_or_equal_with M2 & a <= 0 implies (a * M2) is_less_or_equal_with (a * M1)

    proof

      assume that

       A1: M1 is_less_or_equal_with M2 and

       A2: a <= 0 ;

      

       A3: ( Indices (a * M2)) = ( Indices M2) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M2)) holds ((a * M2) * (i,j)) <= ((a * M1) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M2));

        then

         A6: [i, j] in ( Indices M1) by A4, MATRIX_0: 24;

        then (M1 * (i,j)) <= (M2 * (i,j)) by A1;

        then (a * (M2 * (i,j))) <= (a * (M1 * (i,j))) by A2, XREAL_1: 65;

        then ((a * M2) * (i,j)) <= (a * (M1 * (i,j))) by A3, A5, Th4;

        hence thesis by A6, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:91

    a >= 0 & a <= b & M1 is Nonnegative & M1 is_less_or_equal_with M2 implies (a * M1) is_less_or_equal_with (b * M2)

    proof

      assume that

       A1: a >= 0 & a <= b and

       A2: M1 is Nonnegative & M1 is_less_or_equal_with M2;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) <= ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) >= 0 & (M1 * (i,j)) <= (M2 * (i,j)) by A2, A3;

        then (a * (M1 * (i,j))) <= (b * (M2 * (i,j))) by A1, XREAL_1: 66;

        then ((a * M1) * (i,j)) <= (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:92

    a <= 0 & b <= a & M1 is Nonpositive & M2 is_less_or_equal_with M1 implies (a * M1) is_less_or_equal_with (b * M2)

    proof

      assume that

       A1: a <= 0 & b <= a and

       A2: M1 is Nonpositive & M2 is_less_or_equal_with M1;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) <= ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) <= 0 & (M2 * (i,j)) <= (M1 * (i,j)) by A2, A4, A3;

        then (a * (M1 * (i,j))) <= (b * (M2 * (i,j))) by A1, XREAL_1: 67;

        then ((a * M1) * (i,j)) <= (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:93

    a < 0 & b <= a & M1 is Negative & M2 is_less_than M1 implies (a * M1) is_less_than (b * M2)

    proof

      assume that

       A1: a < 0 & b <= a and

       A2: M1 is Negative & M2 is_less_than M1;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) < ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) < 0 & (M2 * (i,j)) < (M1 * (i,j)) by A2, A4, A3;

        then (a * (M1 * (i,j))) < (b * (M2 * (i,j))) by A1, XREAL_1: 70;

        then ((a * M1) * (i,j)) < (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:94

    a >= 0 & a < b & M1 is Nonnegative & M1 is_less_than M2 implies (a * M1) is_less_than (b * M2)

    proof

      assume that

       A1: a >= 0 & a < b and

       A2: M1 is Nonnegative & M1 is_less_than M2;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) < ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) >= 0 & (M1 * (i,j)) < (M2 * (i,j)) by A2, A3;

        then (a * (M1 * (i,j))) < (b * (M2 * (i,j))) by A1, XREAL_1: 96;

        then ((a * M1) * (i,j)) < (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:95

    a >= 0 & a < b & M1 is Positive & M1 is_less_or_equal_with M2 implies (a * M1) is_less_than (b * M2)

    proof

      assume that

       A1: a >= 0 & a < b and

       A2: M1 is Positive & M1 is_less_or_equal_with M2;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) < ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) > 0 & (M1 * (i,j)) <= (M2 * (i,j)) by A2, A3;

        then (a * (M1 * (i,j))) < (b * (M2 * (i,j))) by A1, XREAL_1: 97;

        then ((a * M1) * (i,j)) < (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;

    theorem :: MATRIX10:96

    a > 0 & a <= b & M1 is Positive & M1 is_less_than M2 implies (a * M1) is_less_than (b * M2)

    proof

      assume that

       A1: a > 0 & a <= b and

       A2: M1 is Positive & M1 is_less_than M2;

      

       A3: ( Indices (a * M1)) = ( Indices M1) by MATRIXR1: 28;

      

       A4: ( Indices M1) = [:( Seg n), ( Seg n):] & ( Indices M2) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i, j st [i, j] in ( Indices (a * M1)) holds ((a * M1) * (i,j)) < ((b * M2) * (i,j))

      proof

        let i, j;

        assume

         A5: [i, j] in ( Indices (a * M1));

        then (M1 * (i,j)) > 0 & (M1 * (i,j)) < (M2 * (i,j)) by A2, A3;

        then (a * (M1 * (i,j))) < (b * (M2 * (i,j))) by A1, XREAL_1: 98;

        then ((a * M1) * (i,j)) < (b * (M2 * (i,j))) by A3, A5, Th4;

        hence thesis by A4, A3, A5, Th4;

      end;

      hence thesis;

    end;