# 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 ${⊢}{A}\in {ℕ}_{0}$
dfdec100.b ${⊢}{B}\in {ℕ}_{0}$
dfdec100.c ${⊢}{C}\in ℝ$
Assertion dfdec100 Could not format assertion : No typesetting found for |- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode |-

### Proof

Step Hyp Ref Expression
1 dfdec100.a ${⊢}{A}\in {ℕ}_{0}$
2 dfdec100.b ${⊢}{B}\in {ℕ}_{0}$
3 dfdec100.c ${⊢}{C}\in ℝ$
4 dfdec10 Could not format ; B C = ( ( ; 1 0 x. B ) + C ) : No typesetting found for |- ; B C = ( ( ; 1 0 x. B ) + C ) with typecode |-
5 4 oveq2i Could not format ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) : No typesetting found for |- ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) with typecode |-
6 10nn0 ${⊢}10\in {ℕ}_{0}$
7 6 dec0u ${⊢}10\cdot 10=100$
8 6 nn0cni ${⊢}10\in ℂ$
9 8 8 mulcli ${⊢}10\cdot 10\in ℂ$
10 7 9 eqeltrri ${⊢}100\in ℂ$
11 1 nn0cni ${⊢}{A}\in ℂ$
12 10 11 mulcli ${⊢}100{A}\in ℂ$
13 2 nn0cni ${⊢}{B}\in ℂ$
14 8 13 mulcli ${⊢}10{B}\in ℂ$
15 3 recni ${⊢}{C}\in ℂ$
16 12 14 15 addassi ${⊢}100{A}+10{B}+{C}=100{A}+10{B}+{C}$
17 dfdec10 Could not format ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) : No typesetting found for |- ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) with typecode |-
18 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
19 18 oveq2i Could not format ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) with typecode |-
20 8 11 mulcli ${⊢}10{A}\in ℂ$
21 8 20 13 adddii ${⊢}10\left(10{A}+{B}\right)=1010{A}+10{B}$
22 8 8 11 mulassi ${⊢}10\cdot 10{A}=1010{A}$
23 7 oveq1i ${⊢}10\cdot 10{A}=100{A}$
24 22 23 eqtr3i ${⊢}1010{A}=100{A}$
25 24 oveq1i ${⊢}1010{A}+10{B}=100{A}+10{B}$
26 19 21 25 3eqtri Could not format ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) with typecode |-
27 26 oveq1i Could not format ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-
28 17 27 eqtr2i Could not format ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C : No typesetting found for |- ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C with typecode |-
29 5 16 28 3eqtr2ri Could not format ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) : No typesetting found for |- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode |-