Metamath Proof Explorer

Theorem nnge2recfl0

Description: The floor of the reciprocal of an integer greater than 1 is 0. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion nnge2recfl0 
|- ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 1 / N ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nnge2recico01 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 / N ) e. ( 0 [,) 1 ) )
2 ico01fl0 
 |-  ( ( 1 / N ) e. ( 0 [,) 1 ) -> ( |_ ` ( 1 / N ) ) = 0 )
3 1 2 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 1 / N ) ) = 0 )