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