Metamath Proof Explorer


Theorem mulclpi

Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion mulclpi
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )

Proof

Step Hyp Ref Expression
1 mulpiord
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
2 pinn
 |-  ( A e. N. -> A e. _om )
3 pinn
 |-  ( B e. N. -> B e. _om )
4 nnmcl
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) e. _om )
5 2 3 4 syl2an
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .o B ) e. _om )
6 elni2
 |-  ( B e. N. <-> ( B e. _om /\ (/) e. B ) )
7 6 simprbi
 |-  ( B e. N. -> (/) e. B )
8 7 adantl
 |-  ( ( A e. N. /\ B e. N. ) -> (/) e. B )
9 3 adantl
 |-  ( ( A e. N. /\ B e. N. ) -> B e. _om )
10 2 adantr
 |-  ( ( A e. N. /\ B e. N. ) -> A e. _om )
11 elni2
 |-  ( A e. N. <-> ( A e. _om /\ (/) e. A ) )
12 11 simprbi
 |-  ( A e. N. -> (/) e. A )
13 12 adantr
 |-  ( ( A e. N. /\ B e. N. ) -> (/) e. A )
14 nnmordi
 |-  ( ( ( B e. _om /\ A e. _om ) /\ (/) e. A ) -> ( (/) e. B -> ( A .o (/) ) e. ( A .o B ) ) )
15 9 10 13 14 syl21anc
 |-  ( ( A e. N. /\ B e. N. ) -> ( (/) e. B -> ( A .o (/) ) e. ( A .o B ) ) )
16 8 15 mpd
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .o (/) ) e. ( A .o B ) )
17 16 ne0d
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .o B ) =/= (/) )
18 elni
 |-  ( ( A .o B ) e. N. <-> ( ( A .o B ) e. _om /\ ( A .o B ) =/= (/) ) )
19 5 17 18 sylanbrc
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .o B ) e. N. )
20 1 19 eqeltrd
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )