Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nnmulcld | Structured version Visualization version GIF version |
Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnge1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
nnmulcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℕ) |
Ref | Expression |
---|---|
nnmulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | nnmulcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℕ) | |
3 | nnmulcl 10920 | . 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) | |
4 | 1, 2, 3 | syl2anc 691 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 (class class class)co 6549 · cmul 9820 ℕcn 10897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rrecex 9887 ax-cnre 9888 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-om 6958 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-nn 10898 |
This theorem is referenced by: bcm1k 12964 bcp1n 12965 permnn 12975 trireciplem 14433 efaddlem 14662 eftlub 14678 eirrlem 14771 modmulconst 14851 isprm5 15257 crth 15321 phimullem 15322 pcqmul 15396 pcaddlem 15430 pcbc 15442 oddprmdvds 15445 pockthlem 15447 pockthg 15448 vdwlem3 15525 vdwlem6 15528 vdwlem9 15531 torsubg 18080 ablfacrp 18288 dgrcolem1 23833 aalioulem5 23895 aaliou3lem2 23902 log2cnv 24471 log2tlbnd 24472 log2ublem2 24474 log2ub 24476 lgamgulmlem4 24558 wilthlem2 24595 ftalem7 24605 basellem5 24611 mumul 24707 fsumfldivdiaglem 24715 dvdsmulf1o 24720 sgmmul 24726 chtublem 24736 bcmono 24802 bposlem3 24811 bposlem5 24813 gausslemma2dlem1a 24890 lgsquadlem2 24906 lgsquadlem3 24907 lgsquad2lem2 24910 2sqlem6 24948 rplogsumlem1 24973 rplogsumlem2 24974 dchrisum0fmul 24995 vmalogdivsum2 25027 pntrsumbnd2 25056 pntpbnd1 25075 pntpbnd2 25076 ostth2lem2 25123 2sqmod 28979 oddpwdc 29743 eulerpartlemgh 29767 subfaclim 30424 bcprod 30877 faclim2 30887 jm2.27c 36592 relexpmulnn 37020 mccllem 38664 wallispilem5 38962 wallispi2lem1 38964 wallispi2 38966 stirlinglem3 38969 stirlinglem8 38974 stirlinglem15 38981 dirkertrigeqlem3 38993 hoicvrrex 39446 deccarry 39941 fmtnoprmfac2 40017 sfprmdvdsmersenne 40058 lighneallem3 40062 proththdlem 40068 blennnt2 42181 |
Copyright terms: Public domain | W3C validator |