Theorem ceilval

Description: The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015)

	Ref	Expression
Assertion	ceilval	|- ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )

Proof

Step	Hyp	Ref	Expression
1		negeq	|- ( x = A -> -u x = -u A )
2	1	fveq2d	|- ( x = A -> ( |_ ` -u x ) = ( |_ ` -u A ) )
3	2	negeqd	|- ( x = A -> -u ( |_ ` -u x ) = -u ( |_ ` -u A ) )
4		df-ceil	|- |^ = ( x e. RR |-> -u ( |_ ` -u x ) )
5		negex	|- -u ( |_ ` -u A ) e. _V
6	3 4 5	fvmpt	|- ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )