This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flbi2

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

Ref Expression
Assertion flbi2 ( ( 𝑁 ∈ ℤ ∧ 𝐹 ∈ ℝ ) → ( ( ⌊ ‘ ( 𝑁 + 𝐹 ) ) = 𝑁 ↔ ( 0 ≤ 𝐹 ∧ 𝐹 < 1 ) ) )

Proof

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