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=supx∈ℤ|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≤Az≤A
18 brralrspcev ⊢A∈ℝ∧∀z∈x∈ℤ|x≤Az≤A→∃y∈ℝ∀z∈x∈ℤ|x≤Az≤y
19 10 17 18 syl2anc ⊢A∈ℝ→∃y∈ℝ∀z∈x∈ℤ|x≤Az≤y
20 4 9 19 8 suprubd ⊢A∈ℝ→A≤supx∈ℤ|x≤Aℝ<
21 suprleub ⊢x∈ℤ|x≤A⊆ℝ∧x∈ℤ|x≤A≠∅∧∃y∈ℝ∀z∈x∈ℤ|x≤Az≤y∧A∈ℝ→supx∈ℤ|x≤Aℝ<≤A↔∀z∈x∈ℤ|x≤Az≤A
22 4 9 19 10 21 syl31anc ⊢A∈ℝ→supx∈ℤ|x≤Aℝ<≤A↔∀z∈x∈ℤ|x≤Az≤A
23 17 22 mpbird ⊢A∈ℝ→supx∈ℤ|x≤Aℝ<≤A
24 4 9 19 suprcld ⊢A∈ℝ→supx∈ℤ|x≤Aℝ<∈ℝ
25 10 24 letri3d ⊢A∈ℝ→A=supx∈ℤ|x≤Aℝ<↔A≤supx∈ℤ|x≤Aℝ<∧supx∈ℤ|x≤Aℝ<≤A
26 20 23 25 mpbir2and ⊢A∈ℝ→A=supx∈ℤ|x≤Aℝ<