Metamath Proof Explorer


Theorem recclzi

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

Ref Expression
Hypothesis divclz.1
|- A e. CC
Assertion recclzi
|- ( A =/= 0 -> ( 1 / A ) e. CC )

Proof

Step Hyp Ref Expression
1 divclz.1
 |-  A e. CC
2 reccl
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
3 1 2 mpan
 |-  ( A =/= 0 -> ( 1 / A ) e. CC )