Metamath Proof Explorer


Theorem flbi2

Description: A condition equivalent to floor. (Contributed by NM, 15-Aug-2008)

Ref Expression
Assertion flbi2
|- ( ( N e. ZZ /\ F e. RR ) -> ( ( |_ ` ( N + F ) ) = N <-> ( 0 <_ F /\ F < 1 ) ) )

Proof

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