This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dp3mul10

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

Ref Expression
Hypotheses dp3mul10.a ⊢ 𝐴 ∈ ℕ0
dp3mul10.b ⊢ 𝐵 ∈ ℕ0
dp3mul10.c ⊢ 𝐶 ∈ ℝ
Assertion dp3mul10 ( ( 𝐴 . 𝐵 𝐶 ) · 1 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 dpmul10 ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) = 𝐴 𝐵 𝐶
8 dfdec10 ⊢ 𝐴 𝐵 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 )
9 10nn ⊢ 1 0 ∈ ℕ
10 9 nncni ⊢ 1 0 ∈ ℂ
11 1 nn0cni ⊢ 𝐴 ∈ ℂ
12 10 11 mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℂ
13 4 recni ⊢ 𝐵 ∈ ℂ
14 3 recni ⊢ 𝐶 ∈ ℂ
15 9 nnne0i ⊢ 1 0 ≠ 0
16 14 10 15 divcli ⊢ ( 𝐶 / 1 0 ) ∈ ℂ
17 12 13 16 addassi ⊢ ( ( ( 1 0 · 𝐴 ) + 𝐵 ) + ( 𝐶 / 1 0 ) ) = ( ( 1 0 · 𝐴 ) + ( 𝐵 + ( 𝐶 / 1 0 ) ) )
18 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
19 18 oveq1i ⊢ ( 𝐴 𝐵 + ( 𝐶 / 1 0 ) ) = ( ( ( 1 0 · 𝐴 ) + 𝐵 ) + ( 𝐶 / 1 0 ) )
20 df-dp2 ⊢ 𝐵 𝐶 = ( 𝐵 + ( 𝐶 / 1 0 ) )
21 20 oveq2i ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 ) = ( ( 1 0 · 𝐴 ) + ( 𝐵 + ( 𝐶 / 1 0 ) ) )
22 17 19 21 3eqtr4ri ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 ) = ( 𝐴 𝐵 + ( 𝐶 / 1 0 ) )
23 1 2 deccl ⊢ 𝐴 𝐵 ∈ ℕ0
24 23 3 dpval2 ⊢ ( 𝐴 𝐵 . 𝐶 ) = ( 𝐴 𝐵 + ( 𝐶 / 1 0 ) )
25 22 24 eqtr4i ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 𝐶 ) = ( 𝐴 𝐵 . 𝐶 )
26 7 8 25 3eqtri ⊢ ( ( 𝐴 . 𝐵 𝐶 ) · 1 0 ) = ( 𝐴 𝐵 . 𝐶 )