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 ℕ_{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 \|-

Step	Hyp	Ref	Expression
1		0dp2dp.a	$⊢ A \in ℕ_{0}$
2		0dp2dp.b	$⊢ B \in ℝ^{+}$
3		0p1e1	$⊢ 0 + 1 = 1$
4		0z	$⊢ 0 \in ℤ$
5		1z	$⊢ 1 \in ℤ$
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 ℕ_{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	$⊢ (A . B) 10^{0} = (A . B) \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		mulrid	$⊢ A . B \in ℂ \to (A . B) \cdot 1 = A . B$
20	18 19	ax-mp	$⊢ (A . B) \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 \|-

Metamath Proof Explorer