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