This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-dp2

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec . (Contributed by David A. Wheeler, 15-May-2015) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	df-dp2	Could not format assertion : No typesetting found for \|- _ A B = ( A + ( B / ; 1 0 ) ) with typecode \|-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	cdp2	Could not format _ A B : No typesetting found for class _ A B with typecode class
3		caddc	$class +$
4		cdiv	$class \div$
5		c1	$class 1$
6		cc0	$class 0$
7	5 6	cdc	$class 10$
8	1 7 4	co	$class (\frac{B}{10})$
9	0 8 3	co	$class (A + (\frac{B}{10}))$
10	2 9	wceq	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for wff _ A B = ( A + ( B / ; 1 0 ) ) with typecode wff