Metamath Proof Explorer


Theorem nnm1

Description: Multiply an element of _om by 1o . (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion nnm1 ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ด ยทo 1o ) = ๐ด )

Proof

Step Hyp Ref Expression
1 df-1o โŠข 1o = suc โˆ…
2 1 oveq2i โŠข ( ๐ด ยทo 1o ) = ( ๐ด ยทo suc โˆ… )
3 peano1 โŠข โˆ… โˆˆ ฯ‰
4 nnmsuc โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ฯ‰ ) โ†’ ( ๐ด ยทo suc โˆ… ) = ( ( ๐ด ยทo โˆ… ) +o ๐ด ) )
5 3 4 mpan2 โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ด ยทo suc โˆ… ) = ( ( ๐ด ยทo โˆ… ) +o ๐ด ) )
6 nnm0 โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ด ยทo โˆ… ) = โˆ… )
7 6 oveq1d โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ( ๐ด ยทo โˆ… ) +o ๐ด ) = ( โˆ… +o ๐ด ) )
8 nna0r โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( โˆ… +o ๐ด ) = ๐ด )
9 5 7 8 3eqtrd โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ด ยทo suc โˆ… ) = ๐ด )
10 2 9 eqtrid โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ๐ด ยทo 1o ) = ๐ด )