Theorem zmod10

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

	Ref	Expression
Assertion	zmod10	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 1 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2		modfrac	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 mod 1 ) = ( 𝑁 − ( ⌊ ‘ 𝑁 ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 1 ) = ( 𝑁 − ( ⌊ ‘ 𝑁 ) ) )
4		flid	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
5	4	oveq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − ( ⌊ ‘ 𝑁 ) ) = ( 𝑁 − 𝑁 ) )
6		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7	6	subidd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 𝑁 ) = 0 )
8	3 5 7	3eqtrd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 mod 1 ) = 0 )