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 e. RR
2 halfre 
 |-  ( 1 / 2 ) e. RR
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 e. ZZ
9 flbi 
 |-  ( ( ( 1 / 2 ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( 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