# Metamath Proof Explorer

## Theorem flbi2

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

Ref Expression
Assertion flbi2 ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to \left(⌊{N}+{F}⌋={N}↔\left(0\le {F}\wedge {F}<1\right)\right)$

### Proof

Step Hyp Ref Expression
1 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
2 readdcl ${⊢}\left({N}\in ℝ\wedge {F}\in ℝ\right)\to {N}+{F}\in ℝ$
3 1 2 sylan ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to {N}+{F}\in ℝ$
4 simpl ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to {N}\in ℤ$
5 flbi ${⊢}\left({N}+{F}\in ℝ\wedge {N}\in ℤ\right)\to \left(⌊{N}+{F}⌋={N}↔\left({N}\le {N}+{F}\wedge {N}+{F}<{N}+1\right)\right)$
6 3 4 5 syl2anc ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to \left(⌊{N}+{F}⌋={N}↔\left({N}\le {N}+{F}\wedge {N}+{F}<{N}+1\right)\right)$
7 addge01 ${⊢}\left({N}\in ℝ\wedge {F}\in ℝ\right)\to \left(0\le {F}↔{N}\le {N}+{F}\right)$
8 1re ${⊢}1\in ℝ$
9 ltadd2 ${⊢}\left({F}\in ℝ\wedge 1\in ℝ\wedge {N}\in ℝ\right)\to \left({F}<1↔{N}+{F}<{N}+1\right)$
10 8 9 mp3an2 ${⊢}\left({F}\in ℝ\wedge {N}\in ℝ\right)\to \left({F}<1↔{N}+{F}<{N}+1\right)$
11 10 ancoms ${⊢}\left({N}\in ℝ\wedge {F}\in ℝ\right)\to \left({F}<1↔{N}+{F}<{N}+1\right)$
12 7 11 anbi12d ${⊢}\left({N}\in ℝ\wedge {F}\in ℝ\right)\to \left(\left(0\le {F}\wedge {F}<1\right)↔\left({N}\le {N}+{F}\wedge {N}+{F}<{N}+1\right)\right)$
13 1 12 sylan ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to \left(\left(0\le {F}\wedge {F}<1\right)↔\left({N}\le {N}+{F}\wedge {N}+{F}<{N}+1\right)\right)$
14 6 13 bitr4d ${⊢}\left({N}\in ℤ\wedge {F}\in ℝ\right)\to \left(⌊{N}+{F}⌋={N}↔\left(0\le {F}\wedge {F}<1\right)\right)$