let seq be ExtREAL_sequence; :: thesis: ( ( seq is increasing implies for n, m being Nat st m < n holds

seq . m < seq . n ) & ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

A1: dom seq = NAT by FUNCT_2:def 1;

thus ( seq is increasing implies for n, m being Nat st m < n holds

seq . m < seq . n ) :: thesis: ( ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

seq . m < seq . n ) implies seq is increasing ) ; :: thesis: ( ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

thus ( seq is decreasing implies for n, m being Nat st m < n holds

seq . m > seq . n ) :: thesis: ( ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

seq . n < seq . m ) implies seq is decreasing ) ; :: thesis: ( ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

thus ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) :: thesis: ( ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

seq . m <= seq . n ) implies seq is non-decreasing ) ; :: thesis: ( seq is non-increasing iff for n, m being Nat st m <= n holds

seq . n <= seq . m )

thus ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . m >= seq . n ) :: thesis: ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing )

seq . n <= seq . m ; :: thesis: seq is non-increasing

let e1 be ExtReal; :: according to VALUED_0:def 16 :: thesis: for b_{1} being object holds

( not e1 in dom seq or not b_{1} in dom seq or not e1 <= b_{1} or seq . b_{1} <= seq . e1 )

let e2 be ExtReal; :: thesis: ( not e1 in dom seq or not e2 in dom seq or not e1 <= e2 or seq . e2 <= seq . e1 )

thus ( not e1 in dom seq or not e2 in dom seq or not e1 <= e2 or seq . e2 <= seq . e1 ) by A6; :: thesis: verum

seq . m < seq . n ) & ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

A1: dom seq = NAT by FUNCT_2:def 1;

thus ( seq is increasing implies for n, m being Nat st m < n holds

seq . m < seq . n ) :: thesis: ( ( ( for n, m being Nat st m < n holds

seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

proof

thus
( ( for n, m being Nat st m < n holds
assume A2:
seq is increasing
; :: thesis: for n, m being Nat st m < n holds

seq . m < seq . n

let n, m be Nat; :: thesis: ( m < n implies seq . m < seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m < n implies seq . m < seq . n ) by A2, A1; :: thesis: verum

end;seq . m < seq . n

let n, m be Nat; :: thesis: ( m < n implies seq . m < seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m < n implies seq . m < seq . n ) by A2, A1; :: thesis: verum

seq . m < seq . n ) implies seq is increasing ) ; :: thesis: ( ( seq is decreasing implies for n, m being Nat st m < n holds

seq . n < seq . m ) & ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

thus ( seq is decreasing implies for n, m being Nat st m < n holds

seq . m > seq . n ) :: thesis: ( ( ( for n, m being Nat st m < n holds

seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

proof

thus
( ( for n, m being Nat st m < n holds
assume A3:
seq is decreasing
; :: thesis: for n, m being Nat st m < n holds

seq . m > seq . n

let n, m be Nat; :: thesis: ( m < n implies seq . m > seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m < n implies seq . m > seq . n ) by A3, A1; :: thesis: verum

end;seq . m > seq . n

let n, m be Nat; :: thesis: ( m < n implies seq . m > seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m < n implies seq . m > seq . n ) by A3, A1; :: thesis: verum

seq . n < seq . m ) implies seq is decreasing ) ; :: thesis: ( ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) & ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

thus ( seq is non-decreasing implies for n, m being Nat st m <= n holds

seq . m <= seq . n ) :: thesis: ( ( ( for n, m being Nat st m <= n holds

seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . n <= seq . m ) & ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing ) )

proof

thus
( ( for n, m being Nat st m <= n holds
assume A4:
seq is non-decreasing
; :: thesis: for n, m being Nat st m <= n holds

seq . m <= seq . n

let n, m be Nat; :: thesis: ( m <= n implies seq . m <= seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m <= n implies seq . m <= seq . n ) by A4, A1; :: thesis: verum

end;seq . m <= seq . n

let n, m be Nat; :: thesis: ( m <= n implies seq . m <= seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m <= n implies seq . m <= seq . n ) by A4, A1; :: thesis: verum

seq . m <= seq . n ) implies seq is non-decreasing ) ; :: thesis: ( seq is non-increasing iff for n, m being Nat st m <= n holds

seq . n <= seq . m )

thus ( seq is non-increasing implies for n, m being Nat st m <= n holds

seq . m >= seq . n ) :: thesis: ( ( for n, m being Nat st m <= n holds

seq . n <= seq . m ) implies seq is non-increasing )

proof

assume A6:
for n, m being Nat st m <= n holds
assume A5:
seq is non-increasing
; :: thesis: for n, m being Nat st m <= n holds

seq . m >= seq . n

let n, m be Nat; :: thesis: ( m <= n implies seq . m >= seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m <= n implies seq . m >= seq . n ) by A5, A1; :: thesis: verum

end;seq . m >= seq . n

let n, m be Nat; :: thesis: ( m <= n implies seq . m >= seq . n )

( n in NAT & m in NAT ) by ORDINAL1:def 12;

hence ( m <= n implies seq . m >= seq . n ) by A5, A1; :: thesis: verum

seq . n <= seq . m ; :: thesis: seq is non-increasing

let e1 be ExtReal; :: according to VALUED_0:def 16 :: thesis: for b

( not e1 in dom seq or not b

let e2 be ExtReal; :: thesis: ( not e1 in dom seq or not e2 in dom seq or not e1 <= e2 or seq . e2 <= seq . e1 )

thus ( not e1 in dom seq or not e2 in dom seq or not e1 <= e2 or seq . e2 <= seq . e1 ) by A6; :: thesis: verum