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