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 11494 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 11494 | . 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | |
2 | 9p1e10OLD 11159 | . . . 4 ⊢ (9 + 1) = 10 | |
3 | 2 | oveq1i 6660 | . . 3 ⊢ ((9 + 1) · 𝐴) = (10 · 𝐴) |
4 | 3 | oveq1i 6660 | . 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((10 · 𝐴) + 𝐵) |
5 | 1, 4 | eqtri 2644 | 1 ⊢ ;𝐴𝐵 = ((10 · 𝐴) + 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 (class class class)co 6650 1c1 9937 + caddc 9939 · cmul 9941 9c9 11077 10c10 11078 ;cdc 11493 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-10OLD 11087 df-dec 11494 |
This theorem is referenced by: decexOLD 11499 deceq1OLD 11501 deceq2OLD 11503 decclOLD 11513 decnnclOLD 11519 dec0uOLD 11521 dec0hOLD 11523 decnncl2OLD 11526 decltOLD 11531 decltcOLD 11533 decsucOLD 11536 decleOLD 11543 decltiOLD 11548 decsuccOLD 11551 dec10pOLD 11554 decmaOLD 11565 decmacOLD 11567 decma2cOLD 11569 decaddOLD 11571 decaddcOLD 11573 decsubiOLD 11584 decmul1OLD 11586 decmul1cOLD 11588 decmul2cOLD 11590 decmul10addOLD 11594 5t5e25OLD 11640 6t6e36OLD 11647 8t6e48OLD 11660 9t11e99OLD 11672 sq10OLD 13051 3decOLD 13053 3dvdsdecOLD 15055 decsplit1OLD 15790 decsplitOLD 15791 dpfrac1OLD 29600 1t10e1p1e11OLD 41320 tgoldbachltOLD 41710 |
Copyright terms: Public domain | W3C validator |