Theorem 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 e. RR -> ( K e. ( 1 ... ( |_ ` N ) ) <-> ( K e. NN /\ K <_ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		flcl	|- ( N e. RR -> ( |_ ` N ) e. ZZ )
2		fznn	|- ( ( |_ ` N ) e. ZZ -> ( K e. ( 1 ... ( |_ ` N ) ) <-> ( K e. NN /\ K <_ ( |_ ` N ) ) ) )
3	1 2	syl	|- ( N e. RR -> ( K e. ( 1 ... ( |_ ` N ) ) <-> ( K e. NN /\ K <_ ( |_ ` N ) ) ) )
4		nnz	|- ( K e. NN -> K e. ZZ )
5		flge	|- ( ( N e. RR /\ K e. ZZ ) -> ( K <_ N <-> K <_ ( |_ ` N ) ) )
6	4 5	sylan2	|- ( ( N e. RR /\ K e. NN ) -> ( K <_ N <-> K <_ ( |_ ` N ) ) )
7	6	pm5.32da	|- ( N e. RR -> ( ( K e. NN /\ K <_ N ) <-> ( K e. NN /\ K <_ ( |_ ` N ) ) ) )
8	3 7	bitr4d	|- ( N e. RR -> ( K e. ( 1 ... ( |_ ` N ) ) <-> ( K e. NN /\ K <_ N ) ) )