Metamath Proof Explorer


Theorem div1

Description: A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion div1 A A 1 = A

Proof

Step Hyp Ref Expression
1 mulid2 A 1 A = A
2 ax-1cn 1
3 ax-1ne0 1 0
4 2 3 pm3.2i 1 1 0
5 divmul A A 1 1 0 A 1 = A 1 A = A
6 4 5 mp3an3 A A A 1 = A 1 A = A
7 6 anidms A A 1 = A 1 A = A
8 1 7 mpbird A A 1 = A