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 ⊢A∈ℝ∧B∈ℤ→B≤A↔B≤A

Proof

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