sn-recgt0d

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

	Ref	Expression
Hypotheses	sn-recgt0d.a	$⊢ φ \to A \in ℝ$
	sn-recgt0d.z	$⊢ φ \to 0 < A$
Assertion	sn-recgt0d	Could not format assertion : No typesetting found for \|- ( ph -> 0 < ( 1 /R A ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		sn-recgt0d.a	$⊢ φ \to A \in ℝ$
2		sn-recgt0d.z	$⊢ φ \to 0 < A$
3		sn-0lt1	$⊢ 0 < 1$
4	2	gt0ne0d	$⊢ φ \to A \neq 0$
5	1 4	rerecidd	Could not format ( ph -> ( A x. ( 1 /R A ) ) = 1 ) : No typesetting found for \|- ( ph -> ( A x. ( 1 /R A ) ) = 1 ) with typecode \|-
6	3 5	breqtrrid	Could not format ( ph -> 0 < ( A x. ( 1 /R A ) ) ) : No typesetting found for \|- ( ph -> 0 < ( A x. ( 1 /R A ) ) ) with typecode \|-
7	1 4	sn-rereccld	Could not format ( ph -> ( 1 /R A ) e. RR ) : No typesetting found for \|- ( ph -> ( 1 /R A ) e. RR ) with typecode \|-
8	1 7 2	mulgt0b1d	Could not format ( ph -> ( 0 < ( 1 /R A ) <-> 0 < ( A x. ( 1 /R A ) ) ) ) : No typesetting found for \|- ( ph -> ( 0 < ( 1 /R A ) <-> 0 < ( A x. ( 1 /R A ) ) ) ) with typecode \|-
9	6 8	mpbird	Could not format ( ph -> 0 < ( 1 /R A ) ) : No typesetting found for \|- ( ph -> 0 < ( 1 /R A ) ) with typecode \|-

Metamath Proof Explorer