![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > decnncl | Structured version Visualization version GIF version |
Description: Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
Ref | Expression |
---|---|
decnncl.1 | ⊢ 𝐴 ∈ ℕ0 |
decnncl.2 | ⊢ 𝐵 ∈ ℕ |
Ref | Expression |
---|---|
decnncl | ⊢ ;𝐴𝐵 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdec10 12664 | . 2 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) | |
2 | 10nn0 12679 | . . 3 ⊢ ;10 ∈ ℕ0 | |
3 | decnncl.1 | . . 3 ⊢ 𝐴 ∈ ℕ0 | |
4 | decnncl.2 | . . 3 ⊢ 𝐵 ∈ ℕ | |
5 | 2, 3, 4 | numnncl 12671 | . 2 ⊢ ((;10 · 𝐴) + 𝐵) ∈ ℕ |
6 | 1, 5 | eqeltri 2829 | 1 ⊢ ;𝐴𝐵 ∈ ℕ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7394 0cc0 11094 1c1 11095 + caddc 11097 · cmul 11099 ℕcn 12196 ℕ0cn0 12456 ;cdc 12661 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-resscn 11151 ax-1cn 11152 ax-icn 11153 ax-addcl 11154 ax-addrcl 11155 ax-mulcl 11156 ax-mulrcl 11157 ax-mulcom 11158 ax-addass 11159 ax-mulass 11160 ax-distr 11161 ax-i2m1 11162 ax-1ne0 11163 ax-1rid 11164 ax-rnegex 11165 ax-rrecex 11166 ax-cnre 11167 ax-pre-lttri 11168 ax-pre-lttrn 11169 ax-pre-ltadd 11170 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-ov 7397 df-om 7840 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8355 df-rdg 8394 df-er 8688 df-en 8925 df-dom 8926 df-sdom 8927 df-pnf 11234 df-mnf 11235 df-ltxr 11237 df-nn 12197 df-2 12259 df-3 12260 df-4 12261 df-5 12262 df-6 12263 df-7 12264 df-8 12265 df-9 12266 df-n0 12457 df-dec 12662 |
This theorem is referenced by: 11prm 17032 13prm 17033 17prm 17034 19prm 17035 23prm 17036 37prm 17038 43prm 17039 83prm 17040 139prm 17041 163prm 17042 317prm 17043 631prm 17044 1259lem1 17048 1259lem2 17049 1259lem3 17050 1259lem4 17051 1259lem5 17052 1259prm 17053 2503lem1 17054 2503lem2 17055 2503lem3 17056 2503prm 17057 4001lem1 17058 4001lem2 17059 4001lem3 17060 4001lem4 17061 4001prm 17062 ocndx 17310 ocid 17311 dsndx 17314 dsid 17315 dsndxnn 17316 unifndx 17324 unifid 17325 unifndxnn 17326 slotsdifunifndx 17330 odrngstr 17332 homndx 17340 homid 17341 ccondx 17342 ccoid 17343 slotsdifocndx 17347 imasvalstr 17381 prdsvalstr 17382 oppchomfvalOLD 17643 oppcbasOLD 17648 resccoOLD 17765 catstr 17893 ipostr 18466 mgpdsOLD 19962 sradsOLD 20758 cnfldstr 20882 tuslemOLD 23703 tmslemOLD 23922 mcubic 26281 cubic2 26282 cubic 26283 quart1cl 26288 quart1lem 26289 quart1 26290 quartlem1 26291 quartlem2 26292 log2ub 26383 log2le1 26384 birthday 26388 bposlem8 26723 bposlem9 26724 pntlemd 27026 pntlema 27028 pntlemb 27029 pntlemf 27037 pntlemo 27039 itvndx 27617 lngndx 27618 itvid 27619 lngid 27620 slotsinbpsd 27621 slotslnbpsd 27622 lngndxnitvndx 27623 trkgstr 27624 ttgvalOLD 28056 ttglemOLD 28058 ttgdsOLD 28067 eengstr 28167 edgfid 28177 edgfndx 28178 edgfndxnn 28179 edgfndxidOLD 28181 baseltedgfOLD 28183 12gcd5e1 40737 60gcd7e1 40739 420gcd8e4 40740 12lcm5e60 40742 60lcm7e420 40744 420lcm8e840 40745 lcmineqlem 40786 3lexlogpow5ineq1 40788 3lexlogpow5ineq2 40789 3lexlogpow5ineq4 40790 3lexlogpow2ineq1 40792 3lexlogpow2ineq2 40793 3lexlogpow5ineq5 40794 aks4d1p1p5 40809 aks4d1p1 40810 257prm 46065 fmtno4prmfac 46076 fmtno4prmfac193 46077 fmtno4nprmfac193 46078 fmtno5nprm 46087 139prmALT 46100 127prm 46103 3exp4mod41 46120 41prothprmlem2 46122 2exp340mod341 46237 341fppr2 46238 bgoldbtbndlem1 46309 tgblthelfgott 46319 tgoldbachlt 46320 tgoldbach 46321 |
Copyright terms: Public domain | W3C validator |