Metamath Proof Explorer


Theorem intfrac

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

Ref Expression
Assertion intfrac ( 𝐴 ∈ ℝ → 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 mod 1 ) ) )

Proof

Step Hyp Ref Expression
1 modfrac ( 𝐴 ∈ ℝ → ( 𝐴 mod 1 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )
2 1 oveq2d ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 mod 1 ) ) = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) )
3 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
4 3 recnd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
5 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6 4 5 pncan3d ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ) = 𝐴 )
7 2 6 eqtr2d ( 𝐴 ∈ ℝ → 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 mod 1 ) ) )