Theorem dfdec10 9522

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 9520	. 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2		9p1e10 9521	. . . 4 ⊢ (9 + 1) = ;10
3	2	oveq1i 5966	. . 3 ⊢ ((9 + 1) · 𝐴) = (;10 · 𝐴)
4	3	oveq1i 5966	. 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) = ((;10 · 𝐴) + 𝐵)
5	1, 4	eqtri 2227	1 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵)

Syntax hints:   = wceq 1373  (class class class)co 5956  0cc0 7940  1c1 7941   + caddc 7943   · cmul 7945  9c9 9109  ;cdc 9519

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4169  ax-cnex 8031  ax-resscn 8032  ax-1cn 8033  ax-1re 8034  ax-icn 8035  ax-addcl 8036  ax-addrcl 8037  ax-mulcl 8038  ax-mulcom 8041  ax-addass 8042  ax-mulass 8043  ax-distr 8044  ax-1rid 8047  ax-0id 8048  ax-cnre 8051

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-int 3891  df-br 4051  df-iota 5240  df-fv 5287  df-ov 5959  df-inn 9052  df-2 9110  df-3 9111  df-4 9112  df-5 9113  df-6 9114  df-7 9115  df-8 9116  df-9 9117  df-dec 9520

This theorem is referenced by:  decnncl  9538  dec0u  9539  dec0h  9540  decnncl2  9542  declt  9546  decltc  9547  decsuc  9549  decle  9552  declti  9556  decsucc  9559  dec10p  9561  decma  9569  decmac  9570  decma2c  9571  decadd  9572  decaddc  9573  decsubi  9581  decmul1  9582  decmul1c  9583  decmul2c  9584  decmul10add  9587  5t5e25  9621  6t6e36  9626  8t6e48  9637  9t11e99  9648  3dec  10876  3dvdsdec  12246  dec2dvds  12804  dec5dvds  12805  dec5nprm  12807  dec2nprm  12808  decsplit1  12821  decsplit  12822