![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > dfdec10 | GIF version |
Description: Version of the definition of the "decimal constructor" using ;10 instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021.) |
Ref | Expression |
---|---|
dfdec10 | ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dec 9415 | . 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | |
2 | 9p1e10 9416 | . . . 4 ⊢ (9 + 1) = ;10 | |
3 | 2 | oveq1i 5906 | . . 3 ⊢ ((9 + 1) · 𝐴) = (;10 · 𝐴) |
4 | 3 | oveq1i 5906 | . 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((;10 · 𝐴) + 𝐵) |
5 | 1, 4 | eqtri 2210 | 1 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 (class class class)co 5896 0cc0 7841 1c1 7842 + caddc 7844 · cmul 7846 9c9 9007 ;cdc 9414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4136 ax-cnex 7932 ax-resscn 7933 ax-1cn 7934 ax-1re 7935 ax-icn 7936 ax-addcl 7937 ax-addrcl 7938 ax-mulcl 7939 ax-mulcom 7942 ax-addass 7943 ax-mulass 7944 ax-distr 7945 ax-1rid 7948 ax-0id 7949 ax-cnre 7952 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-br 4019 df-iota 5196 df-fv 5243 df-ov 5899 df-inn 8950 df-2 9008 df-3 9009 df-4 9010 df-5 9011 df-6 9012 df-7 9013 df-8 9014 df-9 9015 df-dec 9415 |
This theorem is referenced by: decnncl 9433 dec0u 9434 dec0h 9435 decnncl2 9437 declt 9441 decltc 9442 decsuc 9444 decle 9447 declti 9451 decsucc 9454 dec10p 9456 decma 9464 decmac 9465 decma2c 9466 decadd 9467 decaddc 9468 decsubi 9476 decmul1 9477 decmul1c 9478 decmul2c 9479 decmul10add 9482 5t5e25 9516 6t6e36 9521 8t6e48 9532 9t11e99 9543 3dec 10726 3dvdsdec 11902 |
Copyright terms: Public domain | W3C validator |