Metamath Proof Explorer


Theorem reccli

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

Ref Expression
Hypotheses divclz.1 A
reccl.2 A 0
Assertion reccli 1 A

Proof

Step Hyp Ref Expression
1 divclz.1 A
2 reccl.2 A 0
3 1 recclzi A 0 1 A
4 2 3 ax-mp 1 A