flbi2

Description: A condition equivalent to floor. (Contributed by NM, 15-Aug-2008)

		Ref	Expression
	Assertion	flbi2	$⊢ (N \in ℤ \land F \in ℝ) \to (⌊N + F⌋ = N \leftrightarrow (0 \leq F \land F < 1))$

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2		readdcl	$⊢ (N \in ℝ \land F \in ℝ) \to N + F \in ℝ$
3	1 2	sylan	$⊢ (N \in ℤ \land F \in ℝ) \to N + F \in ℝ$
4		simpl	$⊢ (N \in ℤ \land F \in ℝ) \to N \in ℤ$
5		flbi	$⊢ (N + F \in ℝ \land N \in ℤ) \to (⌊N + F⌋ = N \leftrightarrow (N \leq N + F \land N + F < N + 1))$
6	3 4 5	syl2anc	$⊢ (N \in ℤ \land F \in ℝ) \to (⌊N + F⌋ = N \leftrightarrow (N \leq N + F \land N + F < N + 1))$
7		addge01	$⊢ (N \in ℝ \land F \in ℝ) \to (0 \leq F \leftrightarrow N \leq N + F)$
8		1re	$⊢ 1 \in ℝ$
9		ltadd2	$⊢ (F \in ℝ \land 1 \in ℝ \land N \in ℝ) \to (F < 1 \leftrightarrow N + F < N + 1)$
10	8 9	mp3an2	$⊢ (F \in ℝ \land N \in ℝ) \to (F < 1 \leftrightarrow N + F < N + 1)$
11	10	ancoms	$⊢ (N \in ℝ \land F \in ℝ) \to (F < 1 \leftrightarrow N + F < N + 1)$
12	7 11	anbi12d	$⊢ (N \in ℝ \land F \in ℝ) \to ((0 \leq F \land F < 1) \leftrightarrow (N \leq N + F \land N + F < N + 1))$
13	1 12	sylan	$⊢ (N \in ℤ \land F \in ℝ) \to ((0 \leq F \land F < 1) \leftrightarrow (N \leq N + F \land N + F < N + 1))$
14	6 13	bitr4d	$⊢ (N \in ℤ \land F \in ℝ) \to (⌊N + F⌋ = N \leftrightarrow (0 \leq F \land F < 1))$

Metamath Proof Explorer