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 ⊢ A ∈ ℝ ∧ 1 < A → ¬ 1 A ∈ ℤ

Proof

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