Metamath Proof Explorer

Theorem dpmul100

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

Ref Expression
Hypotheses dp3mul10.a ⊢ 𝐴 ∈ ℕ0
dp3mul10.b ⊢ 𝐵 ∈ ℕ0
dp3mul10.c ⊢ 𝐶 ∈ ℝ
Assertion dpmul100 ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) = 𝐴 𝐵 𝐶

Proof

Step Hyp Ref Expression
1 dp3mul10.a ⊢ 𝐴 ∈ ℕ0
2 dp3mul10.b ⊢ 𝐵 ∈ ℕ0
3 dp3mul10.c ⊢ 𝐶 ∈ ℝ
4 2 nn0rei ⊢ 𝐵 ∈ ℝ
5 dp2cl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 𝐶 ∈ ℝ )
6 4 3 5 mp2an ⊢ 𝐵 𝐶 ∈ ℝ
7 1 6 dpval2 ⊢ ( 𝐴 . 𝐵 𝐶 ) = ( 𝐴 + ( 𝐵 𝐶 / 1 0 ) )
8 1 nn0cni ⊢ 𝐴 ∈ ℂ
9 6 recni ⊢ 𝐵 𝐶 ∈ ℂ
10 10nn0 ⊢ 1 0 ∈ ℕ0
11 10 nn0cni ⊢ 1 0 ∈ ℂ
12 10nn ⊢ 1 0 ∈ ℕ
13 12 nnne0i ⊢ 1 0 ≠ 0
14 9 11 13 divcli ⊢ ( 𝐵 𝐶 / 1 0 ) ∈ ℂ
15 8 14 addcli ⊢ ( 𝐴 + ( 𝐵 𝐶 / 1 0 ) ) ∈ ℂ
16 7 15 eqeltri ⊢ ( 𝐴 . 𝐵 𝐶 ) ∈ ℂ
17 16 11 11 mulassi ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) · 1 0 ) = ( ( 𝐴 . 𝐵 𝐶 ) · ( 1 0 · 1 0 ) )
18 1 2 3 dfdec100 ⊢ 𝐴 𝐵 𝐶 = ( ( 1 0 0 · 𝐴 ) + 𝐵 𝐶 )
19 11 8 11 mul32i ⊢ ( ( 1 0 · 𝐴 ) · 1 0 ) = ( ( 1 0 · 1 0 ) · 𝐴 )
20 10 dec0u ⊢ ( 1 0 · 1 0 ) = 1 0 0
21 20 oveq1i ⊢ ( ( 1 0 · 1 0 ) · 𝐴 ) = ( 1 0 0 · 𝐴 )
22 19 21 eqtri ⊢ ( ( 1 0 · 𝐴 ) · 1 0 ) = ( 1 0 0 · 𝐴 )
23 2 3 dpval3 ⊢ ( 𝐵 . 𝐶 ) = 𝐵 𝐶
24 23 oveq1i ⊢ ( ( 𝐵 . 𝐶 ) · 1 0 ) = ( 𝐵 𝐶 · 1 0 )
25 2 3 dpmul10 ⊢ ( ( 𝐵 . 𝐶 ) · 1 0 ) = 𝐵 𝐶
26 24 25 eqtr3i ⊢ ( 𝐵 𝐶 · 1 0 ) = 𝐵 𝐶
27 22 26 oveq12i ⊢ ( ( ( 1 0 · 𝐴 ) · 1 0 ) + ( 𝐵 𝐶 · 1 0 ) ) = ( ( 1 0 0 · 𝐴 ) + 𝐵 𝐶 )
28 1 6 dpmul10 ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) = 𝐴 𝐵 𝐶
29 dfdec10 ⊢ 𝐴 𝐵 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 )
30 28 29 eqtri ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) = ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 )
31 30 oveq1i ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) · 1 0 ) = ( ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 ) · 1 0 )
32 11 8 mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℂ
33 32 9 11 adddiri ⊢ ( ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 ) · 1 0 ) = ( ( ( 1 0 · 𝐴 ) · 1 0 ) + ( 𝐵 𝐶 · 1 0 ) )
34 31 33 eqtr2i ⊢ ( ( ( 1 0 · 𝐴 ) · 1 0 ) + ( 𝐵 𝐶 · 1 0 ) ) = ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) · 1 0 )
35 18 27 34 3eqtr2ri ⊢ ( ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) · 1 0 ) = 𝐴 𝐵 𝐶
36 20 oveq2i ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · ( 1 0 · 1 0 ) ) = ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 )
37 17 35 36 3eqtr3ri ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 0 ) = 𝐴 𝐵 𝐶