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 2 1 N = 0

Proof

Step Hyp Ref Expression
1 nnge2recico01 N 2 1 N 0 1
2 ico01fl0 1 N 0 1 1 N = 0
3 1 2 syl N 2 1 N = 0