Metamath Proof Explorer


Theorem nnmcl

Description: Closure of multiplication of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. (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 )