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

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. )