Theorem sn-recgt0d

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

	Ref	Expression
Hypotheses	sn-recgt0d.a	|- ( ph -> A e. RR )
	sn-recgt0d.z	|- ( ph -> 0 < A )
Assertion	sn-recgt0d	|- ( ph -> 0 < ( 1 /R A ) )

Proof

Step	Hyp	Ref	Expression
1		sn-recgt0d.a	|- ( ph -> A e. RR )
2		sn-recgt0d.z	|- ( ph -> 0 < A )
3		sn-0lt1	|- 0 < 1
4	2	gt0ne0d	|- ( ph -> A =/= 0 )
5	1 4	rerecid	|- ( ph -> ( A x. ( 1 /R A ) ) = 1 )
6	3 5	breqtrrid	|- ( ph -> 0 < ( A x. ( 1 /R A ) ) )
7	1 4	sn-rereccld	|- ( ph -> ( 1 /R A ) e. RR )
8	1 7 2	mulgt0b1d	|- ( ph -> ( 0 < ( 1 /R A ) <-> 0 < ( A x. ( 1 /R A ) ) ) )
9	6 8	mpbird	|- ( ph -> 0 < ( 1 /R A ) )