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 )