Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
2 |
|
readdcl |
|- ( ( N e. RR /\ F e. RR ) -> ( N + F ) e. RR ) |
3 |
1 2
|
sylan |
|- ( ( N e. ZZ /\ F e. RR ) -> ( N + F ) e. RR ) |
4 |
|
simpl |
|- ( ( N e. ZZ /\ F e. RR ) -> N e. ZZ ) |
5 |
|
flbi |
|- ( ( ( N + F ) e. RR /\ N e. ZZ ) -> ( ( |_ ` ( N + F ) ) = N <-> ( N <_ ( N + F ) /\ ( N + F ) < ( N + 1 ) ) ) ) |
6 |
3 4 5
|
syl2anc |
|- ( ( N e. ZZ /\ F e. RR ) -> ( ( |_ ` ( N + F ) ) = N <-> ( N <_ ( N + F ) /\ ( N + F ) < ( N + 1 ) ) ) ) |
7 |
|
addge01 |
|- ( ( N e. RR /\ F e. RR ) -> ( 0 <_ F <-> N <_ ( N + F ) ) ) |
8 |
|
1re |
|- 1 e. RR |
9 |
|
ltadd2 |
|- ( ( F e. RR /\ 1 e. RR /\ N e. RR ) -> ( F < 1 <-> ( N + F ) < ( N + 1 ) ) ) |
10 |
8 9
|
mp3an2 |
|- ( ( F e. RR /\ N e. RR ) -> ( F < 1 <-> ( N + F ) < ( N + 1 ) ) ) |
11 |
10
|
ancoms |
|- ( ( N e. RR /\ F e. RR ) -> ( F < 1 <-> ( N + F ) < ( N + 1 ) ) ) |
12 |
7 11
|
anbi12d |
|- ( ( N e. RR /\ F e. RR ) -> ( ( 0 <_ F /\ F < 1 ) <-> ( N <_ ( N + F ) /\ ( N + F ) < ( N + 1 ) ) ) ) |
13 |
1 12
|
sylan |
|- ( ( N e. ZZ /\ F e. RR ) -> ( ( 0 <_ F /\ F < 1 ) <-> ( N <_ ( N + F ) /\ ( N + F ) < ( N + 1 ) ) ) ) |
14 |
6 13
|
bitr4d |
|- ( ( N e. ZZ /\ F e. RR ) -> ( ( |_ ` ( N + F ) ) = N <-> ( 0 <_ F /\ F < 1 ) ) ) |