Metamath Proof Explorer


Theorem mulidpi

Description: 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Assertion mulidpi A𝑵A𝑵1𝑜=A

Proof

Step Hyp Ref Expression
1 1pi 1𝑜𝑵
2 mulpiord A𝑵1𝑜𝑵A𝑵1𝑜=A𝑜1𝑜
3 1 2 mpan2 A𝑵A𝑵1𝑜=A𝑜1𝑜
4 pinn A𝑵Aω
5 nnm1 AωA𝑜1𝑜=A
6 4 5 syl A𝑵A𝑜1𝑜=A
7 3 6 eqtrd A𝑵A𝑵1𝑜=A