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

Metamath Proof Explorer

Theorem nnmcl

Description: Closure of multiplication of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. Theorem 2.20 of Schloeder p. 6. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = B -> ( A .o x ) = ( A .o B ) )
2 1 eleq1d 
 |-  ( x = B -> ( ( A .o x ) e. _om <-> ( A .o B ) e. _om ) )
3 2 imbi2d 
 |-  ( x = B -> ( ( A e. _om -> ( A .o x ) e. _om ) <-> ( A e. _om -> ( A .o B ) e. _om ) ) )
4 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
5 4 eleq1d 
 |-  ( x = (/) -> ( ( A .o x ) e. _om <-> ( A .o (/) ) e. _om ) )
6 oveq2 
 |-  ( x = y -> ( A .o x ) = ( A .o y ) )
7 6 eleq1d 
 |-  ( x = y -> ( ( A .o x ) e. _om <-> ( A .o y ) e. _om ) )
8 oveq2 
 |-  ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
9 8 eleq1d 
 |-  ( x = suc y -> ( ( A .o x ) e. _om <-> ( A .o suc y ) e. _om ) )
10 nnm0 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )
11 peano1 
 |-  (/) e. _om
12 10 11 eqeltrdi 
 |-  ( A e. _om -> ( A .o (/) ) e. _om )
13 nnacl 
 |-  ( ( ( A .o y ) e. _om /\ A e. _om ) -> ( ( A .o y ) +o A ) e. _om )
14 13 expcom 
 |-  ( A e. _om -> ( ( A .o y ) e. _om -> ( ( A .o y ) +o A ) e. _om ) )
15 14 adantr 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A .o y ) e. _om -> ( ( A .o y ) +o A ) e. _om ) )
16 nnmsuc 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
17 16 eleq1d 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A .o suc y ) e. _om <-> ( ( A .o y ) +o A ) e. _om ) )
18 15 17 sylibrd 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( A .o y ) e. _om -> ( A .o suc y ) e. _om ) )
19 18 expcom 
 |-  ( y e. _om -> ( A e. _om -> ( ( A .o y ) e. _om -> ( A .o suc y ) e. _om ) ) )
20 5 7 9 12 19 finds2 
 |-  ( x e. _om -> ( A e. _om -> ( A .o x ) e. _om ) )
21 3 20 vtoclga 
 |-  ( B e. _om -> ( A e. _om -> ( A .o B ) e. _om ) )
22 21 impcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )