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	⊢ 𝐴 ∈ ℕ0
	0dp2dp.b	⊢ 𝐵 ∈ ℝ+
Assertion	0dp2dp	⊢ ( ( 0 . _ 𝐴 𝐵 ) · ; 1 0 ) = ( 𝐴 . 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		0dp2dp.a	⊢ 𝐴 ∈ ℕ0
2		0dp2dp.b	⊢ 𝐵 ∈ ℝ+
3		0p1e1	⊢ ( 0 + 1 ) = 1
4		0z	⊢ 0 ∈ ℤ
5		1z	⊢ 1 ∈ ℤ
6	1 2 3 4 5	dpexpp1	⊢ ( ( 𝐴 . 𝐵 ) · ( ; 1 0 ↑ 0 ) ) = ( ( 0 . _ 𝐴 𝐵 ) · ( ; 1 0 ↑ 1 ) )
7		10nn0	⊢ ; 1 0 ∈ ℕ0
8	7	nn0cni	⊢ ; 1 0 ∈ ℂ
9		exp0	⊢ ( ; 1 0 ∈ ℂ → ( ; 1 0 ↑ 0 ) = 1 )
10	8 9	ax-mp	⊢ ( ; 1 0 ↑ 0 ) = 1
11	10	oveq2i	⊢ ( ( 𝐴 . 𝐵 ) · ( ; 1 0 ↑ 0 ) ) = ( ( 𝐴 . 𝐵 ) · 1 )
12		exp1	⊢ ( ; 1 0 ∈ ℂ → ( ; 1 0 ↑ 1 ) = ; 1 0 )
13	8 12	ax-mp	⊢ ( ; 1 0 ↑ 1 ) = ; 1 0
14	13	oveq2i	⊢ ( ( 0 . _ 𝐴 𝐵 ) · ( ; 1 0 ↑ 1 ) ) = ( ( 0 . _ 𝐴 𝐵 ) · ; 1 0 )
15	6 11 14	3eqtr3ri	⊢ ( ( 0 . _ 𝐴 𝐵 ) · ; 1 0 ) = ( ( 𝐴 . 𝐵 ) · 1 )
16	1 2	rpdpcl	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ+
17		rpcn	⊢ ( ( 𝐴 . 𝐵 ) ∈ ℝ+ → ( 𝐴 . 𝐵 ) ∈ ℂ )
18	16 17	ax-mp	⊢ ( 𝐴 . 𝐵 ) ∈ ℂ
19		mulrid	⊢ ( ( 𝐴 . 𝐵 ) ∈ ℂ → ( ( 𝐴 . 𝐵 ) · 1 ) = ( 𝐴 . 𝐵 ) )
20	18 19	ax-mp	⊢ ( ( 𝐴 . 𝐵 ) · 1 ) = ( 𝐴 . 𝐵 )
21	15 20	eqtri	⊢ ( ( 0 . _ 𝐴 𝐵 ) · ; 1 0 ) = ( 𝐴 . 𝐵 )