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	⊢ 𝐴 ∈ ℕ0
Assertion	decsplit0	⊢ ( ( 𝐴 · ( ; 1 0 ↑ 0 ) ) + 0 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		decsplit0.1	⊢ 𝐴 ∈ ℕ0
2	1	decsplit0b	⊢ ( ( 𝐴 · ( ; 1 0 ↑ 0 ) ) + 0 ) = ( 𝐴 + 0 )
3	1	nn0cni	⊢ 𝐴 ∈ ℂ
4	3	addid1i	⊢ ( 𝐴 + 0 ) = 𝐴
5	2 4	eqtri	⊢ ( ( 𝐴 · ( ; 1 0 ↑ 0 ) ) + 0 ) = 𝐴