Metamath Proof Explorer


Theorem rerecclzi

Description: Closure law for reciprocal. (Contributed by NM, 30-Apr-2005)

Ref Expression
Hypothesis redivcl.1 A
Assertion rerecclzi A01A

Proof

Step Hyp Ref Expression
1 redivcl.1 A
2 rereccl AA01A
3 1 2 mpan A01A