Theorem dpmul100

Description: Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dp3mul10.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp3mul10.b	$$⊢B\in {\mathbb{N}}_0$$
3		dp3mul10.c	$$⊢C\in ℝ$$
4	2	nn0rei	$$⊢B\in ℝ$$
5		dp2cl	Could not format ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) : No typesetting found for |- ( ( B e. RR /\ C e. RR ) -> _ B C e. RR ) with typecode |-
6	4 3 5	mp2an	Could not format _ B C e. RR : No typesetting found for |- _ B C e. RR with typecode |-
7	1 6	dpval2	Could not format ( A . _ B C ) = ( A + ( _ B C / ; 1 0 ) ) : No typesetting found for |- ( A . _ B C ) = ( A + ( _ B C / ; 1 0 ) ) with typecode |-
8	1	nn0cni	$$⊢A\in ℂ$$
9	6	recni	Could not format _ B C e. CC : No typesetting found for |- _ B C e. CC with typecode |-
10		10nn0	$$⊢10\in {\mathbb{N}}_0$$
11	10	nn0cni	$$⊢10\in ℂ$$
12		10nn	$$⊢10\in \mathbb{N}$$
13	12	nnne0i	$$⊢10\ne 0$$
14	9 11 13	divcli	Could not format ( _ B C / ; 1 0 ) e. CC : No typesetting found for |- ( _ B C / ; 1 0 ) e. CC with typecode |-
15	8 14	addcli	Could not format ( A + ( _ B C / ; 1 0 ) ) e. CC : No typesetting found for |- ( A + ( _ B C / ; 1 0 ) ) e. CC with typecode |-
16	7 15	eqeltri	Could not format ( A . _ B C ) e. CC : No typesetting found for |- ( A . _ B C ) e. CC with typecode |-
17	16 11 11	mulassi	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) : No typesetting found for |- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) with typecode |-
18	1 2 3	dfdec100	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 |-
19	11 8 11	mul32i	$$⊢10A\cdot 10=10\cdot 10A$$
20	10	dec0u	$$⊢10\cdot 10=100$$
21	20	oveq1i	$$⊢10\cdot 10A=100A$$
22	19 21	eqtri	$$⊢10A\cdot 10=100A$$
23	2 3	dpval3	Could not format ( B . C ) = _ B C : No typesetting found for |- ( B . C ) = _ B C with typecode |-
24	23	oveq1i	Could not format ( ( B . C ) x. ; 1 0 ) = ( _ B C x. ; 1 0 ) : No typesetting found for |- ( ( B . C ) x. ; 1 0 ) = ( _ B C x. ; 1 0 ) with typecode |-
25	2 3	dpmul10	Could not format ( ( B . C ) x. ; 1 0 ) = ; B C : No typesetting found for |- ( ( B . C ) x. ; 1 0 ) = ; B C with typecode |-
26	24 25	eqtr3i	Could not format ( _ B C x. ; 1 0 ) = ; B C : No typesetting found for |- ( _ B C x. ; 1 0 ) = ; B C with typecode |-
27	22 26	oveq12i	Could not format ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ; ; 1 0 0 x. A ) + ; B C ) : No typesetting found for |- ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ; ; 1 0 0 x. A ) + ; B C ) with typecode |-
28	1 6	dpmul10	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C with typecode |-
29		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 |-
30	28 29	eqtri	Could not format ( ( A . _ B C ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + _ B C ) : No typesetting found for |- ( ( A . _ B C ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + _ B C ) with typecode |-
31	30	oveq1i	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) : No typesetting found for |- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) with typecode |-
32	11 8	mulcli	$$⊢10A\in ℂ$$
33	32 9 11	adddiri	Could not format ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) : No typesetting found for |- ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) with typecode |-
34	31 33	eqtr2i	Could not format ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) : No typesetting found for |- ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) with typecode |-
35	18 27 34	3eqtr2ri	Could not format ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ; ; A B C : No typesetting found for |- ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ; ; A B C with typecode |-
36	20	oveq2i	Could not format ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( A . _ B C ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( A . _ B C ) x. ; ; 1 0 0 ) with typecode |-
37	17 35 36	3eqtr3ri	Could not format ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C : No typesetting found for |- ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C with typecode |-