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

Metamath Proof Explorer

Theorem flmod

Description: The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008)

		Ref	Expression
	Assertion	flmod	$⊢ A \in ℝ \to ⌊A⌋ = A - (A \mod 1)$

Step	Hyp	Ref	Expression
1		modfrac	$⊢ A \in ℝ \to A \mod 1 = A - ⌊A⌋$
2	1	oveq2d	$⊢ A \in ℝ \to A - (A \mod 1) = A - (A - ⌊A⌋)$
3		recn	$⊢ A \in ℝ \to A \in ℂ$
4		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
5	4	recnd	$⊢ A \in ℝ \to ⌊A⌋ \in ℂ$
6	3 5	nncand	$⊢ A \in ℝ \to A - (A - ⌊A⌋) = ⌊A⌋$
7	2 6	eqtr2d	$⊢ A \in ℝ \to ⌊A⌋ = A - (A \mod 1)$