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