This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 rerecid2d ⊢ ( 𝜑 → ( ( 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 )