Theorem ceilid

Description: An integer is its own ceiling. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	ceilid	⊢ ( 𝐴 ∈ ℤ → ( ⌈ ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2		ceilval	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℤ → ( ⌈ ‘ 𝐴 ) = - ( ⌊ ‘ - 𝐴 ) )
4		znegcl	⊢ ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
5		flid	⊢ ( - 𝐴 ∈ ℤ → ( ⌊ ‘ - 𝐴 ) = - 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ - 𝐴 ) = - 𝐴 )
7	6	negeqd	⊢ ( 𝐴 ∈ ℤ → - ( ⌊ ‘ - 𝐴 ) = - - 𝐴 )
8		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
9	8	negnegd	⊢ ( 𝐴 ∈ ℤ → - - 𝐴 = 𝐴 )
10	3 7 9	3eqtrd	⊢ ( 𝐴 ∈ ℤ → ( ⌈ ‘ 𝐴 ) = 𝐴 )