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 \in ℝ \land 1 < A) \to \neg \frac{1}{A} \in ℤ$

Step	Hyp	Ref	Expression
1		recgt1i	$⊢ (A \in ℝ \land 1 < A) \to (0 < \frac{1}{A} \land \frac{1}{A} < 1)$
2	1	simprd	$⊢ (A \in ℝ \land 1 < A) \to \frac{1}{A} < 1$
3	1	simpld	$⊢ (A \in ℝ \land 1 < A) \to 0 < \frac{1}{A}$
4		zgt0ge1	$⊢ \frac{1}{A} \in ℤ \to (0 < \frac{1}{A} \leftrightarrow 1 \leq \frac{1}{A})$
5	3 4	syl5ibcom	$⊢ (A \in ℝ \land 1 < A) \to (\frac{1}{A} \in ℤ \to 1 \leq \frac{1}{A})$
6		1re	$⊢ 1 \in ℝ$
7		0lt1	$⊢ 0 < 1$
8		0re	$⊢ 0 \in ℝ$
9		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land A \in ℝ) \to ((0 < 1 \land 1 < A) \to 0 < A)$
10	8 6 9	mp3an12	$⊢ A \in ℝ \to ((0 < 1 \land 1 < A) \to 0 < A)$
11	7 10	mpani	$⊢ A \in ℝ \to (1 < A \to 0 < A)$
12	11	imdistani	$⊢ (A \in ℝ \land 1 < A) \to (A \in ℝ \land 0 < A)$
13		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
14	12 13	syl	$⊢ (A \in ℝ \land 1 < A) \to A \neq 0$
15		rereccl	$⊢ (A \in ℝ \land A \neq 0) \to \frac{1}{A} \in ℝ$
16	14 15	syldan	$⊢ (A \in ℝ \land 1 < A) \to \frac{1}{A} \in ℝ$
17		lenlt	$⊢ (1 \in ℝ \land \frac{1}{A} \in ℝ) \to (1 \leq \frac{1}{A} \leftrightarrow \neg \frac{1}{A} < 1)$
18	6 16 17	sylancr	$⊢ (A \in ℝ \land 1 < A) \to (1 \leq \frac{1}{A} \leftrightarrow \neg \frac{1}{A} < 1)$
19	5 18	sylibd	$⊢ (A \in ℝ \land 1 < A) \to (\frac{1}{A} \in ℤ \to \neg \frac{1}{A} < 1)$
20	2 19	mt2d	$⊢ (A \in ℝ \land 1 < A) \to \neg \frac{1}{A} \in ℤ$

Metamath Proof Explorer