Theorem decsplit

Description: Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
	decsplit.2	$$⊢B\in {\mathbb{N}}_0$$
	decsplit.3	$$⊢D\in {\mathbb{N}}_0$$
	decsplit.4	$$⊢M\in {\mathbb{N}}_0$$
	decsplit.5	$$⊢M+1=N$$
	decsplit.6	$$⊢A{10}^M+B=C$$
Assertion	decsplit	Could not format assertion : No typesetting found for |- ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ; C D with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decsplit0.1	$$⊢A\in {\mathbb{N}}_0$$
2		decsplit.2	$$⊢B\in {\mathbb{N}}_0$$
3		decsplit.3	$$⊢D\in {\mathbb{N}}_0$$
4		decsplit.4	$$⊢M\in {\mathbb{N}}_0$$
5		decsplit.5	$$⊢M+1=N$$
6		decsplit.6	$$⊢A{10}^M+B=C$$
7		10nn0	$$⊢10\in {\mathbb{N}}_0$$
8	7 4	nn0expcli	$$⊢{10}^M\in {\mathbb{N}}_0$$
9	1 8	nn0mulcli	$$⊢A{10}^M\in {\mathbb{N}}_0$$
10	7 9	nn0mulcli	$$⊢10A{10}^M\in {\mathbb{N}}_0$$
11	10	nn0cni	$$⊢10A{10}^M\in ℂ$$
12	7 2	nn0mulcli	$$⊢10B\in {\mathbb{N}}_0$$
13	12	nn0cni	$$⊢10B\in ℂ$$
14	3	nn0cni	$$⊢D\in ℂ$$
15	11 13 14	addassi	$$⊢10A{10}^M+10B+D=10A{10}^M+10B+D$$
16	7	nn0cni	$$⊢10\in ℂ$$
17	9	nn0cni	$$⊢A{10}^M\in ℂ$$
18	2	nn0cni	$$⊢B\in ℂ$$
19	16 17 18	adddii	$$⊢10\left(A{10}^M+B\right)=10A{10}^M+10B$$
20	6	oveq2i	$$⊢10\left(A{10}^M+B\right)=10C$$
21	19 20	eqtr3i	$$⊢10A{10}^M+10B=10C$$
22	21	oveq1i	$$⊢10A{10}^M+10B+D=10C+D$$
23	15 22	eqtr3i	$$⊢10A{10}^M+10B+D=10C+D$$
24	8	nn0cni	$$⊢{10}^M\in ℂ$$
25	24 16	mulcomi	$$⊢{10}^M\cdot 10=10{10}^M$$
26	7 4 5 25	numexpp1	$$⊢{10}^N=10{10}^M$$
27	26	oveq2i	$$⊢A{10}^N=A10{10}^M$$
28	1	nn0cni	$$⊢A\in ℂ$$
29	28 16 24	mul12i	$$⊢A10{10}^M=10A{10}^M$$
30	27 29	eqtri	$$⊢A{10}^N=10A{10}^M$$
31		dfdec10	Could not format ; B D = ( ( ; 1 0 x. B ) + D ) : No typesetting found for |- ; B D = ( ( ; 1 0 x. B ) + D ) with typecode |-
32	30 31	oveq12i	Could not format ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ( ; 1 0 x. B ) + D ) ) : No typesetting found for |- ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ( ( ; 1 0 x. ( A x. ( ; 1 0 ^ M ) ) ) + ( ( ; 1 0 x. B ) + D ) ) with typecode |-
33		dfdec10	Could not format ; C D = ( ( ; 1 0 x. C ) + D ) : No typesetting found for |- ; C D = ( ( ; 1 0 x. C ) + D ) with typecode |-
34	23 32 33	3eqtr4i	Could not format ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ; C D : No typesetting found for |- ( ( A x. ( ; 1 0 ^ N ) ) + ; B D ) = ; C D with typecode |-