Metamath Proof Explorer

Theorem zmod10

Description: An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion zmod10 
|- ( N e. ZZ -> ( N mod 1 ) = 0 )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 modfrac 
 |-  ( N e. RR -> ( N mod 1 ) = ( N - ( |_ ` N ) ) )
3 1 2 syl 
 |-  ( N e. ZZ -> ( N mod 1 ) = ( N - ( |_ ` N ) ) )
4 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
5 4 oveq2d 
 |-  ( N e. ZZ -> ( N - ( |_ ` N ) ) = ( N - N ) )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 6 subidd 
 |-  ( N e. ZZ -> ( N - N ) = 0 )
8 3 5 7 3eqtrd 
 |-  ( N e. ZZ -> ( N mod 1 ) = 0 )