Metamath Proof Explorer

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 mulid1 ⊢ ( ( 𝐴 . 𝐵 ) ∈ ℂ → ( ( 𝐴 . 𝐵 ) · 1 ) = ( 𝐴 . 𝐵 ) )
20 18 19 ax-mp ⊢ ( ( 𝐴 . 𝐵 ) · 1 ) = ( 𝐴 . 𝐵 )
21 15 20 eqtri ⊢ ( ( 0 . 𝐴 𝐵 ) · 1 0 ) = ( 𝐴 . 𝐵 )