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 ⊢ φ → A ∈ ℝ
sn-reclt0d.z ⊢ φ → 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 ⊢ φ → A ∈ ℝ
2 sn-reclt0d.z ⊢ φ → A < 0
3 2 lt0ne0d ⊢ φ → A ≠ 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 ∈ ℝ → 0 - ℝ A ∈ ℝ
6 1 5 syl ⊢ φ → 0 - ℝ A ∈ ℝ
7 relt0neg1 ⊢ A ∈ ℝ → A < 0 ↔ 0 < 0 - ℝ A
8 1 7 syl ⊢ φ → A < 0 ↔ 0 < 0 - ℝ A
9 2 8 mpbid ⊢ φ → 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 rerecid2d 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 ⊢ φ → 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 |-