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)