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

Metamath Proof Explorer

Theorem nnmcom

Description: Multiplication of natural numbers is commutative. Theorem 4K(5) of Enderton p. 81. (Contributed by NM, 21-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnmcom 
|- ( ( A e. _om /\ B e. _om ) -> ( A .o B ) = ( B .o A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = A -> ( x .o B ) = ( A .o B ) )
2 oveq2 
 |-  ( x = A -> ( B .o x ) = ( B .o A ) )
3 1 2 eqeq12d 
 |-  ( x = A -> ( ( x .o B ) = ( B .o x ) <-> ( A .o B ) = ( B .o A ) ) )
4 3 imbi2d 
 |-  ( x = A -> ( ( B e. _om -> ( x .o B ) = ( B .o x ) ) <-> ( B e. _om -> ( A .o B ) = ( B .o A ) ) ) )
5 oveq1 
 |-  ( x = (/) -> ( x .o B ) = ( (/) .o B ) )
6 oveq2 
 |-  ( x = (/) -> ( B .o x ) = ( B .o (/) ) )
7 5 6 eqeq12d 
 |-  ( x = (/) -> ( ( x .o B ) = ( B .o x ) <-> ( (/) .o B ) = ( B .o (/) ) ) )
8 oveq1 
 |-  ( x = y -> ( x .o B ) = ( y .o B ) )
9 oveq2 
 |-  ( x = y -> ( B .o x ) = ( B .o y ) )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( x .o B ) = ( B .o x ) <-> ( y .o B ) = ( B .o y ) ) )
11 oveq1 
 |-  ( x = suc y -> ( x .o B ) = ( suc y .o B ) )
12 oveq2 
 |-  ( x = suc y -> ( B .o x ) = ( B .o suc y ) )
13 11 12 eqeq12d 
 |-  ( x = suc y -> ( ( x .o B ) = ( B .o x ) <-> ( suc y .o B ) = ( B .o suc y ) ) )
14 nnm0r 
 |-  ( B e. _om -> ( (/) .o B ) = (/) )
15 nnm0 
 |-  ( B e. _om -> ( B .o (/) ) = (/) )
16 14 15 eqtr4d 
 |-  ( B e. _om -> ( (/) .o B ) = ( B .o (/) ) )
17 oveq1 
 |-  ( ( y .o B ) = ( B .o y ) -> ( ( y .o B ) +o B ) = ( ( B .o y ) +o B ) )
18 nnmsucr 
 |-  ( ( y e. _om /\ B e. _om ) -> ( suc y .o B ) = ( ( y .o B ) +o B ) )
19 nnmsuc 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
20 19 ancoms 
 |-  ( ( y e. _om /\ B e. _om ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
21 18 20 eqeq12d 
 |-  ( ( y e. _om /\ B e. _om ) -> ( ( suc y .o B ) = ( B .o suc y ) <-> ( ( y .o B ) +o B ) = ( ( B .o y ) +o B ) ) )
22 17 21 imbitrrid 
 |-  ( ( y e. _om /\ B e. _om ) -> ( ( y .o B ) = ( B .o y ) -> ( suc y .o B ) = ( B .o suc y ) ) )
23 22 ex 
 |-  ( y e. _om -> ( B e. _om -> ( ( y .o B ) = ( B .o y ) -> ( suc y .o B ) = ( B .o suc y ) ) ) )
24 7 10 13 16 23 finds2 
 |-  ( x e. _om -> ( B e. _om -> ( x .o B ) = ( B .o x ) ) )
25 4 24 vtoclga 
 |-  ( A e. _om -> ( B e. _om -> ( A .o B ) = ( B .o A ) ) )
26 25 imp 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) = ( B .o A ) )