Theorem decsplit0

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	decsplit0	$$⊢A{10}^0+0=A$$

Proof

Step	Hyp	Ref	Expression
1		decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
2	1	decsplit0b	$$⊢A{10}^0+0=A+0$$
3	1	nn0cni	$$⊢A\in ℂ$$
4	3	addridi	$$⊢A+0=A$$
5	2 4	eqtri	$$⊢A{10}^0+0=A$$