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