Metamath Proof Explorer

Theorem flge

Description: The floor function value is the greatest integer less than or equal to its argument. (Contributed by NM, 15-Nov-2004) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion flge ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 flltp1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) )
3 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
4 3 zred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℝ )
5 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℝ )
6 5 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
7 6 peano2zd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℤ )
8 7 zred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ )
9 lelttr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) → 𝐵 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
10 4 5 8 9 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ 𝐴 ∧ 𝐴 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) → 𝐵 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
11 2 10 mpan2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 → 𝐵 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
12 zleltp1 ⊢ ( ( 𝐵 ∈ ℤ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ↔ 𝐵 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
13 3 6 12 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ↔ 𝐵 < ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
14 11 13 sylibrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 → 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ) )
15 flle ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
17 6 zred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
18 letr ⊢ ( ( 𝐵 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
19 4 17 5 18 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
20 16 19 mpan2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ ( ⌊ ‘ 𝐴 ) → 𝐵 ≤ 𝐴 ) )
21 14 20 impbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ≤ 𝐴 ↔ 𝐵 ≤ ( ⌊ ‘ 𝐴 ) ) )