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

Theorem mulclpi 6831
Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
Assertion
Ref Expression
mulclpi ((𝐴N𝐵N) → (𝐴 ·N 𝐵) ∈ N)

Proof of Theorem mulclpi
StepHypRef Expression
1 mulpiord 6820 . 2 ((𝐴N𝐵N) → (𝐴 ·N 𝐵) = (𝐴 ·𝑜 𝐵))
2 pinn 6812 . . . 4 (𝐴N𝐴 ∈ ω)
3 pinn 6812 . . . 4 (𝐵N𝐵 ∈ ω)
4 nnmcl 6196 . . . 4 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 𝐵) ∈ ω)
52, 3, 4syl2an 283 . . 3 ((𝐴N𝐵N) → (𝐴 ·𝑜 𝐵) ∈ ω)
6 elni2 6817 . . . . . . 7 (𝐵N ↔ (𝐵 ∈ ω ∧ ∅ ∈ 𝐵))
76simprbi 269 . . . . . 6 (𝐵N → ∅ ∈ 𝐵)
87adantl 271 . . . . 5 ((𝐴N𝐵N) → ∅ ∈ 𝐵)
93adantl 271 . . . . . 6 ((𝐴N𝐵N) → 𝐵 ∈ ω)
102adantr 270 . . . . . 6 ((𝐴N𝐵N) → 𝐴 ∈ ω)
11 elni2 6817 . . . . . . . 8 (𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
1211simprbi 269 . . . . . . 7 (𝐴N → ∅ ∈ 𝐴)
1312adantr 270 . . . . . 6 ((𝐴N𝐵N) → ∅ ∈ 𝐴)
14 nnmordi 6227 . . . . . 6 (((𝐵 ∈ ω ∧ 𝐴 ∈ ω) ∧ ∅ ∈ 𝐴) → (∅ ∈ 𝐵 → (𝐴 ·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵)))
159, 10, 13, 14syl21anc 1171 . . . . 5 ((𝐴N𝐵N) → (∅ ∈ 𝐵 → (𝐴 ·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵)))
168, 15mpd 13 . . . 4 ((𝐴N𝐵N) → (𝐴 ·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵))
17 ne0i 3281 . . . 4 ((𝐴 ·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵) → (𝐴 ·𝑜 𝐵) ≠ ∅)
1816, 17syl 14 . . 3 ((𝐴N𝐵N) → (𝐴 ·𝑜 𝐵) ≠ ∅)
19 elni 6811 . . 3 ((𝐴 ·𝑜 𝐵) ∈ N ↔ ((𝐴 ·𝑜 𝐵) ∈ ω ∧ (𝐴 ·𝑜 𝐵) ≠ ∅))
205, 18, 19sylanbrc 408 . 2 ((𝐴N𝐵N) → (𝐴 ·𝑜 𝐵) ∈ N)
211, 20eqeltrd 2161 1 ((𝐴N𝐵N) → (𝐴 ·N 𝐵) ∈ N)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1436  wne 2251  c0 3275  ωcom 4378  (class class class)co 5613   ·𝑜 comu 6133  Ncnpi 6775   ·N cmi 6777
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3929  ax-sep 3932  ax-nul 3940  ax-pow 3984  ax-pr 4010  ax-un 4234  ax-setind 4326  ax-iinf 4376
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-int 3672  df-iun 3715  df-br 3821  df-opab 3875  df-mpt 3876  df-tr 3912  df-id 4094  df-iord 4167  df-on 4169  df-suc 4172  df-iom 4379  df-xp 4417  df-rel 4418  df-cnv 4419  df-co 4420  df-dm 4421  df-rn 4422  df-res 4423  df-ima 4424  df-iota 4946  df-fun 4983  df-fn 4984  df-f 4985  df-f1 4986  df-fo 4987  df-f1o 4988  df-fv 4989  df-ov 5616  df-oprab 5617  df-mpt2 5618  df-1st 5868  df-2nd 5869  df-recs 6024  df-irdg 6089  df-oadd 6139  df-omul 6140  df-ni 6807  df-mi 6809
This theorem is referenced by:  mulasspig  6835  distrpig  6836  ltmpig  6842  enqer  6861  enqdc  6864  addcmpblnq  6870  mulcmpblnq  6871  addpipqqslem  6872  mulpipq2  6874  mulpipqqs  6876  ordpipqqs  6877  addclnq  6878  mulclnq  6879  addcomnqg  6884  addassnqg  6885  mulassnqg  6887  mulcanenq  6888  distrnqg  6890  recexnq  6893  nqtri3or  6899  ltdcnq  6900  ltsonq  6901  ltanqg  6903  ltmnqg  6904  1lt2nq  6909  ltexnqq  6911  archnqq  6920  addcmpblnq0  6946  mulcmpblnq0  6947  mulcanenq0ec  6948  addclnq0  6954  mulclnq0  6955  nqpnq0nq  6956  nqnq0a  6957  nqnq0m  6958  nq0m0r  6959  distrnq0  6962  addassnq0lemcl  6964
  Copyright terms: Public domain W3C validator