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	mulid1i	⊢ ( 𝐴 · 1 ) = 𝐴
7	4 6	eqtri	⊢ ( 𝐴 · ( ; 1 0 ↑ 0 ) ) = 𝐴
8	7	oveq1i	⊢ ( ( 𝐴 · ( ; 1 0 ↑ 0 ) ) + 𝐵 ) = ( 𝐴 + 𝐵 )