Metamath Proof Explorer

Theorem flval3

Description: An alternate way to define the floor function, as the supremum of all integers less than or equal to its argument. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion flval3 ⊢ A ∈ ℝ → A = sup x ∈ ℤ | x ≤ A ℝ <

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ x ∈ ℤ | x ≤ A ⊆ ℤ
2 zssre ⊢ ℤ ⊆ ℝ
3 1 2 sstri ⊢ x ∈ ℤ | x ≤ A ⊆ ℝ
4 3 a1i ⊢ A ∈ ℝ → x ∈ ℤ | x ≤ A ⊆ ℝ
5 breq1 ⊢ x = A → x ≤ A ↔ A ≤ A
6 flcl ⊢ A ∈ ℝ → A ∈ ℤ
7 flle ⊢ A ∈ ℝ → A ≤ A
8 5 6 7 elrabd ⊢ A ∈ ℝ → A ∈ x ∈ ℤ | x ≤ A
9 8 ne0d ⊢ A ∈ ℝ → x ∈ ℤ | x ≤ A ≠ ∅
10 reflcl ⊢ A ∈ ℝ → A ∈ ℝ
11 breq1 ⊢ x = z → x ≤ A ↔ z ≤ A
12 11 elrab ⊢ z ∈ x ∈ ℤ | x ≤ A ↔ z ∈ ℤ ∧ z ≤ A
13 flge ⊢ A ∈ ℝ ∧ z ∈ ℤ → z ≤ A ↔ z ≤ A
14 13 biimpd ⊢ A ∈ ℝ ∧ z ∈ ℤ → z ≤ A → z ≤ A
15 14 expimpd ⊢ A ∈ ℝ → z ∈ ℤ ∧ z ≤ A → z ≤ A
16 12 15 biimtrid ⊢ A ∈ ℝ → z ∈ x ∈ ℤ | x ≤ A → z ≤ A
17 16 ralrimiv ⊢ A ∈ ℝ → ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ A
18 brralrspcev ⊢ A ∈ ℝ ∧ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ A → ∃ y ∈ ℝ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ y
19 10 17 18 syl2anc ⊢ A ∈ ℝ → ∃ y ∈ ℝ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ y
20 4 9 19 8 suprubd ⊢ A ∈ ℝ → A ≤ sup x ∈ ℤ | x ≤ A ℝ <
21 suprleub ⊢ x ∈ ℤ | x ≤ A ⊆ ℝ ∧ x ∈ ℤ | x ≤ A ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ y ∧ A ∈ ℝ → sup x ∈ ℤ | x ≤ A ℝ < ≤ A ↔ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ A
22 4 9 19 10 21 syl31anc ⊢ A ∈ ℝ → sup x ∈ ℤ | x ≤ A ℝ < ≤ A ↔ ∀ z ∈ x ∈ ℤ | x ≤ A z ≤ A
23 17 22 mpbird ⊢ A ∈ ℝ → sup x ∈ ℤ | x ≤ A ℝ < ≤ A
24 4 9 19 suprcld ⊢ A ∈ ℝ → sup x ∈ ℤ | x ≤ A ℝ < ∈ ℝ
25 10 24 letri3d ⊢ A ∈ ℝ → A = sup x ∈ ℤ | x ≤ A ℝ < ↔ A ≤ sup x ∈ ℤ | x ≤ A ℝ < ∧ sup x ∈ ℤ | x ≤ A ℝ < ≤ A
26 20 23 25 mpbir2and ⊢ A ∈ ℝ → A = sup x ∈ ℤ | x ≤ A ℝ <