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

Theorem mulclpi 6177
Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
Assertion
Ref Expression
mulclpi ((A N B N) → (A ·N B) N)

Proof of Theorem mulclpi
StepHypRef Expression
1 mulpiord 6166 . 2 ((A N B N) → (A ·N B) = (A ·𝑜 B))
2 pinn 6158 . . . 4 (A NA 𝜔)
3 pinn 6158 . . . 4 (B NB 𝜔)
4 nnmcl 5966 . . . 4 ((A 𝜔 B 𝜔) → (A ·𝑜 B) 𝜔)
52, 3, 4syl2an 273 . . 3 ((A N B N) → (A ·𝑜 B) 𝜔)
6 elni2 6163 . . . . . . 7 (B N ↔ (B 𝜔 B))
76simprbi 260 . . . . . 6 (B N → ∅ B)
87adantl 262 . . . . 5 ((A N B N) → ∅ B)
93adantl 262 . . . . . 6 ((A N B N) → B 𝜔)
102adantr 261 . . . . . 6 ((A N B N) → A 𝜔)
11 elni2 6163 . . . . . . . 8 (A N ↔ (A 𝜔 A))
1211simprbi 260 . . . . . . 7 (A N → ∅ A)
1312adantr 261 . . . . . 6 ((A N B N) → ∅ A)
14 nnmordi 5991 . . . . . 6 (((B 𝜔 A 𝜔) A) → (∅ B → (A ·𝑜 ∅) (A ·𝑜 B)))
159, 10, 13, 14syl21anc 1117 . . . . 5 ((A N B N) → (∅ B → (A ·𝑜 ∅) (A ·𝑜 B)))
168, 15mpd 13 . . . 4 ((A N B N) → (A ·𝑜 ∅) (A ·𝑜 B))
17 ne0i 3201 . . . 4 ((A ·𝑜 ∅) (A ·𝑜 B) → (A ·𝑜 B) ≠ ∅)
1816, 17syl 14 . . 3 ((A N B N) → (A ·𝑜 B) ≠ ∅)
19 elni 6157 . . 3 ((A ·𝑜 B) N ↔ ((A ·𝑜 B) 𝜔 (A ·𝑜 B) ≠ ∅))
205, 18, 19sylanbrc 394 . 2 ((A N B N) → (A ·𝑜 B) N)
211, 20eqeltrd 2090 1 ((A N B N) → (A ·N B) N)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1369  wne 2180  c0 3195  𝜔com 4231  (class class class)co 5427   ·𝑜 comu 5905  Ncnpi 6121   ·N cmi 6123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-13 1380  ax-14 1381  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998  ax-coll 3838  ax-sep 3841  ax-nul 3849  ax-pow 3893  ax-pr 3910  ax-un 4111  ax-setind 4195  ax-iinf 4229
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3an 871  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1622  df-eu 1879  df-mo 1880  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-ne 2182  df-ral 2283  df-rex 2284  df-reu 2285  df-rab 2287  df-v 2531  df-sbc 2736  df-csb 2824  df-dif 2891  df-un 2893  df-in 2895  df-ss 2902  df-nul 3196  df-pw 3328  df-sn 3348  df-pr 3349  df-op 3351  df-uni 3547  df-int 3582  df-iun 3625  df-br 3731  df-opab 3785  df-mpt 3786  df-tr 3821  df-id 3996  df-iord 4044  df-on 4046  df-suc 4049  df-iom 4232  df-xp 4269  df-rel 4270  df-cnv 4271  df-co 4272  df-dm 4273  df-rn 4274  df-res 4275  df-ima 4276  df-iota 4785  df-fun 4822  df-fn 4823  df-f 4824  df-f1 4825  df-fo 4826  df-f1o 4827  df-fv 4828  df-ov 5430  df-oprab 5431  df-mpt2 5432  df-1st 5681  df-2nd 5682  df-recs 5833  df-irdg 5869  df-oadd 5911  df-omul 5912  df-ni 6153  df-mi 6155
This theorem is referenced by:  mulasspig  6181  distrpig  6182  ltmpig  6188  enqer  6206  enqdc  6209  addcmpblnq  6215  mulcmpblnq  6216  addpipqqslem  6217  mulpipq2  6219  mulpipqqs  6221  ordpipqqs  6222  addclnq  6223  mulclnq  6224  addcomnqg  6229  addassnqg  6230  mulassnqg  6232  mulcanenq  6233  distrnqg  6235  recexnq  6238  nqtri3or  6244  ltdcnq  6245  ltsonq  6246  ltanqg  6248  ltmnqg  6249  1lt2nq  6253  ltexnqq  6255  archnqq  6263  addcmpblnq0  6287  mulcmpblnq0  6288  mulcanenq0ec  6289  addclnq0  6295  mulclnq0  6296  nqpnq0nq  6297  nqnq0a  6298  nqnq0m  6299  nq0m0r  6300  distrnq0  6303  addassnq0lemcl  6305
  Copyright terms: Public domain W3C validator