Metamath Proof Explorer

Theorem flidz

Description: A real number equals its floor iff it is an integer. (Contributed by NM, 11-Nov-2008)

		Ref	Expression
	Assertion	flidz	$⊢ A \in ℝ \to (⌊A⌋ = A \leftrightarrow A \in ℤ)$

Step	Hyp	Ref	Expression
1		flcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℤ$
2		eleq1	$⊢ ⌊A⌋ = A \to (⌊A⌋ \in ℤ \leftrightarrow A \in ℤ)$
3	1 2	syl5ibcom	$⊢ A \in ℝ \to (⌊A⌋ = A \to A \in ℤ)$
4		flid	$⊢ A \in ℤ \to ⌊A⌋ = A$
5	3 4	impbid1	$⊢ A \in ℝ \to (⌊A⌋ = A \leftrightarrow A \in ℤ)$