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 )

Metamath Proof Explorer

Theorem dfdec100

Proof