Metamath Proof Explorer

Theorem flbi2

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

Ref Expression
Assertion flbi2 ⊢ N ∈ ℤ ∧ F ∈ ℝ → N + F = N ↔ 0 ≤ F ∧ F < 1

Proof

Step Hyp Ref Expression
1 zre ⊢ N ∈ ℤ → N ∈ ℝ
2 readdcl ⊢ N ∈ ℝ ∧ F ∈ ℝ → N + F ∈ ℝ
3 1 2 sylan ⊢ N ∈ ℤ ∧ F ∈ ℝ → N + F ∈ ℝ
4 simpl ⊢ N ∈ ℤ ∧ F ∈ ℝ → N ∈ ℤ
5 flbi ⊢ N + F ∈ ℝ ∧ N ∈ ℤ → N + F = N ↔ N ≤ N + F ∧ N + F < N + 1
6 3 4 5 syl2anc ⊢ N ∈ ℤ ∧ F ∈ ℝ → N + F = N ↔ N ≤ N + F ∧ N + F < N + 1
7 addge01 ⊢ N ∈ ℝ ∧ F ∈ ℝ → 0 ≤ F ↔ N ≤ N + F
8 1re ⊢ 1 ∈ ℝ
9 ltadd2 ⊢ F ∈ ℝ ∧ 1 ∈ ℝ ∧ N ∈ ℝ → F < 1 ↔ N + F < N + 1
10 8 9 mp3an2 ⊢ F ∈ ℝ ∧ N ∈ ℝ → F < 1 ↔ N + F < N + 1
11 10 ancoms ⊢ N ∈ ℝ ∧ F ∈ ℝ → F < 1 ↔ N + F < N + 1
12 7 11 anbi12d ⊢ N ∈ ℝ ∧ F ∈ ℝ → 0 ≤ F ∧ F < 1 ↔ N ≤ N + F ∧ N + F < N + 1
13 1 12 sylan ⊢ N ∈ ℤ ∧ F ∈ ℝ → 0 ≤ F ∧ F < 1 ↔ N ≤ N + F ∧ N + F < N + 1
14 6 13 bitr4d ⊢ N ∈ ℤ ∧ F ∈ ℝ → N + F = N ↔ 0 ≤ F ∧ F < 1