reclt0

Description: The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Step	Hyp	Ref	Expression
1		reclt0.1	$⊢ φ \to A \in ℝ$
2		reclt0.2	$⊢ φ \to A \neq 0$
3	1	adantr	$⊢ (φ \land A < 0) \to A \in ℝ$
4		simpr	$⊢ (φ \land A < 0) \to A < 0$
5	3 4	reclt0d	$⊢ (φ \land A < 0) \to \frac{1}{A} < 0$
6	5	ex	$⊢ φ \to (A < 0 \to \frac{1}{A} < 0)$
7		0red	$⊢ (φ \land \neg A < 0) \to 0 \in ℝ$
8	1	adantr	$⊢ (φ \land \neg A < 0) \to A \in ℝ$
9	2	necomd	$⊢ φ \to 0 \neq A$
10	9	adantr	$⊢ (φ \land \neg A < 0) \to 0 \neq A$
11		simpr	$⊢ (φ \land \neg A < 0) \to \neg A < 0$
12	7 8 10 11	lttri5d	$⊢ (φ \land \neg A < 0) \to 0 < A$
13		0red	$⊢ (φ \land 0 < A) \to 0 \in ℝ$
14	1 2	rereccld	$⊢ φ \to \frac{1}{A} \in ℝ$
15	14	adantr	$⊢ (φ \land 0 < A) \to \frac{1}{A} \in ℝ$
16	1	adantr	$⊢ (φ \land 0 < A) \to A \in ℝ$
17		simpr	$⊢ (φ \land 0 < A) \to 0 < A$
18	16 17	recgt0d	$⊢ (φ \land 0 < A) \to 0 < \frac{1}{A}$
19	13 15 18	ltled	$⊢ (φ \land 0 < A) \to 0 \leq \frac{1}{A}$
20	13 15	lenltd	$⊢ (φ \land 0 < A) \to (0 \leq \frac{1}{A} \leftrightarrow \neg \frac{1}{A} < 0)$
21	19 20	mpbid	$⊢ (φ \land 0 < A) \to \neg \frac{1}{A} < 0$
22	12 21	syldan	$⊢ (φ \land \neg A < 0) \to \neg \frac{1}{A} < 0$
23	22	ex	$⊢ φ \to (\neg A < 0 \to \neg \frac{1}{A} < 0)$
24	23	con4d	$⊢ φ \to (\frac{1}{A} < 0 \to A < 0)$
25	24	imp	$⊢ (φ \land \frac{1}{A} < 0) \to A < 0$
26	25	ex	$⊢ φ \to (\frac{1}{A} < 0 \to A < 0)$
27	6 26	impbid	$⊢ φ \to (A < 0 \leftrightarrow \frac{1}{A} < 0)$

Metamath Proof Explorer