Metamath Proof Explorer


Theorem recidzi

Description: Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999)

Ref Expression
Hypothesis divclz.1 𝐴 ∈ ℂ
Assertion recidzi ( 𝐴 ≠ 0 → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 divclz.1 𝐴 ∈ ℂ
2 recid ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
3 1 2 mpan ( 𝐴 ≠ 0 → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )