Theorem ceilm1lt

Description: One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceilm1lt	|- ( A e. RR -> ( ( |^ ` A ) - 1 ) < A )

Proof

Step	Hyp	Ref	Expression
1		ceilval	|- ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
2	1	oveq1d	|- ( A e. RR -> ( ( |^ ` A ) - 1 ) = ( -u ( |_ ` -u A ) - 1 ) )
3		ceim1l	|- ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) < A )
4	2 3	eqbrtrd	|- ( A e. RR -> ( ( |^ ` A ) - 1 ) < A )