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-\left(A\mathrm{mod}1\right)$$

Proof

Step	Hyp	Ref	Expression
1		modfrac	$$⊢A\in ℝ\to A\mathrm{mod}1=A-⌊A⌋$$
2	1	oveq2d	$$⊢A\in ℝ\to A-\left(A\mathrm{mod}1\right)=A-\left(A-⌊A⌋\right)$$
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-\left(A-⌊A⌋\right)=⌊A⌋$$
7	2 6	eqtr2d	$$⊢A\in ℝ\to ⌊A⌋=A-\left(A\mathrm{mod}1\right)$$