Theorem fllep1

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

	Ref	Expression
Assertion	fllep1	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		flltp1	⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )
2		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3		peano2re	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
4	2 3	syl	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
5		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ ) → ( 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
6	4 5	mpdan	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
7	1 6	mpd	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )