Theorem 0dp2dp

Description: Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	0dp2dp.a	|- A e. NN0
	0dp2dp.b	|- B e. RR+
Assertion	0dp2dp	|- ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B )

Proof

Step	Hyp	Ref	Expression
1		0dp2dp.a	|- A e. NN0
2		0dp2dp.b	|- B e. RR+
3		0p1e1	|- ( 0 + 1 ) = 1
4		0z	|- 0 e. ZZ
5		1z	|- 1 e. ZZ
6	1 2 3 4 5	dpexpp1	|- ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) )
7		10nn0	|- ; 1 0 e. NN0
8	7	nn0cni	|- ; 1 0 e. CC
9		exp0	|- ( ; 1 0 e. CC -> ( ; 1 0 ^ 0 ) = 1 )
10	8 9	ax-mp	|- ( ; 1 0 ^ 0 ) = 1
11	10	oveq2i	|- ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( A . B ) x. 1 )
12		exp1	|- ( ; 1 0 e. CC -> ( ; 1 0 ^ 1 ) = ; 1 0 )
13	8 12	ax-mp	|- ( ; 1 0 ^ 1 ) = ; 1 0
14	13	oveq2i	|- ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ A B ) x. ; 1 0 )
15	6 11 14	3eqtr3ri	|- ( ( 0 . _ A B ) x. ; 1 0 ) = ( ( A . B ) x. 1 )
16	1 2	rpdpcl	|- ( A . B ) e. RR+
17		rpcn	|- ( ( A . B ) e. RR+ -> ( A . B ) e. CC )
18	16 17	ax-mp	|- ( A . B ) e. CC
19		mulid1	|- ( ( A . B ) e. CC -> ( ( A . B ) x. 1 ) = ( A . B ) )
20	18 19	ax-mp	|- ( ( A . B ) x. 1 ) = ( A . B )
21	15 20	eqtri	|- ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B )