Theorem intfrac

Description: Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008)

	Ref	Expression
Assertion	intfrac	$$⊢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⌋+A-⌊A⌋$$
3		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
4	3	recnd	$$⊢A\in ℝ\to ⌊A⌋\in ℂ$$
5		recn	$$⊢A\in ℝ\to A\in ℂ$$
6	4 5	pncan3d	$$⊢A\in ℝ\to ⌊A⌋+A-⌊A⌋=A$$
7	2 6	eqtr2d	$$⊢A\in ℝ\to A=⌊A⌋+\left(A\mathrm{mod}1\right)$$