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

Metamath Proof Explorer

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 ∈ ℕ 0
Assertion decsplit0 ⊢ A ⁢ 10 0 + 0 = A

Proof

Step Hyp Ref Expression
1 decsplit0.1 ⊢ A ∈ ℕ 0
2 1 decsplit0b ⊢ A ⁢ 10 0 + 0 = A + 0
3 1 nn0cni ⊢ A ∈ ℂ
4 3 addridi ⊢ A + 0 = A
5 2 4 eqtri ⊢ A ⁢ 10 0 + 0 = A