Theorem zmod10

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

	Ref	Expression
Assertion	zmod10	$$⊢N\in \mathbb{Z}\to N\mathrm{mod}1=0$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
2		modfrac	$$⊢N\in ℝ\to N\mathrm{mod}1=N-⌊N⌋$$
3	1 2	syl	$$⊢N\in \mathbb{Z}\to N\mathrm{mod}1=N-⌊N⌋$$
4		flid	$$⊢N\in \mathbb{Z}\to ⌊N⌋=N$$
5	4	oveq2d	$$⊢N\in \mathbb{Z}\to N-⌊N⌋=N-N$$
6		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
7	6	subidd	$$⊢N\in \mathbb{Z}\to N-N=0$$
8	3 5 7	3eqtrd	$$⊢N\in \mathbb{Z}\to N\mathrm{mod}1=0$$