Theorem decsplit1

Description: Split a decimal number into two parts. Base case: N = 1 . (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Hypothesis	decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
Assertion	decsplit1	Could not format assertion : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
2		10nn0	$$⊢10\in {\mathbb{N}}_0$$
3	2	numexp1	$$⊢{10}^1=10$$
4	3	oveq2i	$$⊢A{10}^1=A\cdot 10$$
5	2	nn0cni	$$⊢10\in ℂ$$
6	1	nn0cni	$$⊢A\in ℂ$$
7	5 6	mulcomi	$$⊢10A=A\cdot 10$$
8	4 7	eqtr4i	$$⊢A{10}^1=10A$$
9	8	oveq1i	$$⊢A{10}^1+B=10A+B$$
10		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
11	9 10	eqtr4i	Could not format ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B : No typesetting found for |- ( ( A x. ( ; 1 0 ^ 1 ) ) + B ) = ; A B with typecode |-