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	Could not format assertion : No typesetting found for |- ( ph -> ( 1 /R A ) < 0 ) with typecode |-

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	Could not format ( ph -> ( 1 /R A ) e. RR ) : No typesetting found for |- ( ph -> ( 1 /R A ) e. RR ) with typecode |-
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	Could not format ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R ( ( 1 /R A ) x. A ) ) ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R ( ( 1 /R A ) x. A ) ) ) with typecode |-
11	1 3	rerecid2	Could not format ( ph -> ( ( 1 /R A ) x. A ) = 1 ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. A ) = 1 ) with typecode |-
12	11	oveq2d	Could not format ( ph -> ( 0 -R ( ( 1 /R A ) x. A ) ) = ( 0 -R 1 ) ) : No typesetting found for |- ( ph -> ( 0 -R ( ( 1 /R A ) x. A ) ) = ( 0 -R 1 ) ) with typecode |-
13	10 12	eqtrd	Could not format ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R 1 ) ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) = ( 0 -R 1 ) ) with typecode |-
14		reneg1lt0	$$⊢0{-}_{ℝ}1<0$$
15	14	a1i	$$⊢\phi \to 0{-}_{ℝ}1<0$$
16	13 15	eqbrtrd	Could not format ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) < 0 ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( 0 -R A ) ) < 0 ) with typecode |-
17	4 6 9 16	mulgt0con1d	Could not format ( ph -> ( 1 /R A ) < 0 ) : No typesetting found for |- ( ph -> ( 1 /R A ) < 0 ) with typecode |-