let n be Nat; for M being Matrix of n,REAL st M is Positive holds
- M is Negative
let M be Matrix of n,REAL; ( M is Positive implies - M is Negative )
A1:
( Indices M = [:(Seg n),(Seg n):] & Indices (- M) = [:(Seg n),(Seg n):] )
by MATRIX_0:24;
assume A2:
M is Positive
; - M is Negative
for i, j being Nat st [i,j] in Indices (- M) holds
(- M) * (i,j) < 0
proof
let i,
j be
Nat;
( [i,j] in Indices (- M) implies (- M) * (i,j) < 0 )
assume A3:
[i,j] in Indices (- M)
;
(- M) * (i,j) < 0
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
(- M) * (
i,
j)
< 0
by A1, A3, Th2;
verum
end;
hence
- M is Negative
; verum