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 ℕ_{0}$
	decsplit.2	$⊢ B \in ℕ_{0}$
	decsplit.3	$⊢ D \in ℕ_{0}$
	decsplit.4	$⊢ M \in ℕ_{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 ℕ_{0}$
2		decsplit.2	$⊢ B \in ℕ_{0}$
3		decsplit.3	$⊢ D \in ℕ_{0}$
4		decsplit.4	$⊢ M \in ℕ_{0}$
5		decsplit.5	$⊢ M + 1 = N$
6		decsplit.6	$⊢ A 10^{M} + B = C$
7		10nn0	$⊢ 10 \in ℕ_{0}$
8	7 4	nn0expcli	$⊢ 10^{M} \in ℕ_{0}$
9	1 8	nn0mulcli	$⊢ A 10^{M} \in ℕ_{0}$
10	7 9	nn0mulcli	$⊢ 10 A 10^{M} \in ℕ_{0}$
11	10	nn0cni	$⊢ 10 A 10^{M} \in ℂ$
12	7 2	nn0mulcli	$⊢ 10 B \in ℕ_{0}$
13	12	nn0cni	$⊢ 10 B \in ℂ$
14	3	nn0cni	$⊢ D \in ℂ$
15	11 13 14	addassi	$⊢ 10 A 10^{M} + 10 B + D = 10 A 10^{M} + 10 B + D$
16	7	nn0cni	$⊢ 10 \in ℂ$
17	9	nn0cni	$⊢ A 10^{M} \in ℂ$
18	2	nn0cni	$⊢ B \in ℂ$
19	16 17 18	adddii	$⊢ 10 (A 10^{M} + B) = 10 A 10^{M} + 10 B$
20	6	oveq2i	$⊢ 10 (A 10^{M} + B) = 10 C$
21	19 20	eqtr3i	$⊢ 10 A 10^{M} + 10 B = 10 C$
22	21	oveq1i	$⊢ 10 A 10^{M} + 10 B + D = 10 C + D$
23	15 22	eqtr3i	$⊢ 10 A 10^{M} + 10 B + D = 10 C + 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} = A 10 10^{M}$
28	1	nn0cni	$⊢ A \in ℂ$
29	28 16 24	mul12i	$⊢ A 10 10^{M} = 10 A 10^{M}$
30	27 29	eqtri	$⊢ A 10^{N} = 10 A 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 \|-

Metamath Proof Explorer

Theorem decsplit

Proof