Metamath Proof Explorer

Theorem decsplit

Description: Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Hypotheses decsplit0.1 ⊢ 𝐴 ∈ ℕ0
decsplit.2 ⊢ 𝐵 ∈ ℕ0
decsplit.3 ⊢ 𝐷 ∈ ℕ0
decsplit.4 ⊢ 𝑀 ∈ ℕ0
decsplit.5 ⊢ ( 𝑀 + 1 ) = 𝑁
decsplit.6 ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) = 𝐶
Assertion decsplit ( ( 𝐴 · ( 1 0 ↑ 𝑁 ) ) + 𝐵 𝐷 ) = 𝐶 𝐷

Proof

Step Hyp Ref Expression
1 decsplit0.1 ⊢ 𝐴 ∈ ℕ0
2 decsplit.2 ⊢ 𝐵 ∈ ℕ0
3 decsplit.3 ⊢ 𝐷 ∈ ℕ0
4 decsplit.4 ⊢ 𝑀 ∈ ℕ0
5 decsplit.5 ⊢ ( 𝑀 + 1 ) = 𝑁
6 decsplit.6 ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) = 𝐶
7 10nn0 ⊢ 1 0 ∈ ℕ0
8 7 4 nn0expcli ⊢ ( 1 0 ↑ 𝑀 ) ∈ ℕ0
9 1 8 nn0mulcli ⊢ ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ∈ ℕ0
10 7 9 nn0mulcli ⊢ ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) ∈ ℕ0
11 10 nn0cni ⊢ ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) ∈ ℂ
12 7 2 nn0mulcli ⊢ ( 1 0 · 𝐵 ) ∈ ℕ0
13 12 nn0cni ⊢ ( 1 0 · 𝐵 ) ∈ ℂ
14 3 nn0cni ⊢ 𝐷 ∈ ℂ
15 11 13 14 addassi ⊢ ( ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( 1 0 · 𝐵 ) ) + 𝐷 ) = ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( 1 0 · 𝐵 ) + 𝐷 ) )
16 7 nn0cni ⊢ 1 0 ∈ ℂ
17 9 nn0cni ⊢ ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ∈ ℂ
18 2 nn0cni ⊢ 𝐵 ∈ ℂ
19 16 17 18 adddii ⊢ ( 1 0 · ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) ) = ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( 1 0 · 𝐵 ) )
20 6 oveq2i ⊢ ( 1 0 · ( ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) + 𝐵 ) ) = ( 1 0 · 𝐶 )
21 19 20 eqtr3i ⊢ ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( 1 0 · 𝐵 ) ) = ( 1 0 · 𝐶 )
22 21 oveq1i ⊢ ( ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( 1 0 · 𝐵 ) ) + 𝐷 ) = ( ( 1 0 · 𝐶 ) + 𝐷 )
23 15 22 eqtr3i ⊢ ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( 1 0 · 𝐵 ) + 𝐷 ) ) = ( ( 1 0 · 𝐶 ) + 𝐷 )
24 8 nn0cni ⊢ ( 1 0 ↑ 𝑀 ) ∈ ℂ
25 24 16 mulcomi ⊢ ( ( 1 0 ↑ 𝑀 ) · 1 0 ) = ( 1 0 · ( 1 0 ↑ 𝑀 ) )
26 7 4 5 25 numexpp1 ⊢ ( 1 0 ↑ 𝑁 ) = ( 1 0 · ( 1 0 ↑ 𝑀 ) )
27 26 oveq2i ⊢ ( 𝐴 · ( 1 0 ↑ 𝑁 ) ) = ( 𝐴 · ( 1 0 · ( 1 0 ↑ 𝑀 ) ) )
28 1 nn0cni ⊢ 𝐴 ∈ ℂ
29 28 16 24 mul12i ⊢ ( 𝐴 · ( 1 0 · ( 1 0 ↑ 𝑀 ) ) ) = ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) )
30 27 29 eqtri ⊢ ( 𝐴 · ( 1 0 ↑ 𝑁 ) ) = ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) )
31 dfdec10 ⊢ 𝐵 𝐷 = ( ( 1 0 · 𝐵 ) + 𝐷 )
32 30 31 oveq12i ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑁 ) ) + 𝐵 𝐷 ) = ( ( 1 0 · ( 𝐴 · ( 1 0 ↑ 𝑀 ) ) ) + ( ( 1 0 · 𝐵 ) + 𝐷 ) )
33 dfdec10 ⊢ 𝐶 𝐷 = ( ( 1 0 · 𝐶 ) + 𝐷 )
34 23 32 33 3eqtr4i ⊢ ( ( 𝐴 · ( 1 0 ↑ 𝑁 ) ) + 𝐵 𝐷 ) = 𝐶 𝐷