Theorem flword2

Description: Ordering relationship for the greatest integer function. (Contributed by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Assertion	flword2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
2	1	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
3		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
4	3	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐵 ) ∈ ℤ )
5		flwordi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) )
6		eluz2	⊢ ( ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ ( ⌊ ‘ 𝐵 ) ∈ ℤ ∧ ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) ) )
7	2 4 5 6	syl3anbrc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝐴 ) ) )