This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mullidd ⊢ ( 𝐴 ∈ ℝ → ( 1 · ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )
11 7 10 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) = ( ⌊ ‘ 𝐴 ) )
12 11 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( 1 · ( ⌊ ‘ ( 𝐴 / 1 ) ) ) ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )
13 3 12 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 mod 1 ) = ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) )