fllt

Description: The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005)

		Ref	Expression
	Assertion	fllt	$⊢ (A \in ℝ \land B \in ℤ) \to (A < B \leftrightarrow ⌊A⌋ < B)$

Step	Hyp	Ref	Expression
1		flge	$⊢ (A \in ℝ \land B \in ℤ) \to (B \leq A \leftrightarrow B \leq ⌊A⌋)$
2		zre	$⊢ B \in ℤ \to B \in ℝ$
3		lenlt	$⊢ (B \in ℝ \land A \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
4	2 3	sylan	$⊢ (B \in ℤ \land A \in ℝ) \to (B \leq A \leftrightarrow \neg A < B)$
5	4	ancoms	$⊢ (A \in ℝ \land B \in ℤ) \to (B \leq A \leftrightarrow \neg A < B)$
6		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
7		lenlt	$⊢ (B \in ℝ \land ⌊A⌋ \in ℝ) \to (B \leq ⌊A⌋ \leftrightarrow \neg ⌊A⌋ < B)$
8	2 6 7	syl2anr	$⊢ (A \in ℝ \land B \in ℤ) \to (B \leq ⌊A⌋ \leftrightarrow \neg ⌊A⌋ < B)$
9	1 5 8	3bitr3d	$⊢ (A \in ℝ \land B \in ℤ) \to (\neg A < B \leftrightarrow \neg ⌊A⌋ < B)$
10	9	con4bid	$⊢ (A \in ℝ \land B \in ℤ) \to (A < B \leftrightarrow ⌊A⌋ < B)$

Metamath Proof Explorer