Metamath Proof Explorer

Theorem ceilid

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

Ref Expression
Assertion ceilid 
|- ( A e. ZZ -> ( |^ ` A ) = A )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 ceilval 
 |-  ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
3 1 2 syl 
 |-  ( A e. ZZ -> ( |^ ` A ) = -u ( |_ ` -u A ) )
4 znegcl 
 |-  ( A e. ZZ -> -u A e. ZZ )
5 flid 
 |-  ( -u A e. ZZ -> ( |_ ` -u A ) = -u A )
6 4 5 syl 
 |-  ( A e. ZZ -> ( |_ ` -u A ) = -u A )
7 6 negeqd 
 |-  ( A e. ZZ -> -u ( |_ ` -u A ) = -u -u A )
8 zcn 
 |-  ( A e. ZZ -> A e. CC )
9 8 negnegd 
 |-  ( A e. ZZ -> -u -u A = A )
10 3 7 9 3eqtrd 
 |-  ( A e. ZZ -> ( |^ ` A ) = A )