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	⊢ 𝑍 = ( ⌊ ‘ 𝐴 )
	intfrac2.2	⊢ 𝐹 = ( 𝐴 − 𝑍 )
Assertion	intfrac2	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = ( 𝑍 + 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		intfrac2.1	⊢ 𝑍 = ( ⌊ ‘ 𝐴 )
2		intfrac2.2	⊢ 𝐹 = ( 𝐴 − 𝑍 )
3		fracge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )
4	1	oveq2i	⊢ ( 𝐴 − 𝑍 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) )
5	2 4	eqtri	⊢ 𝐹 = ( 𝐴 − ( ⌊ ‘ 𝐴 ) )
6	3 5	breqtrrdi	⊢ ( 𝐴 ∈ ℝ → 0 ≤ 𝐹 )
7		fraclt1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )
8	5 7	eqbrtrid	⊢ ( 𝐴 ∈ ℝ → 𝐹 < 1 )
9	2	oveq2i	⊢ ( 𝑍 + 𝐹 ) = ( 𝑍 + ( 𝐴 − 𝑍 ) )
10		flcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
11	1 10	eqeltrid	⊢ ( 𝐴 ∈ ℝ → 𝑍 ∈ ℤ )
12	11	zcnd	⊢ ( 𝐴 ∈ ℝ → 𝑍 ∈ ℂ )
13		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
14	12 13	pncan3d	⊢ ( 𝐴 ∈ ℝ → ( 𝑍 + ( 𝐴 − 𝑍 ) ) = 𝐴 )
15	9 14	syl5req	⊢ ( 𝐴 ∈ ℝ → 𝐴 = ( 𝑍 + 𝐹 ) )
16	6 8 15	3jca	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = ( 𝑍 + 𝐹 ) ) )