deccl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > deccl		Structured version Visualization version GIF version

Theorem deccl 11836

Description: Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)

**Hypotheses**
Ref	Expression
deccl.1	⊢ 𝐴 ∈ ℕ₀
deccl.2	⊢ 𝐵 ∈ ℕ₀

**Assertion**
Ref	Expression
deccl	⊢ ;𝐴𝐵 ∈ ℕ₀

**Proof of Theorem deccl**
Step	Hyp	Ref	Expression
1		df-dec 11822	. 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2		9nn0 11644	. . . 4 ⊢ 9 ∈ ℕ₀
3		1nn0 11636	. . . 4 ⊢ 1 ∈ ℕ₀
4	2, 3	nn0addcli 11657	. . 3 ⊢ (9 + 1) ∈ ℕ₀
5		deccl.1	. . 3 ⊢ 𝐴 ∈ ℕ₀
6		deccl.2	. . 3 ⊢ 𝐵 ∈ ℕ₀
7	4, 5, 6	numcl 11834	. 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) ∈ ℕ₀
8	1, 7	eqeltri 2902	1 ⊢ ;𝐴𝐵 ∈ ℕ₀

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2166 (class class class)co 6905 1c1 10253 + caddc 10255 · cmul 10257 9c9 11413 ℕ₀cn0 11618 cdc 11821

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-un 7209 ax-resscn 10309 ax-1cn 10310 ax-icn 10311 ax-addcl 10312 ax-addrcl 10313 ax-mulcl 10314 ax-mulrcl 10315 ax-mulcom 10316 ax-addass 10317 ax-mulass 10318 ax-distr 10319 ax-i2m1 10320 ax-1ne0 10321 ax-1rid 10322 ax-rnegex 10323 ax-rrecex 10324 ax-cnre 10325 ax-pre-lttri 10326 ax-pre-lttrn 10327 ax-pre-ltadd 10328

This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-pss 3814 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4659 df-iun 4742 df-br 4874 df-opab 4936 df-mpt 4953 df-tr 4976 df-id 5250 df-eprel 5255 df-po 5263 df-so 5264 df-fr 5301 df-we 5303 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-pred 5920 df-ord 5966 df-on 5967 df-lim 5968 df-suc 5969 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-f1 6128 df-fo 6129 df-f1o 6130 df-fv 6131 df-ov 6908 df-om 7327 df-wrecs 7672 df-recs 7734 df-rdg 7772 df-er 8009 df-en 8223 df-dom 8224 df-sdom 8225 df-pnf 10393 df-mnf 10394 df-ltxr 10396 df-nn 11351 df-2 11414 df-3 11415 df-4 11416 df-5 11417 df-6 11418 df-7 11419 df-8 11420 df-9 11421 df-n0 11619 df-dec 11822

This theorem is referenced by: 10nn0 11839 3declth 11854 3decltc 11855 decleh 11857 decmul1 11886 bpoly4 15162 fsumcube 15163 3dvds2dec 15431 dec2dvds 16138 dec5dvds2 16140 2exp8 16162 2exp16 16163 prmlem2 16192 37prm 16193 43prm 16194 83prm 16195 139prm 16196 163prm 16197 317prm 16198 631prm 16199 1259lem1 16203 1259lem2 16204 1259lem3 16205 1259lem4 16206 1259lem5 16207 1259prm 16208 2503lem1 16209 2503lem2 16210 2503lem3 16211 2503prm 16212 4001lem1 16213 4001lem2 16214 4001lem3 16215 4001lem4 16216 4001prm 16217 slotsbhcdif 16433 cnfldfun 20118 tnglem 22814 quart1cl 24994 quart1lem 24995 quart1 24996 log2ublem3 25088 log2ub 25089 log2le1 25090 birthday 25094 bpos1 25421 bpos 25431 1kp2ke3k 27861 dp3mul10 30151 dpmul1000 30152 dpadd 30164 dpmul 30166 dpmul4 30167 hgt750lemd 31275 hgt750lem 31278 hgt750lem2 31279 hgt750leme 31285 tgoldbachgnn 31286 tgoldbachgt 31290 kur14lem9 31742 sqn5i 38060 decpmulnc 38062 decpmul 38063 sqdeccom12 38064 sq3deccom12 38065 235t711 38066 ex-decpmul 38067 inductionexd 39293 fmtno3 42293 fmtno4 42294 fmtno5lem1 42295 fmtno5lem2 42296 fmtno5lem3 42297 fmtno5lem4 42298 fmtno5 42299 257prm 42303 fmtno4prmfac 42314 fmtno4nprmfac193 42316 fmtno5faclem1 42321 fmtno5faclem2 42322 fmtno5faclem3 42323 fmtno5fac 42324 fmtno5nprm 42325 139prmALT 42341 31prm 42342 127prm 42345 m7prm 42346 2exp11 42347 m11nprm 42348 evengpoap3 42517 bgoldbachlt 42531 tgoldbachlt 42534