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 e. N. -> ( A .N 1o ) = A )

Proof

Step	Hyp	Ref	Expression
1		1pi	|- 1o e. N.
2		mulpiord	|- ( ( A e. N. /\ 1o e. N. ) -> ( A .N 1o ) = ( A .o 1o ) )
3	1 2	mpan2	|- ( A e. N. -> ( A .N 1o ) = ( A .o 1o ) )
4		pinn	|- ( A e. N. -> A e. _om )
5		nnm1	|- ( A e. _om -> ( A .o 1o ) = A )
6	4 5	syl	|- ( A e. N. -> ( A .o 1o ) = A )
7	3 6	eqtrd	|- ( A e. N. -> ( A .N 1o ) = A )