Metamath Proof Explorer

Theorem flval2

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

Ref Expression
Assertion flval2 ⊢ A ∈ ℝ → A = ι x ∈ ℤ | x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x

Proof

Step Hyp Ref Expression
1 flle ⊢ A ∈ ℝ → A ≤ A
2 flge ⊢ A ∈ ℝ ∧ y ∈ ℤ → y ≤ A ↔ y ≤ A
3 2 biimpd ⊢ A ∈ ℝ ∧ y ∈ ℤ → y ≤ A → y ≤ A
4 3 ralrimiva ⊢ A ∈ ℝ → ∀ y ∈ ℤ y ≤ A → y ≤ A
5 flcl ⊢ A ∈ ℝ → A ∈ ℤ
6 zmax ⊢ A ∈ ℝ → ∃! x ∈ ℤ x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x
7 breq1 ⊢ x = A → x ≤ A ↔ A ≤ A
8 breq2 ⊢ x = A → y ≤ x ↔ y ≤ A
9 8 imbi2d ⊢ x = A → y ≤ A → y ≤ x ↔ y ≤ A → y ≤ A
10 9 ralbidv ⊢ x = A → ∀ y ∈ ℤ y ≤ A → y ≤ x ↔ ∀ y ∈ ℤ y ≤ A → y ≤ A
11 7 10 anbi12d ⊢ x = A → x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x ↔ A ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ A
12 11 riota2 ⊢ A ∈ ℤ ∧ ∃! x ∈ ℤ x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x → A ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ A ↔ ι x ∈ ℤ | x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x = A
13 5 6 12 syl2anc ⊢ A ∈ ℝ → A ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ A ↔ ι x ∈ ℤ | x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x = A
14 1 4 13 mpbi2and ⊢ A ∈ ℝ → ι x ∈ ℤ | x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x = A
15 14 eqcomd ⊢ A ∈ ℝ → A = ι x ∈ ℤ | x ≤ A ∧ ∀ y ∈ ℤ y ≤ A → y ≤ x