Metamath Proof Explorer


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 ) ) )