Metamath Proof Explorer


Theorem recid

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

Ref Expression
Assertion recid A A 0 A 1 A = 1

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 divcan2 1 A A 0 A 1 A = 1
3 1 2 mp3an1 A A 0 A 1 A = 1