Theorem flo1

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

	Ref	Expression
Assertion	flo1	$$⊢\left(x\in ℝ⟼x-⌊x⌋\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssidd	$$⊢\top \to ℝ\subseteq ℝ$$
2		reflcl	$$⊢x\in ℝ\to ⌊x⌋\in ℝ$$
3		resubcl	$$⊢\left(x\in ℝ\wedge ⌊x⌋\in ℝ\right)\to x-⌊x⌋\in ℝ$$
4	2 3	mpdan	$$⊢x\in ℝ\to x-⌊x⌋\in ℝ$$
5	4	recnd	$$⊢x\in ℝ\to x-⌊x⌋\in ℂ$$
6	5	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to x-⌊x⌋\in ℂ$$
7		1red	$$⊢\top \to 1\in ℝ$$
8		id	$$⊢x\in ℝ\to x\in ℝ$$
9		flle	$$⊢x\in ℝ\to ⌊x⌋\le x$$
10	2 8 9	abssubge0d	$$⊢x\in ℝ\to \left|x-⌊x⌋\right|=x-⌊x⌋$$
11		fracle1	$$⊢x\in ℝ\to x-⌊x⌋\le 1$$
12	10 11	eqbrtrd	$$⊢x\in ℝ\to \left|x-⌊x⌋\right|\le 1$$
13	12	ad2antrl	$$⊢\left(\top \wedge \left(x\in ℝ\wedge 1\le x\right)\right)\to \left|x-⌊x⌋\right|\le 1$$
14	1 6 7 7 13	elo1d	$$⊢\top \to \left(x\in ℝ⟼x-⌊x⌋\right)\in 𝑂\left(1\right)$$
15	14	mptru	$$⊢\left(x\in ℝ⟼x-⌊x⌋\right)\in 𝑂\left(1\right)$$