Theorem reclt0

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

	Ref	Expression
Hypotheses	reclt0.1	$$⊢\phi \to A\in ℝ$$
	reclt0.2	$$⊢\phi \to A\ne 0$$
Assertion	reclt0	$$⊢\phi \to \left(A<0\leftrightarrow \frac{1}{A}<0\right)$$

Proof

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