This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flval

Description: Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A . (Contributed by NM, 14-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

Ref Expression
Assertion flval ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝐴 ) )
2 breq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 < ( 𝑥 + 1 ) ↔ 𝐴 < ( 𝑥 + 1 ) ) )
3 1 2 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ↔ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) )
4 3 riotabidv ⊢ ( 𝑦 = 𝐴 → ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) )
5 df-fl ⊢ ⌊ = ( 𝑦 ∈ ℝ ↦ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) )
6 riotaex ⊢ ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) ∈ V
7 4 5 6 fvmpt ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℤ ( 𝑥 ≤ 𝐴 ∧ 𝐴 < ( 𝑥 + 1 ) ) ) )