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 ) )
proof
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;
thus ( ( for n, m being Nat st m < n holds
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
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;
thus ( ( for n, m being Nat st m < n holds
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
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;
thus ( ( for n, m being Nat st m <= n holds
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 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;
assume A6: for n, m being Nat st m <= n holds
seq . n <= seq . m ; :: thesis: seq is non-increasing
let e1 be ExtReal; :: according to VALUED_0:def 16 :: thesis: for b1 being object holds
( not e1 in dom seq or not b1 in dom seq or not e1 <= b1 or seq . b1 <= 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