Metamath Proof Explorer


Theorem modfrac

Description: The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008)

Ref Expression
Assertion modfrac ( 𝐴 ∈ ℝ → ( 𝐴 mod 1 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 1rp 1 ∈ ℝ+
2 modval ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ+ ) → ( 𝐴 mod 1 ) = ( 𝐴 − ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) ) )
3 1 2 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 mod 1 ) = ( 𝐴 − ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) ) )
4 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5 4 div1d ( 𝐴 ∈ ℝ → ( 𝐴 / 1 ) = 𝐴 )
6 5 fveq2d ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 1 ) ) = ( ⌊ ‘ 𝐴 ) )
7 6 oveq2d ( 𝐴 ∈ ℝ → ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) = ( 1 · ( ⌊ ‘ 𝐴 ) ) )
8 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
9 8 recnd ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℂ )
10 9 mulid2d ( 𝐴 ∈ ℝ → ( 1 · ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )
11 7 10 eqtrd ( 𝐴 ∈ ℝ → ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) = ( ⌊ ‘ 𝐴 ) )
12 11 oveq2d ( 𝐴 ∈ ℝ → ( 𝐴 − ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )
13 3 12 eqtrd ( 𝐴 ∈ ℝ → ( 𝐴 mod 1 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )