This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zmod10

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

		Ref	Expression
	Assertion	zmod10	$⊢ N \in ℤ \to N \mod 1 = 0$

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