Metamath Proof Explorer

Theorem dpmul1000

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

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

Proof

Step Hyp Ref Expression
1 dpmul1000.a ⊢ 𝐴 ∈ ℕ0
2 dpmul1000.b ⊢ 𝐵 ∈ ℕ0
3 dpmul1000.c ⊢ 𝐶 ∈ ℕ0
4 dpmul1000.d ⊢ 𝐷 ∈ ℝ
5 2 nn0rei ⊢ 𝐵 ∈ ℝ
6 3 nn0rei ⊢ 𝐶 ∈ ℝ
7 dp2cl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → 𝐶 𝐷 ∈ ℝ )
8 6 4 7 mp2an ⊢ 𝐶 𝐷 ∈ ℝ
9 dp2cl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 𝐷 ∈ ℝ ) → 𝐵 𝐶 𝐷 ∈ ℝ )
10 5 8 9 mp2an ⊢ 𝐵 𝐶 𝐷 ∈ ℝ
11 dpcl ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 𝐶 𝐷 ∈ ℝ ) → ( 𝐴 . 𝐵 𝐶 𝐷 ) ∈ ℝ )
12 1 10 11 mp2an ⊢ ( 𝐴 . 𝐵 𝐶 𝐷 ) ∈ ℝ
13 12 recni ⊢ ( 𝐴 . 𝐵 𝐶 𝐷 ) ∈ ℂ
14 10nn0 ⊢ 1 0 ∈ ℕ0
15 0nn0 ⊢ 0 ∈ ℕ0
16 14 15 deccl ⊢ 1 0 0 ∈ ℕ0
17 16 nn0cni ⊢ 1 0 0 ∈ ℂ
18 14 nn0cni ⊢ 1 0 ∈ ℂ
19 13 17 18 mulassi ⊢ ( ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 ) · 1 0 ) = ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · ( 1 0 0 · 1 0 ) )
20 1 2 8 dpmul100 ⊢ ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 ) = 𝐴 𝐵 𝐶 𝐷
21 20 oveq1i ⊢ ( ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 ) · 1 0 ) = ( 𝐴 𝐵 𝐶 𝐷 · 1 0 )
22 16 dec0u ⊢ ( 1 0 · 1 0 0 ) = 1 0 0 0
23 18 17 22 mulcomli ⊢ ( 1 0 0 · 1 0 ) = 1 0 0 0
24 23 oveq2i ⊢ ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · ( 1 0 0 · 1 0 ) ) = ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 0 )
25 19 21 24 3eqtr3i ⊢ ( 𝐴 𝐵 𝐶 𝐷 · 1 0 ) = ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 0 )
26 dfdec10 ⊢ 𝐴 𝐵 𝐶 𝐷 = ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 𝐷 )
27 26 oveq1i ⊢ ( 𝐴 𝐵 𝐶 𝐷 · 1 0 ) = ( ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 𝐷 ) · 1 0 )
28 1 2 deccl ⊢ 𝐴 𝐵 ∈ ℕ0
29 28 nn0cni ⊢ 𝐴 𝐵 ∈ ℂ
30 18 29 mulcli ⊢ ( 1 0 · 𝐴 𝐵 ) ∈ ℂ
31 8 recni ⊢ 𝐶 𝐷 ∈ ℂ
32 30 31 18 adddiri ⊢ ( ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 𝐷 ) · 1 0 ) = ( ( ( 1 0 · 𝐴 𝐵 ) · 1 0 ) + ( 𝐶 𝐷 · 1 0 ) )
33 28 3 4 dfdec100 ⊢ 𝐴 𝐵 𝐶 𝐷 = ( ( 1 0 0 · 𝐴 𝐵 ) + 𝐶 𝐷 )
34 14 dec0u ⊢ ( 1 0 · 1 0 ) = 1 0 0
35 34 oveq1i ⊢ ( ( 1 0 · 1 0 ) · 𝐴 𝐵 ) = ( 1 0 0 · 𝐴 𝐵 )
36 18 18 29 mul32i ⊢ ( ( 1 0 · 1 0 ) · 𝐴 𝐵 ) = ( ( 1 0 · 𝐴 𝐵 ) · 1 0 )
37 35 36 eqtr3i ⊢ ( 1 0 0 · 𝐴 𝐵 ) = ( ( 1 0 · 𝐴 𝐵 ) · 1 0 )
38 3 4 dpmul10 ⊢ ( ( 𝐶 . 𝐷 ) · 1 0 ) = 𝐶 𝐷
39 dpval ⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ ) → ( 𝐶 . 𝐷 ) = 𝐶 𝐷 )
40 3 4 39 mp2an ⊢ ( 𝐶 . 𝐷 ) = 𝐶 𝐷
41 40 oveq1i ⊢ ( ( 𝐶 . 𝐷 ) · 1 0 ) = ( 𝐶 𝐷 · 1 0 )
42 38 41 eqtr3i ⊢ 𝐶 𝐷 = ( 𝐶 𝐷 · 1 0 )
43 37 42 oveq12i ⊢ ( ( 1 0 0 · 𝐴 𝐵 ) + 𝐶 𝐷 ) = ( ( ( 1 0 · 𝐴 𝐵 ) · 1 0 ) + ( 𝐶 𝐷 · 1 0 ) )
44 33 43 eqtr2i ⊢ ( ( ( 1 0 · 𝐴 𝐵 ) · 1 0 ) + ( 𝐶 𝐷 · 1 0 ) ) = 𝐴 𝐵 𝐶 𝐷
45 27 32 44 3eqtri ⊢ ( 𝐴 𝐵 𝐶 𝐷 · 1 0 ) = 𝐴 𝐵 𝐶 𝐷
46 25 45 eqtr3i ⊢ ( ( 𝐴 . 𝐵 𝐶 𝐷 ) · 1 0 0 0 ) = 𝐴 𝐵 𝐶 𝐷