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 ) ) )