This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceige

Description: The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007)

Ref Expression
Assertion ceige 
|- ( A e. RR -> A <_ -u ( |_ ` -u A ) )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 reflcl 
 |-  ( -u A e. RR -> ( |_ ` -u A ) e. RR )
3 1 2 syl 
 |-  ( A e. RR -> ( |_ ` -u A ) e. RR )
4 flle 
 |-  ( -u A e. RR -> ( |_ ` -u A ) <_ -u A )
5 1 4 syl 
 |-  ( A e. RR -> ( |_ ` -u A ) <_ -u A )
6 5 adantr 
 |-  ( ( A e. RR /\ ( |_ ` -u A ) e. RR ) -> ( |_ ` -u A ) <_ -u A )
7 lenegcon2 
 |-  ( ( A e. RR /\ ( |_ ` -u A ) e. RR ) -> ( A <_ -u ( |_ ` -u A ) <-> ( |_ ` -u A ) <_ -u A ) )
8 6 7 mpbird 
 |-  ( ( A e. RR /\ ( |_ ` -u A ) e. RR ) -> A <_ -u ( |_ ` -u A ) )
9 3 8 mpdan 
 |-  ( A e. RR -> A <_ -u ( |_ ` -u A ) )