Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfdecOLD | Structured version Visualization version GIF version |
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. Obsolete version of df-dec 11370 as of 1-Aug-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
dfdecOLD | ⊢ ;𝐴𝐵 = ((10 · 𝐴) + 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dec 11370 | . 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | |
2 | 9p1e10OLD 11036 | . . . 4 ⊢ (9 + 1) = 10 | |
3 | 2 | oveq1i 6559 | . . 3 ⊢ ((9 + 1) · 𝐴) = (10 · 𝐴) |
4 | 3 | oveq1i 6559 | . 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((10 · 𝐴) + 𝐵) |
5 | 1, 4 | eqtri 2632 | 1 ⊢ ;𝐴𝐵 = ((10 · 𝐴) + 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 (class class class)co 6549 1c1 9816 + caddc 9818 · cmul 9820 9c9 10954 10c10 10955 ;cdc 11369 |
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-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-10OLD 10964 df-dec 11370 |
This theorem is referenced by: decexOLD 11375 deceq1OLD 11377 deceq2OLD 11379 decclOLD 11389 decnnclOLD 11395 dec0uOLD 11397 dec0hOLD 11399 decnncl2OLD 11402 decltOLD 11407 decltcOLD 11409 decsucOLD 11412 decleOLD 11419 decltiOLD 11424 decsuccOLD 11427 dec10pOLD 11430 decmaOLD 11441 decmacOLD 11443 decma2cOLD 11445 decaddOLD 11447 decaddcOLD 11449 decsubiOLD 11460 decmul1OLD 11462 decmul1cOLD 11464 decmul2cOLD 11466 decmul10addOLD 11470 5t5e25OLD 11516 6t6e36OLD 11523 8t6e48OLD 11536 9t11e99OLD 11548 sq10OLD 12913 3decOLD 12915 3dvdsdecOLD 14893 decsplit1OLD 15628 decsplitOLD 15629 1t10e1p1e11OLD 39938 tgoldbachltOLD 40237 dpfrac1OLD 42313 |
Copyright terms: Public domain | W3C validator |