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

Metamath Proof Explorer

Theorem decsplit0b

Description: Split a decimal number into two parts. Base case: N = 0 . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Hypothesis decsplit0.1 ⊢ 𝐴 ∈ ℕ0
Assertion decsplit0b ( ( 𝐴 · ( 1 0 ↑ 0 ) ) + 𝐵 ) = ( 𝐴 + 𝐵 )

Proof

Step Hyp Ref Expression
1 decsplit0.1 ⊢ 𝐴 ∈ ℕ0
2 10nn0 ⊢ 1 0 ∈ ℕ0
3 2 numexp0 ⊢ ( 1 0 ↑ 0 ) = 1
4 3 oveq2i ⊢ ( 𝐴 · ( 1 0 ↑ 0 ) ) = ( 𝐴 · 1 )
5 1 nn0cni ⊢ 𝐴 ∈ ℂ
6 5 mulridi ⊢ ( 𝐴 · 1 ) = 𝐴
7 4 6 eqtri ⊢ ( 𝐴 · ( 1 0 ↑ 0 ) ) = 𝐴
8 7 oveq1i ⊢ ( ( 𝐴 · ( 1 0 ↑ 0 ) ) + 𝐵 ) = ( 𝐴 + 𝐵 )