Description: The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | flmod | ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( 𝐴 − ( 𝐴 mod 1 ) ) ) |
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 ) ) ) |