Metamath Proof Explorer


Theorem fracle1

Description: The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion fracle1 ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ≤ 1 )

Proof

Step Hyp Ref Expression
1 fraclt1 ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 )
2 reflcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3 resubcl ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
4 2 3 mpdan ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
5 1re 1 ∈ ℝ
6 ltle ( ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ≤ 1 ) )
7 4 5 6 sylancl ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) < 1 → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ≤ 1 ) )
8 1 7 mpd ( 𝐴 ∈ ℝ → ( 𝐴 − ( ⌊ ‘ 𝐴 ) ) ≤ 1 )