Theorem sn-reclt0d

Description: The reciprocal of a negative real is negative. (Contributed by SN, 26-Nov-2025)

	Ref	Expression
Hypotheses	sn-reclt0d.a	$$⊢\phi \to A\in ℝ$$
	sn-reclt0d.z	$$⊢\phi \to A<0$$
Assertion	sn-reclt0d	$$⊢\phi \to 1{/}_{ℝ}A<0$$

Proof

Step	Hyp	Ref	Expression
1		sn-reclt0d.a	$$⊢\phi \to A\in ℝ$$
2		sn-reclt0d.z	$$⊢\phi \to A<0$$
3	2	lt0ne0d	$$⊢\phi \to A\ne 0$$
4	1 3	sn-rereccld	$$⊢\phi \to 1{/}_{ℝ}A\in ℝ$$
5		rernegcl	$$⊢A\in ℝ\to 0{-}_{ℝ}A\in ℝ$$
6	1 5	syl	$$⊢\phi \to 0{-}_{ℝ}A\in ℝ$$
7		relt0neg1	$$⊢A\in ℝ\to \left(A<0\leftrightarrow 0<0{-}_{ℝ}A\right)$$
8	1 7	syl	$$⊢\phi \to \left(A<0\leftrightarrow 0<0{-}_{ℝ}A\right)$$
9	2 8	mpbid	$$⊢\phi \to 0<0{-}_{ℝ}A$$
10	4 1	remulneg2d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}A\right)=0{-}_{ℝ}\left(1{/}_{ℝ}A\right)A$$
11	1 3	rerecid2d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)A=1$$
12	11	oveq2d	$$⊢\phi \to 0{-}_{ℝ}\left(1{/}_{ℝ}A\right)A=0{-}_{ℝ}1$$
13	10 12	eqtrd	$$⊢\phi \to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}A\right)=0{-}_{ℝ}1$$
14		reneg1lt0	$$⊢0{-}_{ℝ}1<0$$
15	14	a1i	$$⊢\phi \to 0{-}_{ℝ}1<0$$
16	13 15	eqbrtrd	$$⊢\phi \to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}A\right)<0$$
17	4 6 9 16	mulgt0con1d	$$⊢\phi \to 1{/}_{ℝ}A<0$$