Metamath Proof Explorer


Theorem recclzi

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

Ref Expression
Hypothesis divclz.1 A
Assertion recclzi A 0 1 A

Proof

Step Hyp Ref Expression
1 divclz.1 A
2 reccl A A 0 1 A
3 1 2 mpan A 0 1 A