Theorem reclt0

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

	Ref	Expression
Hypotheses	reclt0.1	|- ( ph -> A e. RR )
	reclt0.2	|- ( ph -> A =/= 0 )
Assertion	reclt0	|- ( ph -> ( A < 0 <-> ( 1 / A ) < 0 ) )

Proof

Step	Hyp	Ref	Expression
1		reclt0.1	|- ( ph -> A e. RR )
2		reclt0.2	|- ( ph -> A =/= 0 )
3	1	adantr	|- ( ( ph /\ A < 0 ) -> A e. RR )
4		simpr	|- ( ( ph /\ A < 0 ) -> A < 0 )
5	3 4	reclt0d	|- ( ( ph /\ A < 0 ) -> ( 1 / A ) < 0 )
6	5	ex	|- ( ph -> ( A < 0 -> ( 1 / A ) < 0 ) )
7		0red	|- ( ( ph /\ -. A < 0 ) -> 0 e. RR )
8	1	adantr	|- ( ( ph /\ -. A < 0 ) -> A e. RR )
9	2	necomd	|- ( ph -> 0 =/= A )
10	9	adantr	|- ( ( ph /\ -. A < 0 ) -> 0 =/= A )
11		simpr	|- ( ( ph /\ -. A < 0 ) -> -. A < 0 )
12	7 8 10 11	lttri5d	|- ( ( ph /\ -. A < 0 ) -> 0 < A )
13		0red	|- ( ( ph /\ 0 < A ) -> 0 e. RR )
14	1 2	rereccld	|- ( ph -> ( 1 / A ) e. RR )
15	14	adantr	|- ( ( ph /\ 0 < A ) -> ( 1 / A ) e. RR )
16	1	adantr	|- ( ( ph /\ 0 < A ) -> A e. RR )
17		simpr	|- ( ( ph /\ 0 < A ) -> 0 < A )
18	16 17	recgt0d	|- ( ( ph /\ 0 < A ) -> 0 < ( 1 / A ) )
19	13 15 18	ltled	|- ( ( ph /\ 0 < A ) -> 0 <_ ( 1 / A ) )
20	13 15	lenltd	|- ( ( ph /\ 0 < A ) -> ( 0 <_ ( 1 / A ) <-> -. ( 1 / A ) < 0 ) )
21	19 20	mpbid	|- ( ( ph /\ 0 < A ) -> -. ( 1 / A ) < 0 )
22	12 21	syldan	|- ( ( ph /\ -. A < 0 ) -> -. ( 1 / A ) < 0 )
23	22	ex	|- ( ph -> ( -. A < 0 -> -. ( 1 / A ) < 0 ) )
24	23	con4d	|- ( ph -> ( ( 1 / A ) < 0 -> A < 0 ) )
25	24	imp	|- ( ( ph /\ ( 1 / A ) < 0 ) -> A < 0 )
26	25	ex	|- ( ph -> ( ( 1 / A ) < 0 -> A < 0 ) )
27	6 26	impbid	|- ( ph -> ( A < 0 <-> ( 1 / A ) < 0 ) )