Metamath Proof Explorer

Theorem flval3

Description: An alternate way to define the floor (greatest integer) 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 ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℤ
2 zssre ⊢ ℤ ⊆ ℝ
3 1 2 sstri ⊢ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ
4 3 a1i ⊢ ( 𝐴 ∈ ℝ → { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ )
5 breq1 ⊢ ( 𝑥 = ( ⌊ ‘ 𝐴 ) → ( 𝑥 ≤ 𝐴 ↔ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) )
6 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
7 flle ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
8 5 6 7 elrabd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } )
9 8 ne0d ⊢ ( 𝐴 ∈ ℝ → { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ≠ ∅ )
10 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
11 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≤ 𝐴 ↔ 𝑧 ≤ 𝐴 ) )
12 11 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ↔ ( 𝑧 ∈ ℤ ∧ 𝑧 ≤ 𝐴 ) )
13 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ≤ 𝐴 ↔ 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
14 13 biimpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ≤ 𝐴 → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
15 14 expimpd ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑧 ∈ ℤ ∧ 𝑧 ≤ 𝐴 ) → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
16 12 15 syl5bi ⊢ ( 𝐴 ∈ ℝ → ( 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } → 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
17 16 ralrimiv ⊢ ( 𝐴 ∈ ℝ → ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) )
18 brralrspcev ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 )
19 10 17 18 syl2anc ⊢ ( 𝐴 ∈ ℝ → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 )
20 4 9 19 8 suprubd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) )
21 suprleub ⊢ ( ( ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ⊆ ℝ ∧ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ 𝑦 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ) → ( sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
22 4 9 19 10 21 syl31anc ⊢ ( 𝐴 ∈ ℝ → ( sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ↔ ∀ 𝑧 ∈ { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } 𝑧 ≤ ( ⌊ ‘ 𝐴 ) ) )
23 17 22 mpbird ⊢ ( 𝐴 ∈ ℝ → sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) )
24 4 9 19 suprcld ⊢ ( 𝐴 ∈ ℝ → sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ∈ ℝ )
25 10 24 letri3d ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ↔ ( ( ⌊ ‘ 𝐴 ) ≤ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ∧ sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) ≤ ( ⌊ ‘ 𝐴 ) ) ) )
26 20 23 25 mpbir2and ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = sup ( { 𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴 } , ℝ , < ) )