dpval

Description: Define the value of the decimal point operator. See df-dp . (Contributed by David A. Wheeler, 15-May-2015)

		Ref	Expression
	Assertion	dpval	Could not format assertion : No typesetting found for \|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) with typecode \|-

Step	Hyp	Ref	Expression
1		df-dp2	Could not format _ x y = ( x + ( y / ; 1 0 ) ) : No typesetting found for \|- _ x y = ( x + ( y / ; 1 0 ) ) with typecode \|-
2		oveq1	$⊢ x = A \to x + (\frac{y}{10}) = A + (\frac{y}{10})$
3	1 2	eqtrid	Could not format ( x = A -> _ x y = ( A + ( y / ; 1 0 ) ) ) : No typesetting found for \|- ( x = A -> _ x y = ( A + ( y / ; 1 0 ) ) ) with typecode \|-
4		oveq1	$⊢ y = B \to \frac{y}{10} = \frac{B}{10}$
5	4	oveq2d	$⊢ y = B \to A + (\frac{y}{10}) = A + (\frac{B}{10})$
6		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for \|- _ A B = ( A + ( B / ; 1 0 ) ) with typecode \|-
7	5 6	eqtr4di	Could not format ( y = B -> ( A + ( y / ; 1 0 ) ) = _ A B ) : No typesetting found for \|- ( y = B -> ( A + ( y / ; 1 0 ) ) = _ A B ) with typecode \|-
8		df-dp	Could not format . = ( x e. NN0 , y e. RR \|-> _ x y ) : No typesetting found for \|- . = ( x e. NN0 , y e. RR \|-> _ x y ) with typecode \|-
9	6	ovexi	Could not format _ A B e. _V : No typesetting found for \|- _ A B e. _V with typecode \|-
10	3 7 8 9	ovmpo	Could not format ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) : No typesetting found for \|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) with typecode \|-

Metamath Proof Explorer