![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nn0mulcld | Structured version Visualization version GIF version |
Description: Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nn0red.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
nn0addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℕ0) |
Ref | Expression |
---|---|
nn0mulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0red.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0) | |
2 | nn0addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℕ0) | |
3 | nn0mulcl 11442 | . 2 ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) ∈ ℕ0) | |
4 | 1, 2, 3 | syl2anc 696 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2103 (class class class)co 6765 · cmul 10054 ℕ0cn0 11405 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-resscn 10106 ax-1cn 10107 ax-icn 10108 ax-addcl 10109 ax-addrcl 10110 ax-mulcl 10111 ax-mulrcl 10112 ax-mulcom 10113 ax-addass 10114 ax-mulass 10115 ax-distr 10116 ax-i2m1 10117 ax-1ne0 10118 ax-1rid 10119 ax-rnegex 10120 ax-rrecex 10121 ax-cnre 10122 ax-pre-lttri 10123 ax-pre-lttrn 10124 ax-pre-ltadd 10125 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-ov 6768 df-om 7183 df-wrecs 7527 df-recs 7588 df-rdg 7626 df-er 7862 df-en 8073 df-dom 8074 df-sdom 8075 df-pnf 10189 df-mnf 10190 df-ltxr 10192 df-nn 11134 df-n0 11406 |
This theorem is referenced by: quoremnn0ALT 12771 expmulz 13021 faclbnd4lem3 13197 oddge22np1 15196 mulgcd 15388 rpmulgcd2 15493 hashgcdlem 15616 odzdvds 15623 prmreclem3 15745 vdwapf 15799 vdwlem5 15812 vdwlem6 15813 odmodnn0 18080 odmulg 18094 odadd 18374 ablfacrplem 18585 ablfacrp2 18587 2lgslem1c 25238 2lgslem3a 25241 2lgslem3b 25242 2lgslem3c 25243 2lgslem3d 25244 dchrisumlem1 25298 eulerpartlemsv2 30650 eulerpartlemsf 30651 eulerpartlems 30652 eulerpartlemv 30656 eulerpartlemb 30660 breprexplemc 30940 erdsze2lem1 31413 erdsze2lem2 31414 pell1qrge1 37853 jm2.27c 37993 rmxdiophlem 38001 stoweidlem1 40638 wallispilem4 40705 wallispilem5 40706 wallispi2lem2 40709 stirlinglem3 40713 stirlinglem5 40715 stirlinglem7 40717 stirlinglem10 40720 stirlinglem11 40721 etransclem32 40903 etransclem44 40915 etransclem46 40917 fmtnofac2lem 41907 fmtnofac1 41909 2pwp1prm 41930 lighneallem3 41951 ply1mulgsumlem2 42602 |
Copyright terms: Public domain | W3C validator |