flltnz

Description: The floor of a non-integer real is less than it. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	flltnz	$⊢ (A \in ℝ \land \neg A \in ℤ) \to ⌊A⌋ < A$

Step	Hyp	Ref	Expression
1		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land \neg A \in ℤ) \to ⌊A⌋ \in ℝ$
3		simpl	$⊢ (A \in ℝ \land \neg A \in ℤ) \to A \in ℝ$
4		fllelt	$⊢ A \in ℝ \to (⌊A⌋ \leq A \land A < ⌊A⌋ + 1)$
5	4	adantr	$⊢ (A \in ℝ \land \neg A \in ℤ) \to (⌊A⌋ \leq A \land A < ⌊A⌋ + 1)$
6	5	simpld	$⊢ (A \in ℝ \land \neg A \in ℤ) \to ⌊A⌋ \leq A$
7		simpr	$⊢ (A \in ℝ \land \neg A \in ℤ) \to \neg A \in ℤ$
8		flidz	$⊢ A \in ℝ \to (⌊A⌋ = A \leftrightarrow A \in ℤ)$
9	8	adantr	$⊢ (A \in ℝ \land \neg A \in ℤ) \to (⌊A⌋ = A \leftrightarrow A \in ℤ)$
10	7 9	mtbird	$⊢ (A \in ℝ \land \neg A \in ℤ) \to \neg ⌊A⌋ = A$
11	10	neqned	$⊢ (A \in ℝ \land \neg A \in ℤ) \to ⌊A⌋ \neq A$
12	11	necomd	$⊢ (A \in ℝ \land \neg A \in ℤ) \to A \neq ⌊A⌋$
13	2 3 6 12	leneltd	$⊢ (A \in ℝ \land \neg A \in ℤ) \to ⌊A⌋ < A$

Metamath Proof Explorer