Theorem sn-recgt0d

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

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

Proof

Step	Hyp	Ref	Expression
1		sn-recgt0d.a	$$⊢\phi \to A\in ℝ$$
2		sn-recgt0d.z	$$⊢\phi \to 0<A$$
3		sn-0lt1	$$⊢0<1$$
4	2	gt0ne0d	$$⊢\phi \to A\ne 0$$
5	1 4	rerecid	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 |-