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 ) )