Theorem ceilval

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

	Ref	Expression
Assertion	ceilval	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$

Proof

Step	Hyp	Ref	Expression
1		negeq	$$⊢x=A\to -x=-A$$
2	1	fveq2d	$$⊢x=A\to ⌊-x⌋=⌊-A⌋$$
3	2	negeqd	$$⊢x=A\to -⌊-x⌋=-⌊-A⌋$$
4		df-ceil	$$⊢⌈.⌉=\left(x\in ℝ⟼-⌊-x⌋\right)$$
5		negex	$$⊢-⌊-A⌋\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in ℝ\to ⌈A⌉=-⌊-A⌋$$