Theorem intfrac2

Description: Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac ? (Contributed by NM, 16-Aug-2008)

	Ref	Expression
Hypotheses	intfrac2.1	$$⊢Z=⌊A⌋$$
	intfrac2.2	$$⊢F=A-Z$$
Assertion	intfrac2	$$⊢A\in ℝ\to \left(0\le F\wedge F<1\wedge A=Z+F\right)$$

Proof

Step	Hyp	Ref	Expression
1		intfrac2.1	$$⊢Z=⌊A⌋$$
2		intfrac2.2	$$⊢F=A-Z$$
3		fracge0	$$⊢A\in ℝ\to 0\le A-⌊A⌋$$
4	1	oveq2i	$$⊢A-Z=A-⌊A⌋$$
5	2 4	eqtri	$$⊢F=A-⌊A⌋$$
6	3 5	breqtrrdi	$$⊢A\in ℝ\to 0\le F$$
7		fraclt1	$$⊢A\in ℝ\to A-⌊A⌋<1$$
8	5 7	eqbrtrid	$$⊢A\in ℝ\to F<1$$
9	2	oveq2i	$$⊢Z+F=Z+A-Z$$
10		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
11	1 10	eqeltrid	$$⊢A\in ℝ\to Z\in \mathbb{Z}$$
12	11	zcnd	$$⊢A\in ℝ\to Z\in ℂ$$
13		recn	$$⊢A\in ℝ\to A\in ℂ$$
14	12 13	pncan3d	$$⊢A\in ℝ\to Z+A-Z=A$$
15	9 14	syl5req	$$⊢A\in ℝ\to A=Z+F$$
16	6 8 15	3jca	$$⊢A\in ℝ\to \left(0\le F\wedge F<1\wedge A=Z+F\right)$$