Description: Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | intfrac | ⊢ ( 𝐴 ∈ ℝ → 𝐴 = ( ( ⌊ ‘ 𝐴 ) + ( 𝐴 mod 1 ) ) ) |
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 ) ) ) |