flo1

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

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

Step	Hyp	Ref	Expression
1		ssidd	$⊢ ⊤ \to ℝ \subseteq ℝ$
2		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
3		resubcl	$⊢ (x \in ℝ \land ⌊x⌋ \in ℝ) \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	$⊢ (⊤ \land x \in ℝ) \to x - ⌊x⌋ \in ℂ$
7		1red	$⊢ ⊤ \to 1 \in ℝ$
8		id	$⊢ x \in ℝ \to x \in ℝ$
9		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
10	2 8 9	abssubge0d	$⊢ x \in ℝ \to \|x - ⌊x⌋\| = x - ⌊x⌋$
11		fracle1	$⊢ x \in ℝ \to x - ⌊x⌋ \leq 1$
12	10 11	eqbrtrd	$⊢ x \in ℝ \to \|x - ⌊x⌋\| \leq 1$
13	12	ad2antrl	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to \|x - ⌊x⌋\| \leq 1$
14	1 6 7 7 13	elo1d	$⊢ ⊤ \to (x \in ℝ ⟼ x - ⌊x⌋) \in 𝑂 (1)$
15	14	mptru	$⊢ (x \in ℝ ⟼ x - ⌊x⌋) \in 𝑂 (1)$

Metamath Proof Explorer