recgt0

Description: The reciprocal of a positive number is positive. Exercise 4 of Apostol p. 21. (Contributed by NM, 25-Aug-1999) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	recgt0	$⊢ (A \in ℝ \land 0 < A) \to 0 < \frac{1}{A}$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land 0 < A) \to A \in ℝ$
2	1	recnd	$⊢ (A \in ℝ \land 0 < A) \to A \in ℂ$
3		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
4	2 3	recne0d	$⊢ (A \in ℝ \land 0 < A) \to \frac{1}{A} \neq 0$
5	4	necomd	$⊢ (A \in ℝ \land 0 < A) \to 0 \neq \frac{1}{A}$
6	5	neneqd	$⊢ (A \in ℝ \land 0 < A) \to \neg 0 = \frac{1}{A}$
7		0lt1	$⊢ 0 < 1$
8		0re	$⊢ 0 \in ℝ$
9		1re	$⊢ 1 \in ℝ$
10	8 9	ltnsymi	$⊢ 0 < 1 \to \neg 1 < 0$
11	7 10	ax-mp	$⊢ \neg 1 < 0$
12		simpll	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to A \in ℝ$
13	3	adantr	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to A \neq 0$
14	12 13	rereccld	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to \frac{1}{A} \in ℝ$
15	14	renegcld	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to - \frac{1}{A} \in ℝ$
16		simpr	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to \frac{1}{A} < 0$
17	1 3	rereccld	$⊢ (A \in ℝ \land 0 < A) \to \frac{1}{A} \in ℝ$
18	17	adantr	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to \frac{1}{A} \in ℝ$
19	18	lt0neg1d	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to (\frac{1}{A} < 0 \leftrightarrow 0 < - \frac{1}{A})$
20	16 19	mpbid	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 0 < - \frac{1}{A}$
21		simplr	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 0 < A$
22	15 12 20 21	mulgt0d	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 0 < (- \frac{1}{A}) A$
23	2	adantr	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to A \in ℂ$
24	23 13	reccld	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to \frac{1}{A} \in ℂ$
25	24 23	mulneg1d	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to (- \frac{1}{A}) A = - (\frac{1}{A}) A$
26	23 13	recid2d	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to (\frac{1}{A}) A = 1$
27	26	negeqd	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to - (\frac{1}{A}) A = - 1$
28	25 27	eqtrd	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to (- \frac{1}{A}) A = - 1$
29	22 28	breqtrd	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 0 < - 1$
30		1red	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 1 \in ℝ$
31	30	lt0neg1d	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to (1 < 0 \leftrightarrow 0 < - 1)$
32	29 31	mpbird	$⊢ ((A \in ℝ \land 0 < A) \land \frac{1}{A} < 0) \to 1 < 0$
33	32	ex	$⊢ (A \in ℝ \land 0 < A) \to (\frac{1}{A} < 0 \to 1 < 0)$
34	11 33	mtoi	$⊢ (A \in ℝ \land 0 < A) \to \neg \frac{1}{A} < 0$
35		ioran	$⊢ \neg (0 = \frac{1}{A} \lor \frac{1}{A} < 0) \leftrightarrow (\neg 0 = \frac{1}{A} \land \neg \frac{1}{A} < 0)$
36	6 34 35	sylanbrc	$⊢ (A \in ℝ \land 0 < A) \to \neg (0 = \frac{1}{A} \lor \frac{1}{A} < 0)$
37		axlttri	$⊢ (0 \in ℝ \land \frac{1}{A} \in ℝ) \to (0 < \frac{1}{A} \leftrightarrow \neg (0 = \frac{1}{A} \lor \frac{1}{A} < 0))$
38	8 17 37	sylancr	$⊢ (A \in ℝ \land 0 < A) \to (0 < \frac{1}{A} \leftrightarrow \neg (0 = \frac{1}{A} \lor \frac{1}{A} < 0))$
39	36 38	mpbird	$⊢ (A \in ℝ \land 0 < A) \to 0 < \frac{1}{A}$

Metamath Proof Explorer

Theorem recgt0

Proof