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

Metamath Proof Explorer

Theorem recnz

Description: The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion recnz ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ¬ ( 1 / 𝐴 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 recgt1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 0 < ( 1 / 𝐴 ) ∧ ( 1 / 𝐴 ) < 1 ) )
2 1 simprd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 1 / 𝐴 ) < 1 )
3 1 simpld ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
4 zgt0ge1 ⊢ ( ( 1 / 𝐴 ) ∈ ℤ → ( 0 < ( 1 / 𝐴 ) ↔ 1 ≤ ( 1 / 𝐴 ) ) )
5 3 4 syl5ibcom ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( ( 1 / 𝐴 ) ∈ ℤ → 1 ≤ ( 1 / 𝐴 ) ) )
6 1re ⊢ 1 ∈ ℝ
7 0lt1 ⊢ 0 < 1
8 0re ⊢ 0 ∈ ℝ
9 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
10 8 6 9 mp3an12 ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
11 7 10 mpani ⊢ ( 𝐴 ∈ ℝ → ( 1 < 𝐴 → 0 < 𝐴 ) )
12 11 imdistani ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
13 gt0ne0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ≠ 0 )
15 rereccl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )
16 14 15 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
17 lenlt ⊢ ( ( 1 ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ) → ( 1 ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < 1 ) )
18 6 16 17 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 1 ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < 1 ) )
19 5 18 sylibd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( ( 1 / 𝐴 ) ∈ ℤ → ¬ ( 1 / 𝐴 ) < 1 ) )
20 2 19 mt2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ¬ ( 1 / 𝐴 ) ∈ ℤ )