This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnm1

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

Ref Expression
Assertion nnm1 
|- ( A e. _om -> ( A .o 1o ) = A )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 oveq2i 
 |-  ( A .o 1o ) = ( A .o suc (/) )
3 peano1 
 |-  (/) e. _om
4 nnmsuc 
 |-  ( ( A e. _om /\ (/) e. _om ) -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
5 3 4 mpan2 
 |-  ( A e. _om -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
6 nnm0 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )
7 6 oveq1d 
 |-  ( A e. _om -> ( ( A .o (/) ) +o A ) = ( (/) +o A ) )
8 nna0r 
 |-  ( A e. _om -> ( (/) +o A ) = A )
9 5 7 8 3eqtrd 
 |-  ( A e. _om -> ( A .o suc (/) ) = A )
10 2 9 eqtrid 
 |-  ( A e. _om -> ( A .o 1o ) = A )