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