This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flo1

Description: The floor function satisfies |_ ( x ) = x + O(1) . (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion flo1 ( 𝑥 ∈ ℝ ↦ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 ssidd ⊢ ( ⊤ → ℝ ⊆ ℝ )
2 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
3 resubcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ⌊ ‘ 𝑥 ) ∈ ℝ ) → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
4 2 3 mpdan ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
5 4 recnd ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ∈ ℂ )
6 5 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ∈ ℂ )
7 1red ⊢ ( ⊤ → 1 ∈ ℝ )
8 id ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
9 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
10 2 8 9 abssubge0d ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) = ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) )
11 fracle1 ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ≤ 1 )
12 10 11 eqbrtrd ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) ≤ 1 )
13 12 ad2antrl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) ≤ 1 )
14 1 6 7 7 13 elo1d ⊢ ( ⊤ → ( 𝑥 ∈ ℝ ↦ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
15 14 mptru ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ) ∈ 𝑂(1)