Theorem dfdec100

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

	Ref	Expression
Hypotheses	dfdec100.a	$$⊢A\in {\mathbb{N}}_0$$
	dfdec100.b	$$⊢B\in {\mathbb{N}}_0$$
	dfdec100.c	$$⊢C\in ℝ$$
Assertion	dfdec100	Could not format assertion : No typesetting found for |- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfdec100.a	$$⊢A\in {\mathbb{N}}_0$$
2		dfdec100.b	$$⊢B\in {\mathbb{N}}_0$$
3		dfdec100.c	$$⊢C\in ℝ$$
4		dfdec10	Could not format ; B C = ( ( ; 1 0 x. B ) + C ) : No typesetting found for |- ; B C = ( ( ; 1 0 x. B ) + C ) with typecode |-
5	4	oveq2i	Could not format ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) : No typesetting found for |- ( ( ; ; 1 0 0 x. A ) + ; B C ) = ( ( ; ; 1 0 0 x. A ) + ( ( ; 1 0 x. B ) + C ) ) with typecode |-
6		10nn0	$$⊢10\in {\mathbb{N}}_0$$
7	6	dec0u	$$⊢10\cdot 10=100$$
8	6	nn0cni	$$⊢10\in ℂ$$
9	8 8	mulcli	$$⊢10\cdot 10\in ℂ$$
10	7 9	eqeltrri	$$⊢100\in ℂ$$
11	1	nn0cni	$$⊢A\in ℂ$$
12	10 11	mulcli	$$⊢100A\in ℂ$$
13	2	nn0cni	$$⊢B\in ℂ$$
14	8 13	mulcli	$$⊢10B\in ℂ$$
15	3	recni	$$⊢C\in ℂ$$
16	12 14 15	addassi	$$⊢100A+10B+C=100A+10B+C$$
17		dfdec10	Could not format ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) : No typesetting found for |- ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) with typecode |-
18		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
19	18	oveq2i	Could not format ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) with typecode |-
20	8 11	mulcli	$$⊢10A\in ℂ$$
21	8 20 13	adddii	$$⊢10\left(10A+B\right)=1010A+10B$$
22	8 8 11	mulassi	$$⊢10\cdot 10A=1010A$$
23	7	oveq1i	$$⊢10\cdot 10A=100A$$
24	22 23	eqtr3i	$$⊢1010A=100A$$
25	24	oveq1i	$$⊢1010A+10B=100A+10B$$
26	19 21 25	3eqtri	Could not format ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) with typecode |-
27	26	oveq1i	Could not format ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-
28	17 27	eqtr2i	Could not format ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C : No typesetting found for |- ( ( ( ; ; 1 0 0 x. A ) + ( ; 1 0 x. B ) ) + C ) = ; ; A B C with typecode |-
29	5 16 28	3eqtr2ri	Could not format ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) : No typesetting found for |- ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode |-