This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-rereccld

Description: Closure law for reciprocal. (Contributed by SN, 25-Nov-2025)

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

Step	Hyp	Ref	Expression
1		sn-rereccld.a	$⊢ φ \to A \in ℝ$
2		sn-rereccld.z	$⊢ φ \to A \neq 0$
3		1red	$⊢ φ \to 1 \in ℝ$
4	3 1 2	sn-redivcld	Could not format ( ph -> ( 1 /R A ) e. RR ) : No typesetting found for \|- ( ph -> ( 1 /R A ) e. RR ) with typecode \|-