![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > deccl | 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 |
---|---|
deccl.1 | ⊢ 𝐴 ∈ ℕ0 |
deccl.2 | ⊢ 𝐵 ∈ ℕ0 |
Ref | Expression |
---|---|
deccl | ⊢ ;𝐴𝐵 ∈ ℕ0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dec 12619 | . 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | |
2 | 9nn0 12437 | . . . 4 ⊢ 9 ∈ ℕ0 | |
3 | 1nn0 12429 | . . . 4 ⊢ 1 ∈ ℕ0 | |
4 | 2, 3 | nn0addcli 12450 | . . 3 ⊢ (9 + 1) ∈ ℕ0 |
5 | deccl.1 | . . 3 ⊢ 𝐴 ∈ ℕ0 | |
6 | deccl.2 | . . 3 ⊢ 𝐵 ∈ ℕ0 | |
7 | 4, 5, 6 | numcl 12631 | . 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) ∈ ℕ0 |
8 | 1, 7 | eqeltri 2834 | 1 ⊢ ;𝐴𝐵 ∈ ℕ0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7357 1c1 11052 + caddc 11054 · cmul 11056 9c9 12215 ℕ0cn0 12413 ;cdc 12618 |
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 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 |
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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-om 7803 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-ltxr 11194 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-dec 12619 |
This theorem is referenced by: 10nn0 12636 3declth 12650 3decltc 12651 decleh 12653 decmul1 12682 bpoly4 15942 fsumcube 15943 3dvds2dec 16215 dec2dvds 16935 dec5dvds2 16937 2exp8 16961 2exp11 16962 2exp16 16963 prmlem2 16992 37prm 16993 43prm 16994 83prm 16995 139prm 16996 163prm 16997 317prm 16998 631prm 16999 1259lem1 17003 1259lem2 17004 1259lem3 17005 1259lem4 17006 1259lem5 17007 1259prm 17008 2503lem1 17009 2503lem2 17010 2503lem3 17011 2503prm 17012 4001lem1 17013 4001lem2 17014 4001lem3 17015 4001lem4 17016 4001prm 17017 slotsbhcdif 17296 slotsbhcdifOLD 17297 cnfldfunALTOLD 20810 tnglemOLD 23997 quart1cl 26204 quart1lem 26205 quart1 26206 log2ublem3 26298 log2ub 26299 log2le1 26300 birthday 26304 bpos1 26631 bpos 26641 1kp2ke3k 29390 9p10ne21 29414 dp3mul10 31754 dpmul1000 31755 dpadd 31767 dpmul 31769 dpmul4 31770 hgt750lemd 33261 hgt750lem 33264 hgt750lem2 33265 hgt750leme 33271 tgoldbachgnn 33272 tgoldbachgt 33276 kur14lem9 33808 420gcd8e4 40463 12lcm5e60 40465 60lcm7e420 40467 3exp7 40510 3lexlogpow5ineq1 40511 3lexlogpow5ineq2 40512 3lexlogpow5ineq5 40517 aks4d1p1 40533 sqn5i 40785 decpmulnc 40787 decpmul 40788 sqdeccom12 40789 sq3deccom12 40790 235t711 40791 ex-decpmul 40792 resqrtvalex 41907 imsqrtvalex 41908 inductionexd 42417 fmtno3 45733 fmtno4 45734 fmtno5lem1 45735 fmtno5lem2 45736 fmtno5lem3 45737 fmtno5lem4 45738 fmtno5 45739 257prm 45743 fmtno4prmfac 45754 fmtno4nprmfac193 45756 fmtno5faclem1 45761 fmtno5faclem2 45762 fmtno5faclem3 45763 fmtno5fac 45764 fmtno5nprm 45765 139prmALT 45778 31prm 45779 127prm 45781 m7prm 45782 m11nprm 45783 11t31e341 45914 2exp340mod341 45915 341fppr2 45916 nfermltl2rev 45925 evengpoap3 45981 bgoldbachlt 45995 tgoldbachlt 45998 ackval3012 46768 ackval41a 46770 ackval41 46771 ackval42 46772 prstcocvalOLD 47082 |
Copyright terms: Public domain | W3C validator |