Metamath Proof Explorer


Theorem fllelt

Description: A basic property of the floor (greatest integer) function. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion fllelt ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 flval ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ) )
2 1 eqcomd ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) )
3 flcl ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
4 rebtwnz ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) )
5 breq1 ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥𝐴 ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) )
6 oveq1 ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 + 1 ) = ( ( ⌊ ‘ 𝐴 ) + 1 ) )
7 6 breq2d ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝐴 < ( 𝑥 + 1 ) ↔ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
8 5 7 anbi12d ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ↔ ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
9 8 riota2 ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ ∃! 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ) → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ↔ ( 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) ) )
10 3 4 9 syl2anc ( 𝐴 ∈ ℝ → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ↔ ( 𝑥 ∈ ℤ ( 𝑥𝐴𝐴 < ( 𝑥 + 1 ) ) ) = ( ⌊ ‘ 𝐴 ) ) )
11 2 10 mpbird ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )