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	$⊢ A \in ℝ \to ⌊A⌋ = (ι x \in ℤ \| (x \leq A \land A < x + 1))$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ y = A \to (x \leq y \leftrightarrow x \leq A)$
2		breq1	$⊢ y = A \to (y < x + 1 \leftrightarrow A < x + 1)$
3	1 2	anbi12d	$⊢ y = A \to ((x \leq y \land y < x + 1) \leftrightarrow (x \leq A \land A < x + 1))$
4	3	riotabidv	$⊢ y = A \to (ι x \in ℤ \| (x \leq y \land y < x + 1)) = (ι x \in ℤ \| (x \leq A \land A < x + 1))$
5		df-fl	$⊢ ⌊.⌋ = (y \in ℝ ⟼ (ι x \in ℤ \| (x \leq y \land y < x + 1)))$
6		riotaex	$⊢ (ι x \in ℤ \| (x \leq A \land A < x + 1)) \in V$
7	4 5 6	fvmpt	$⊢ A \in ℝ \to ⌊A⌋ = (ι x \in ℤ \| (x \leq A \land A < x + 1))$

Metamath Proof Explorer

Theorem flval

Proof