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

Metamath Proof Explorer

Theorem flwordi

Description: Ordering relation for the floor function. (Contributed by NM, 31-Dec-2005) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion flwordi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
2 1 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
3 2 zred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
4 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
5 flle ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
6 1 5 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
7 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
8 3 1 4 6 7 letrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐵 )
9 flge ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐵 ↔ ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) ) )
10 4 2 9 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐵 ↔ ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) ) )
11 8 10 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ⌊ ‘ 𝐴 ) ≤ ( ⌊ ‘ 𝐵 ) )