Metamath Proof Explorer


Theorem recid2

Description: Multiplication of a number and its reciprocal. (Contributed by NM, 22-Jun-2006) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion recid2 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )

Proof

Step Hyp Ref Expression
1 ax-1cn 1 ∈ ℂ
2 divcan1 ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )
3 1 2 mp3an1 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 𝐴 ) · 𝐴 ) = 1 )