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 / 𝐴 ) ∈ ℤ )