This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceilval

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

Ref Expression
Assertion ceilval ⊢ A ∈ ℝ → A = − − A

Proof

Step Hyp Ref Expression
1 negeq ⊢ x = A → − x = − A
2 1 fveq2d ⊢ x = A → − x = − A
3 2 negeqd ⊢ x = A → − − x = − − A
4 df-ceil ⊢ . = x ∈ ℝ ⟼ − − x
5 negex ⊢ − − A ∈ V
6 3 4 5 fvmpt ⊢ A ∈ ℝ → A = − − A