![]() |
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 9385 | . 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | |
2 | 9p1e10 9386 | . . . 4 ⊢ (9 + 1) = ;10 | |
3 | 2 | oveq1i 5885 | . . 3 ⊢ ((9 + 1) · 𝐴) = (;10 · 𝐴) |
4 | 3 | oveq1i 5885 | . 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((;10 · 𝐴) + 𝐵) |
5 | 1, 4 | eqtri 2198 | 1 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 (class class class)co 5875 0cc0 7811 1c1 7812 + caddc 7814 · cmul 7816 9c9 8977 ;cdc 9384 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4122 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-1rid 7918 ax-0id 7919 ax-cnre 7922 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2740 df-un 3134 df-in 3136 df-ss 3143 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-br 4005 df-iota 5179 df-fv 5225 df-ov 5878 df-inn 8920 df-2 8978 df-3 8979 df-4 8980 df-5 8981 df-6 8982 df-7 8983 df-8 8984 df-9 8985 df-dec 9385 |
This theorem is referenced by: decnncl 9403 dec0u 9404 dec0h 9405 decnncl2 9407 declt 9411 decltc 9412 decsuc 9414 decle 9417 declti 9421 decsucc 9424 dec10p 9426 decma 9434 decmac 9435 decma2c 9436 decadd 9437 decaddc 9438 decsubi 9446 decmul1 9447 decmul1c 9448 decmul2c 9449 decmul10add 9452 5t5e25 9486 6t6e36 9491 8t6e48 9502 9t11e99 9513 3dec 10694 3dvdsdec 11870 |
Copyright terms: Public domain | W3C validator |