This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnge2recico01

Description: The reciprocal of an integer greater than 1 is in the right open interval between 0 and 1. (Contributed by AV, 10-Apr-2026)

Ref Expression
Assertion nnge2recico01 ⊢ N ∈ ℤ ≥ 2 → 1 N ∈ 0 1

Proof

Step Hyp Ref Expression
1 eluzelre ⊢ N ∈ ℤ ≥ 2 → N ∈ ℝ
2 eluz2n0 ⊢ N ∈ ℤ ≥ 2 → N ≠ 0
3 1 2 rereccld ⊢ N ∈ ℤ ≥ 2 → 1 N ∈ ℝ
4 1red ⊢ N ∈ ℤ ≥ 2 → 1 ∈ ℝ
5 0le1 ⊢ 0 ≤ 1
6 5 a1i ⊢ N ∈ ℤ ≥ 2 → 0 ≤ 1
7 eluz2nn ⊢ N ∈ ℤ ≥ 2 → N ∈ ℕ
8 7 nngt0d ⊢ N ∈ ℤ ≥ 2 → 0 < N
9 divge0 ⊢ 1 ∈ ℝ ∧ 0 ≤ 1 ∧ N ∈ ℝ ∧ 0 < N → 0 ≤ 1 N
10 4 6 1 8 9 syl22anc ⊢ N ∈ ℤ ≥ 2 → 0 ≤ 1 N
11 eluz2gt1 ⊢ N ∈ ℤ ≥ 2 → 1 < N
12 recgt1 ⊢ N ∈ ℝ ∧ 0 < N → 1 < N ↔ 1 N < 1
13 1 8 12 syl2anc ⊢ N ∈ ℤ ≥ 2 → 1 < N ↔ 1 N < 1
14 11 13 mpbid ⊢ N ∈ ℤ ≥ 2 → 1 N < 1
15 0re ⊢ 0 ∈ ℝ
16 1xr ⊢ 1 ∈ ℝ *
17 15 16 pm3.2i ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ *
18 elico2 ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ * → 1 N ∈ 0 1 ↔ 1 N ∈ ℝ ∧ 0 ≤ 1 N ∧ 1 N < 1
19 17 18 mp1i ⊢ N ∈ ℤ ≥ 2 → 1 N ∈ 0 1 ↔ 1 N ∈ ℝ ∧ 0 ≤ 1 N ∧ 1 N < 1
20 3 10 14 19 mpbir3and ⊢ N ∈ ℤ ≥ 2 → 1 N ∈ 0 1