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	⊢ ( 𝐴 ∈ N → ( 𝐴 ·N 1o ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1pi	⊢ 1o ∈ N
2		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ 1o ∈ N ) → ( 𝐴 ·N 1o ) = ( 𝐴 ·o 1o ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ N → ( 𝐴 ·N 1o ) = ( 𝐴 ·o 1o ) )
4		pinn	⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
5		nnm1	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 1o ) = 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ N → ( 𝐴 ·o 1o ) = 𝐴 )
7	3 6	eqtrd	⊢ ( 𝐴 ∈ N → ( 𝐴 ·N 1o ) = 𝐴 )