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