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	$$⊢A\in {\mathbb{N}}_0$$
Assertion	decsplit0b	$$⊢A{10}^0+B=A+B$$

Proof

Step	Hyp	Ref	Expression
1		decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
2		10nn0	$$⊢10\in {\mathbb{N}}_0$$
3	2	numexp0	$$⊢{10}^0=1$$
4	3	oveq2i	$$⊢A{10}^0=A\cdot 1$$
5	1	nn0cni	$$⊢A\in ℂ$$
6	5	mulid1i	$$⊢A\cdot 1=A$$
7	4 6	eqtri	$$⊢A{10}^0=A$$
8	7	oveq1i	$$⊢A{10}^0+B=A+B$$