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	$$⊢\phi \to 0<1{/}_{ℝ}A$$

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	rerecidd	$$⊢\phi \to A\left(1{/}_{ℝ}A\right)=1$$
6	3 5	breqtrrid	$$⊢\phi \to 0<A\left(1{/}_{ℝ}A\right)$$
7	1 4	sn-rereccld	$$⊢\phi \to 1{/}_{ℝ}A\in ℝ$$
8	1 7 2	mulgt0b1d	$$⊢\phi \to \left(0<1{/}_{ℝ}A\leftrightarrow 0<A\left(1{/}_{ℝ}A\right)\right)$$
9	6 8	mpbird	$$⊢\phi \to 0<1{/}_{ℝ}A$$