Theorem dfdec10 12718

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.)

Assertion

Ref	Expression
dfdec10	⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵)

Proof of Theorem dfdec10

Step	Hyp	Ref	Expression
1		df-dec 12716	. 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2		9p1e10 12717	. . . 4 ⊢ (9 + 1) = ;10
3	2	oveq1i 7436	. . 3 ⊢ ((9 + 1) · 𝐴) = (;10 · 𝐴)
4	3	oveq1i 7436	. 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((;10 · 𝐴) + 𝐵)
5	1, 4	eqtri 2756	1 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵)

Syntax hints:   = wceq 1533  (class class class)co 7426  0cc0 11146  1c1 11147   + caddc 11149   · cmul 11151  9c9 12312  ;cdc 12715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-dec 12716

This theorem is referenced by:  decnncl  12735  dec0u  12736  dec0h  12737  decnncl2  12739  declt  12743  decltc  12744  decsuc  12746  decle  12749  declti  12753  decsucc  12756  dec10p  12758  decma  12766  decmac  12767  decma2c  12768  decadd  12769  decaddc  12770  decsubi  12778  decmul1c  12780  decmul2c  12781  decmul10add  12784  5t5e25  12818  6t6e36  12823  8t6e48  12834  9t11e99  12845  3dec  14265  bpoly4  16043  3dvdsdec  16316  dec2dvds  17039  dec5dvds  17040  dec5nprm  17042  dec2nprm  17043  decsplit1  17058  decsplit  17059  4001lem1  17117  dfdec100  32614  dpfrac1  32636  dpmul10  32639  dpmul100  32641  dp3mul10  32642  dpmul1000  32643  dpmul  32657  dpmul4  32658  decpmul  41893  1t10e1p1e11  46719  3exp4mod41  46985  41prothprmlem1  46986  41prothprm  46988  tgoldbachlt  47185