Metamath Proof Explorer


Theorem flmod

Description: The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008)

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

Proof

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