Metamath Proof Explorer

Theorem dfdec100

Description: Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 dfdec100.a ⊢ 𝐴 ∈ ℕ0
2 dfdec100.b ⊢ 𝐵 ∈ ℕ0
3 dfdec100.c ⊢ 𝐶 ∈ ℝ
4 dfdec10 ⊢ 𝐵 𝐶 = ( ( 1 0 · 𝐵 ) + 𝐶 )
5 4 oveq2i ⊢ ( ( 1 0 0 · 𝐴 ) + 𝐵 𝐶 ) = ( ( 1 0 0 · 𝐴 ) + ( ( 1 0 · 𝐵 ) + 𝐶 ) )
6 10nn0 ⊢ 1 0 ∈ ℕ0
7 6 dec0u ⊢ ( 1 0 · 1 0 ) = 1 0 0
8 6 nn0cni ⊢ 1 0 ∈ ℂ
9 8 8 mulcli ⊢ ( 1 0 · 1 0 ) ∈ ℂ
10 7 9 eqeltrri ⊢ 1 0 0 ∈ ℂ
11 1 nn0cni ⊢ 𝐴 ∈ ℂ
12 10 11 mulcli ⊢ ( 1 0 0 · 𝐴 ) ∈ ℂ
13 2 nn0cni ⊢ 𝐵 ∈ ℂ
14 8 13 mulcli ⊢ ( 1 0 · 𝐵 ) ∈ ℂ
15 3 recni ⊢ 𝐶 ∈ ℂ
16 12 14 15 addassi ⊢ ( ( ( 1 0 0 · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 ) = ( ( 1 0 0 · 𝐴 ) + ( ( 1 0 · 𝐵 ) + 𝐶 ) )
17 dfdec10 ⊢ 𝐴 𝐵 𝐶 = ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 )
18 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
19 18 oveq2i ⊢ ( 1 0 · 𝐴 𝐵 ) = ( 1 0 · ( ( 1 0 · 𝐴 ) + 𝐵 ) )
20 8 11 mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℂ
21 8 20 13 adddii ⊢ ( 1 0 · ( ( 1 0 · 𝐴 ) + 𝐵 ) ) = ( ( 1 0 · ( 1 0 · 𝐴 ) ) + ( 1 0 · 𝐵 ) )
22 8 8 11 mulassi ⊢ ( ( 1 0 · 1 0 ) · 𝐴 ) = ( 1 0 · ( 1 0 · 𝐴 ) )
23 7 oveq1i ⊢ ( ( 1 0 · 1 0 ) · 𝐴 ) = ( 1 0 0 · 𝐴 )
24 22 23 eqtr3i ⊢ ( 1 0 · ( 1 0 · 𝐴 ) ) = ( 1 0 0 · 𝐴 )
25 24 oveq1i ⊢ ( ( 1 0 · ( 1 0 · 𝐴 ) ) + ( 1 0 · 𝐵 ) ) = ( ( 1 0 0 · 𝐴 ) + ( 1 0 · 𝐵 ) )
26 19 21 25 3eqtri ⊢ ( 1 0 · 𝐴 𝐵 ) = ( ( 1 0 0 · 𝐴 ) + ( 1 0 · 𝐵 ) )
27 26 oveq1i ⊢ ( ( 1 0 · 𝐴 𝐵 ) + 𝐶 ) = ( ( ( 1 0 0 · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 )
28 17 27 eqtr2i ⊢ ( ( ( 1 0 0 · 𝐴 ) + ( 1 0 · 𝐵 ) ) + 𝐶 ) = 𝐴 𝐵 𝐶
29 5 16 28 3eqtr2ri ⊢ 𝐴 𝐵 𝐶 = ( ( 1 0 0 · 𝐴 ) + 𝐵 𝐶 )