Metamath Proof Explorer

Theorem dpmul10

Description: Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpval2.a ⊢ 𝐴 ∈ ℕ0
dpval2.b ⊢ 𝐵 ∈ ℝ
Assertion dpmul10 ( ( 𝐴 . 𝐵 ) · 1 0 ) = 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 dpval2.a ⊢ 𝐴 ∈ ℕ0
2 dpval2.b ⊢ 𝐵 ∈ ℝ
3 2 recni ⊢ 𝐵 ∈ ℂ
4 10nn ⊢ 1 0 ∈ ℕ
5 4 nncni ⊢ 1 0 ∈ ℂ
6 4 nnne0i ⊢ 1 0 ≠ 0
7 3 5 6 divcan2i ⊢ ( 1 0 · ( 𝐵 / 1 0 ) ) = 𝐵
8 7 oveq2i ⊢ ( ( 1 0 · 𝐴 ) + ( 1 0 · ( 𝐵 / 1 0 ) ) ) = ( ( 1 0 · 𝐴 ) + 𝐵 )
9 1 2 dpval2 ⊢ ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / 1 0 ) )
10 9 oveq2i ⊢ ( 1 0 · ( 𝐴 . 𝐵 ) ) = ( 1 0 · ( 𝐴 + ( 𝐵 / 1 0 ) ) )
11 dpcl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )
12 1 2 11 mp2an ⊢ ( 𝐴 . 𝐵 ) ∈ ℝ
13 12 recni ⊢ ( 𝐴 . 𝐵 ) ∈ ℂ
14 5 13 mulcomi ⊢ ( 1 0 · ( 𝐴 . 𝐵 ) ) = ( ( 𝐴 . 𝐵 ) · 1 0 )
15 1 nn0cni ⊢ 𝐴 ∈ ℂ
16 3 5 6 divcli ⊢ ( 𝐵 / 1 0 ) ∈ ℂ
17 5 15 16 adddii ⊢ ( 1 0 · ( 𝐴 + ( 𝐵 / 1 0 ) ) ) = ( ( 1 0 · 𝐴 ) + ( 1 0 · ( 𝐵 / 1 0 ) ) )
18 10 14 17 3eqtr3i ⊢ ( ( 𝐴 . 𝐵 ) · 1 0 ) = ( ( 1 0 · 𝐴 ) + ( 1 0 · ( 𝐵 / 1 0 ) ) )
19 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
20 8 18 19 3eqtr4i ⊢ ( ( 𝐴 . 𝐵 ) · 1 0 ) = 𝐴 𝐵