Theorem reclt0

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

	Ref	Expression
Hypotheses	reclt0.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	reclt0.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion	reclt0	⊢ ( 𝜑 → ( 𝐴 < 0 ↔ ( 1 / 𝐴 ) < 0 ) )

Proof

Step	Hyp	Ref	Expression
1		reclt0.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		reclt0.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → 𝐴 < 0 )
5	3 4	reclt0d	⊢ ( ( 𝜑 ∧ 𝐴 < 0 ) → ( 1 / 𝐴 ) < 0 )
6	5	ex	⊢ ( 𝜑 → ( 𝐴 < 0 → ( 1 / 𝐴 ) < 0 ) )
7		0red	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 ∈ ℝ )
8	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
9	2	necomd	⊢ ( 𝜑 → 0 ≠ 𝐴 )
10	9	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 ≠ 𝐴 )
11		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → ¬ 𝐴 < 0 )
12	7 8 10 11	lttri5d	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → 0 < 𝐴 )
13		0red	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 ∈ ℝ )
14	1 2	rereccld	⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℝ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
16	1	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
17		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
18	16 17	recgt0d	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
19	13 15 18	ltled	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 ≤ ( 1 / 𝐴 ) )
20	13 15	lenltd	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ( 0 ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < 0 ) )
21	19 20	mpbid	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → ¬ ( 1 / 𝐴 ) < 0 )
22	12 21	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 0 ) → ¬ ( 1 / 𝐴 ) < 0 )
23	22	ex	⊢ ( 𝜑 → ( ¬ 𝐴 < 0 → ¬ ( 1 / 𝐴 ) < 0 ) )
24	23	con4d	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) < 0 → 𝐴 < 0 ) )
25	24	imp	⊢ ( ( 𝜑 ∧ ( 1 / 𝐴 ) < 0 ) → 𝐴 < 0 )
26	25	ex	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) < 0 → 𝐴 < 0 ) )
27	6 26	impbid	⊢ ( 𝜑 → ( 𝐴 < 0 ↔ ( 1 / 𝐴 ) < 0 ) )