Theorem fllep1

Description: A basic property of the floor (greatest integer) function. (Contributed by Mario Carneiro, 21-May-2016)

	Ref	Expression
Assertion	fllep1	$$⊢A\in ℝ\to A\le ⌊A⌋+1$$

Proof

Step	Hyp	Ref	Expression
1		flltp1	$$⊢A\in ℝ\to A<⌊A⌋+1$$
2		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
3		peano2re	$$⊢⌊A⌋\in ℝ\to ⌊A⌋+1\in ℝ$$
4	2 3	syl	$$⊢A\in ℝ\to ⌊A⌋+1\in ℝ$$
5		ltle	$$⊢\left(A\in ℝ\wedge ⌊A⌋+1\in ℝ\right)\to \left(A<⌊A⌋+1\to A\le ⌊A⌋+1\right)$$
6	4 5	mpdan	$$⊢A\in ℝ\to \left(A<⌊A⌋+1\to A\le ⌊A⌋+1\right)$$
7	1 6	mpd	$$⊢A\in ℝ\to A\le ⌊A⌋+1$$