Theorem modfrac

Description: The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008)

	Ref	Expression
Assertion	modfrac	$$⊢A\in ℝ\to A\mathrm{mod}1=A-⌊A⌋$$

Proof

Step	Hyp	Ref	Expression
1		1rp	$$⊢1\in {ℝ}^{+}$$
2		modval	$$⊢\left(A\in ℝ\wedge 1\in {ℝ}^{+}\right)\to A\mathrm{mod}1=A-1⌊\frac{A}{1}⌋$$
3	1 2	mpan2	$$⊢A\in ℝ\to A\mathrm{mod}1=A-1⌊\frac{A}{1}⌋$$
4		recn	$$⊢A\in ℝ\to A\in ℂ$$
5	4	div1d	$$⊢A\in ℝ\to \frac{A}{1}=A$$
6	5	fveq2d	$$⊢A\in ℝ\to ⌊\frac{A}{1}⌋=⌊A⌋$$
7	6	oveq2d	$$⊢A\in ℝ\to 1⌊\frac{A}{1}⌋=1⌊A⌋$$
8		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
9	8	recnd	$$⊢A\in ℝ\to ⌊A⌋\in ℂ$$
10	9	mullidd	$$⊢A\in ℝ\to 1⌊A⌋=⌊A⌋$$
11	7 10	eqtrd	$$⊢A\in ℝ\to 1⌊\frac{A}{1}⌋=⌊A⌋$$
12	11	oveq2d	$$⊢A\in ℝ\to A-1⌊\frac{A}{1}⌋=A-⌊A⌋$$
13	3 12	eqtrd	$$⊢A\in ℝ\to A\mathrm{mod}1=A-⌊A⌋$$