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	$$⊢A\in ℝ\to A-⌊A⌋\le 1$$

Proof

Step	Hyp	Ref	Expression
1		fraclt1	$$⊢A\in ℝ\to A-⌊A⌋<1$$
2		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
3		resubcl	$$⊢\left(A\in ℝ\wedge ⌊A⌋\in ℝ\right)\to A-⌊A⌋\in ℝ$$
4	2 3	mpdan	$$⊢A\in ℝ\to A-⌊A⌋\in ℝ$$
5		1re	$$⊢1\in ℝ$$
6		ltle	$$⊢\left(A-⌊A⌋\in ℝ\wedge 1\in ℝ\right)\to \left(A-⌊A⌋<1\to A-⌊A⌋\le 1\right)$$
7	4 5 6	sylancl	$$⊢A\in ℝ\to \left(A-⌊A⌋<1\to A-⌊A⌋\le 1\right)$$
8	1 7	mpd	$$⊢A\in ℝ\to A-⌊A⌋\le 1$$