ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulclpi Unicode version

Theorem mulclpi 7263
Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
Assertion
Ref Expression
mulclpi  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .N  B
)  e.  N. )

Proof of Theorem mulclpi
StepHypRef Expression
1 mulpiord 7252 . 2  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .N  B
)  =  ( A  .o  B ) )
2 pinn 7244 . . . 4  |-  ( A  e.  N.  ->  A  e.  om )
3 pinn 7244 . . . 4  |-  ( B  e.  N.  ->  B  e.  om )
4 nnmcl 6443 . . . 4  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  .o  B
)  e.  om )
52, 3, 4syl2an 287 . . 3  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .o  B
)  e.  om )
6 elni2 7249 . . . . . . 7  |-  ( B  e.  N.  <->  ( B  e.  om  /\  (/)  e.  B
) )
76simprbi 273 . . . . . 6  |-  ( B  e.  N.  ->  (/)  e.  B
)
87adantl 275 . . . . 5  |-  ( ( A  e.  N.  /\  B  e.  N. )  -> 
(/)  e.  B )
93adantl 275 . . . . . 6  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  B  e.  om )
102adantr 274 . . . . . 6  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  A  e.  om )
11 elni2 7249 . . . . . . . 8  |-  ( A  e.  N.  <->  ( A  e.  om  /\  (/)  e.  A
) )
1211simprbi 273 . . . . . . 7  |-  ( A  e.  N.  ->  (/)  e.  A
)
1312adantr 274 . . . . . 6  |-  ( ( A  e.  N.  /\  B  e.  N. )  -> 
(/)  e.  A )
14 nnmordi 6478 . . . . . 6  |-  ( ( ( B  e.  om  /\  A  e.  om )  /\  (/)  e.  A )  ->  ( (/)  e.  B  ->  ( A  .o  (/) )  e.  ( A  .o  B
) ) )
159, 10, 13, 14syl21anc 1226 . . . . 5  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( (/)  e.  B  ->  ( A  .o  (/) )  e.  ( A  .o  B
) ) )
168, 15mpd 13 . . . 4  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .o  (/) )  e.  ( A  .o  B
) )
17 ne0i 3413 . . . 4  |-  ( ( A  .o  (/) )  e.  ( A  .o  B
)  ->  ( A  .o  B )  =/=  (/) )
1816, 17syl 14 . . 3  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .o  B
)  =/=  (/) )
19 elni 7243 . . 3  |-  ( ( A  .o  B )  e.  N.  <->  ( ( A  .o  B )  e. 
om  /\  ( A  .o  B )  =/=  (/) ) )
205, 18, 19sylanbrc 414 . 2  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .o  B
)  e.  N. )
211, 20eqeltrd 2241 1  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A  .N  B
)  e.  N. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 2135    =/= wne 2334   (/)c0 3407   omcom 4564  (class class class)co 5839    .o comu 6376   N.cnpi 7207    .N cmi 7209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4094  ax-sep 4097  ax-nul 4105  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-iinf 4562
This theorem depends on definitions:  df-bi 116  df-dc 825  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2726  df-sbc 2950  df-csb 3044  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3408  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-int 3822  df-iun 3865  df-br 3980  df-opab 4041  df-mpt 4042  df-tr 4078  df-id 4268  df-iord 4341  df-on 4343  df-suc 4346  df-iom 4565  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-rn 4612  df-res 4613  df-ima 4614  df-iota 5150  df-fun 5187  df-fn 5188  df-f 5189  df-f1 5190  df-fo 5191  df-f1o 5192  df-fv 5193  df-ov 5842  df-oprab 5843  df-mpo 5844  df-1st 6103  df-2nd 6104  df-recs 6267  df-irdg 6332  df-oadd 6382  df-omul 6383  df-ni 7239  df-mi 7241
This theorem is referenced by:  mulasspig  7267  distrpig  7268  ltmpig  7274  enqer  7293  enqdc  7296  addcmpblnq  7302  mulcmpblnq  7303  addpipqqslem  7304  mulpipq2  7306  mulpipqqs  7308  ordpipqqs  7309  addclnq  7310  mulclnq  7311  addcomnqg  7316  addassnqg  7317  mulassnqg  7319  mulcanenq  7320  distrnqg  7322  recexnq  7325  nqtri3or  7331  ltdcnq  7332  ltsonq  7333  ltanqg  7335  ltmnqg  7336  1lt2nq  7341  ltexnqq  7343  archnqq  7352  addcmpblnq0  7378  mulcmpblnq0  7379  mulcanenq0ec  7380  addclnq0  7386  mulclnq0  7387  nqpnq0nq  7388  nqnq0a  7389  nqnq0m  7390  nq0m0r  7391  distrnq0  7394  addassnq0lemcl  7396
  Copyright terms: Public domain W3C validator