Theorem sn-reclt0d

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

	Ref	Expression
Hypotheses	sn-reclt0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	sn-reclt0d.z	⊢ ( 𝜑 → 𝐴 < 0 )
Assertion	sn-reclt0d	⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		sn-reclt0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sn-reclt0d.z	⊢ ( 𝜑 → 𝐴 < 0 )
3	2	lt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )
4	1 3	sn-rereccld	⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) ∈ ℝ )
5		rernegcl	⊢ ( 𝐴 ∈ ℝ → ( 0 −ℝ 𝐴 ) ∈ ℝ )
6	1 5	syl	⊢ ( 𝜑 → ( 0 −ℝ 𝐴 ) ∈ ℝ )
7		relt0neg1	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ 0 < ( 0 −ℝ 𝐴 ) ) )
8	1 7	syl	⊢ ( 𝜑 → ( 𝐴 < 0 ↔ 0 < ( 0 −ℝ 𝐴 ) ) )
9	2 8	mpbid	⊢ ( 𝜑 → 0 < ( 0 −ℝ 𝐴 ) )
10	4 1	remulneg2d	⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ 𝐴 ) ) = ( 0 −ℝ ( ( 1 /ℝ 𝐴 ) · 𝐴 ) ) )
11	1 3	rerecid2	⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · 𝐴 ) = 1 )
12	11	oveq2d	⊢ ( 𝜑 → ( 0 −ℝ ( ( 1 /ℝ 𝐴 ) · 𝐴 ) ) = ( 0 −ℝ 1 ) )
13	10 12	eqtrd	⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ 𝐴 ) ) = ( 0 −ℝ 1 ) )
14		reneg1lt0	⊢ ( 0 −ℝ 1 ) < 0
15	14	a1i	⊢ ( 𝜑 → ( 0 −ℝ 1 ) < 0 )
16	13 15	eqbrtrd	⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ 𝐴 ) ) < 0 )
17	4 6 9 16	mulgt0con1d	⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) < 0 )