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

Metamath Proof Explorer

Theorem halffl

Description: Floor of ( 1 / 2 ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion halffl ⊢ 1 2 = 0

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 halfre ⊢ 1 2 ∈ ℝ
3 halfgt0 ⊢ 0 < 1 2
4 1 2 3 ltleii ⊢ 0 ≤ 1 2
5 halflt1 ⊢ 1 2 < 1
6 1e0p1 ⊢ 1 = 0 + 1
7 5 6 breqtri ⊢ 1 2 < 0 + 1
8 0z ⊢ 0 ∈ ℤ
9 flbi ⊢ 1 2 ∈ ℝ ∧ 0 ∈ ℤ → 1 2 = 0 ↔ 0 ≤ 1 2 ∧ 1 2 < 0 + 1
10 2 8 9 mp2an ⊢ 1 2 = 0 ↔ 0 ≤ 1 2 ∧ 1 2 < 0 + 1
11 4 7 10 mpbir2an ⊢ 1 2 = 0