fznnfl

Description: Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016)

		Ref	Expression
	Assertion	fznnfl	$⊢ N \in ℝ \to (K \in (1 \dots ⌊N⌋) \leftrightarrow (K \in ℕ \land K \leq N))$

Step	Hyp	Ref	Expression
1		flcl	$⊢ N \in ℝ \to ⌊N⌋ \in ℤ$
2		fznn	$⊢ ⌊N⌋ \in ℤ \to (K \in (1 \dots ⌊N⌋) \leftrightarrow (K \in ℕ \land K \leq ⌊N⌋))$
3	1 2	syl	$⊢ N \in ℝ \to (K \in (1 \dots ⌊N⌋) \leftrightarrow (K \in ℕ \land K \leq ⌊N⌋))$
4		nnz	$⊢ K \in ℕ \to K \in ℤ$
5		flge	$⊢ (N \in ℝ \land K \in ℤ) \to (K \leq N \leftrightarrow K \leq ⌊N⌋)$
6	4 5	sylan2	$⊢ (N \in ℝ \land K \in ℕ) \to (K \leq N \leftrightarrow K \leq ⌊N⌋)$
7	6	pm5.32da	$⊢ N \in ℝ \to ((K \in ℕ \land K \leq N) \leftrightarrow (K \in ℕ \land K \leq ⌊N⌋))$
8	3 7	bitr4d	$⊢ N \in ℝ \to (K \in (1 \dots ⌊N⌋) \leftrightarrow (K \in ℕ \land K \leq N))$

Metamath Proof Explorer