Metamath Proof Explorer

Theorem flval2

Description: An alternate way to define the floor function. (Contributed by NM, 16-Nov-2004)

		Ref	Expression
	Assertion	flval2	$⊢ A \in ℝ \to ⌊A⌋ = (ι x \in ℤ \| (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x)))$

Proof

Step	Hyp	Ref	Expression
1		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
2		flge	$⊢ (A \in ℝ \land y \in ℤ) \to (y \leq A \leftrightarrow y \leq ⌊A⌋)$
3	2	biimpd	$⊢ (A \in ℝ \land y \in ℤ) \to (y \leq A \to y \leq ⌊A⌋)$
4	3	ralrimiva	$⊢ A \in ℝ \to \forall y \in ℤ (y \leq A \to y \leq ⌊A⌋)$
5		flcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℤ$
6		zmax	$⊢ A \in ℝ \to \exists! x \in ℤ (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x))$
7		breq1	$⊢ x = ⌊A⌋ \to (x \leq A \leftrightarrow ⌊A⌋ \leq A)$
8		breq2	$⊢ x = ⌊A⌋ \to (y \leq x \leftrightarrow y \leq ⌊A⌋)$
9	8	imbi2d	$⊢ x = ⌊A⌋ \to ((y \leq A \to y \leq x) \leftrightarrow (y \leq A \to y \leq ⌊A⌋))$
10	9	ralbidv	$⊢ x = ⌊A⌋ \to (\forall y \in ℤ (y \leq A \to y \leq x) \leftrightarrow \forall y \in ℤ (y \leq A \to y \leq ⌊A⌋))$
11	7 10	anbi12d	$⊢ x = ⌊A⌋ \to ((x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x)) \leftrightarrow (⌊A⌋ \leq A \land \forall y \in ℤ (y \leq A \to y \leq ⌊A⌋)))$
12	11	riota2	$⊢ (⌊A⌋ \in ℤ \land \exists! x \in ℤ (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x))) \to ((⌊A⌋ \leq A \land \forall y \in ℤ (y \leq A \to y \leq ⌊A⌋)) \leftrightarrow (ι x \in ℤ \| (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x))) = ⌊A⌋)$
13	5 6 12	syl2anc	$⊢ A \in ℝ \to ((⌊A⌋ \leq A \land \forall y \in ℤ (y \leq A \to y \leq ⌊A⌋)) \leftrightarrow (ι x \in ℤ \| (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x))) = ⌊A⌋)$
14	1 4 13	mpbi2and	$⊢ A \in ℝ \to (ι x \in ℤ \| (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x))) = ⌊A⌋$
15	14	eqcomd	$⊢ A \in ℝ \to ⌊A⌋ = (ι x \in ℤ \| (x \leq A \land \forall y \in ℤ (y \leq A \to y \leq x)))$