Theorem ceilval

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

	Ref	Expression
Assertion	ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negeq	⊢ ( 𝑥 = 𝐴 → - 𝑥 = - 𝐴 )
2	1	fveq2d	⊢ ( 𝑥 = 𝐴 → ( ⌊ ‘ - 𝑥 ) = ( ⌊ ‘ - 𝐴 ) )
3	2	negeqd	⊢ ( 𝑥 = 𝐴 → - ( ⌊ ‘ - 𝑥 ) = - ( ⌊ ‘ - 𝐴 ) )
4		df-ceil	⊢ ⌈ = ( 𝑥 ∈ ℝ ↦ - ( ⌊ ‘ - 𝑥 ) )
5		negex	⊢ - ( ⌊ ‘ - 𝐴 ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )