This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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