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 ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) = 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 ( { 𝑥 ∈ ℤ ∣ 𝑥𝐴 } , ℝ , < ) )