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\in {\mathbb{N}}_0$$
	0dp2dp.b	$$⊢B\in {ℝ}^{+}$$
Assertion	0dp2dp	Could not format assertion : No typesetting found for |- ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0dp2dp.a	$$⊢A\in {\mathbb{N}}_0$$
2		0dp2dp.b	$$⊢B\in {ℝ}^{+}$$
3		0p1e1	$$⊢0+1=1$$
4		0z	$$⊢0\in \mathbb{Z}$$
5		1z	$$⊢1\in \mathbb{Z}$$
6	1 2 3 4 5	dpexpp1	Could not format ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) : No typesetting found for |- ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) with typecode |-
7		10nn0	$$⊢10\in {\mathbb{N}}_0$$
8	7	nn0cni	$$⊢10\in ℂ$$
9		exp0	$$⊢10\in ℂ\to {10}^0=1$$
10	8 9	ax-mp	$$⊢{10}^0=1$$
11	10	oveq2i	$$⊢\left(A.B\right){10}^0=\left(A.B\right)\cdot 1$$
12		exp1	$$⊢10\in ℂ\to {10}^1=10$$
13	8 12	ax-mp	$$⊢{10}^1=10$$
14	13	oveq2i	Could not format ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ A B ) x. ; 1 0 ) : No typesetting found for |- ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ A B ) x. ; 1 0 ) with typecode |-
15	6 11 14	3eqtr3ri	Could not format ( ( 0 . _ A B ) x. ; 1 0 ) = ( ( A . B ) x. 1 ) : No typesetting found for |- ( ( 0 . _ A B ) x. ; 1 0 ) = ( ( A . B ) x. 1 ) with typecode |-
16	1 2	rpdpcl	$$⊢A.B\in {ℝ}^{+}$$
17		rpcn	$$⊢A.B\in {ℝ}^{+}\to A.B\in ℂ$$
18	16 17	ax-mp	$$⊢A.B\in ℂ$$
19		mulid1	$$⊢A.B\in ℂ\to \left(A.B\right)\cdot 1=A.B$$
20	18 19	ax-mp	$$⊢\left(A.B\right)\cdot 1=A.B$$
21	15 20	eqtri	Could not format ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B ) : No typesetting found for |- ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B ) with typecode |-