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 ∈ ℂ