Theorem dfdec100

Description: Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021)

	Ref	Expression
Hypotheses	dfdec100.a	|- A e. NN0
	dfdec100.b	|- B e. NN0
	dfdec100.c	|- C e. RR
Assertion	dfdec100	|- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C )

Proof

Step	Hyp	Ref	Expression
1		dfdec100.a	|- A e. NN0
2		dfdec100.b	|- B e. NN0
3		dfdec100.c	|- C e. RR
4		dfdec10	|- ; B C = ( ( ; 1 0 x. B ) + C )
5	4	oveq2i	|- ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) )
6		10nn0	|- ; 1 0 e. NN0
7	6	dec0u	|- ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0
8	6	nn0cni	|- ; 1 0 e. CC
9	8 8	mulcli	|- ( ; 1 0 x. ; 1 0 ) e. CC
10	7 9	eqeltrri	|- ; ; 1 0 0 e. CC
11	1	nn0cni	|- A e. CC
12	10 11	mulcli	|- ( ; ; 1 0 0 x. A ) e. CC
13	2	nn0cni	|- B e. CC
14	8 13	mulcli	|- ( ; 1 0 x. B ) e. CC
15	3	recni	|- C e. CC
16	12 14 15	addassi	|- ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) )
17		dfdec10	|- ; ; A B C = ( ( ; 1 0 x. ; A B ) + C )
18		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
19	18	oveq2i	|- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) )
20	8 11	mulcli	|- ( ; 1 0 x. A ) e. CC
21	8 20 13	adddii	|- ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) )
22	8 8 11	mulassi	|- ( ( ; 1 0 x. ; 1 0 ) x. A ) = ( ; 1 0 x. ( ; 1 0 x. A ) )
23	7	oveq1i	|- ( ( ; 1 0 x. ; 1 0 ) x. A ) = ( ; ; 1 0 0 x. A )
24	22 23	eqtr3i	|- ( ; 1 0 x. ( ; 1 0 x. A ) ) = ( ; ; 1 0 0 x. A )
25	24	oveq1i	|- ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) )
26	19 21 25	3eqtri	|- ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) )
27	26	oveq1i	|- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C )
28	17 27	eqtr2i	|- ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C
29	5 16 28	3eqtr2ri	|- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C )