Theorem sn-reclt0d

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

	Ref	Expression
Hypotheses	sn-reclt0d.a	|- ( ph -> A e. RR )
	sn-reclt0d.z	|- ( ph -> A < 0 )
Assertion	sn-reclt0d	|- ( ph -> ( 1 /R A ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		sn-reclt0d.a	|- ( ph -> A e. RR )
2		sn-reclt0d.z	|- ( ph -> A < 0 )
3	2	lt0ne0d	|- ( ph -> A =/= 0 )
4	1 3	sn-rereccld	|- ( ph -> ( 1 /R A ) e. RR )
5		rernegcl	|- ( A e. RR -> ( 0 -R A ) e. RR )
6	1 5	syl	|- ( ph -> ( 0 -R A ) e. RR )
7		relt0neg1	|- ( A e. RR -> ( A < 0 <-> 0 < ( 0 -R A ) ) )
8	1 7	syl	|- ( ph -> ( A < 0 <-> 0 < ( 0 -R A ) ) )
9	2 8	mpbid	|- ( ph -> 0 < ( 0 -R A ) )
10	4 1	remulneg2d	|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R ( ( 1 /R A ) x. A ) ) )
11	1 3	rerecid2	|- ( ph -> ( ( 1 /R A ) x. A ) = 1 )
12	11	oveq2d	|- ( ph -> ( 0 -R ( ( 1 /R A ) x. A ) ) = ( 0 -R 1 ) )
13	10 12	eqtrd	|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R 1 ) )
14		reneg1lt0	|- ( 0 -R 1 ) < 0
15	14	a1i	|- ( ph -> ( 0 -R 1 ) < 0 )
16	13 15	eqbrtrd	|- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) < 0 )
17	4 6 9 16	mulgt0con1d	|- ( ph -> ( 1 /R A ) < 0 )