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 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 / 𝑁 ) ∈ ( 0 [,) 1 ) )

Proof

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