Theorem dpmul1000

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

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

Proof

Step	Hyp	Ref	Expression
1		dpmul1000.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpmul1000.b	$$⊢B\in {\mathbb{N}}_0$$
3		dpmul1000.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpmul1000.d	$$⊢D\in ℝ$$
5	2	nn0rei	$$⊢B\in ℝ$$
6	3	nn0rei	$$⊢C\in ℝ$$
7		dp2cl	Could not format ( ( C e. RR /\ D e. RR ) -> _ C D e. RR ) : No typesetting found for |- ( ( C e. RR /\ D e. RR ) -> _ C D e. RR ) with typecode |-
8	6 4 7	mp2an	Could not format _ C D e. RR : No typesetting found for |- _ C D e. RR with typecode |-
9		dp2cl	Could not format ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR ) : No typesetting found for |- ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR ) with typecode |-
10	5 8 9	mp2an	Could not format _ B _ C D e. RR : No typesetting found for |- _ B _ C D e. RR with typecode |-
11		dpcl	Could not format ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR ) : No typesetting found for |- ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR ) with typecode |-
12	1 10 11	mp2an	Could not format ( A . _ B _ C D ) e. RR : No typesetting found for |- ( A . _ B _ C D ) e. RR with typecode |-
13	12	recni	Could not format ( A . _ B _ C D ) e. CC : No typesetting found for |- ( A . _ B _ C D ) e. CC with typecode |-
14		10nn0	$$⊢10\in {\mathbb{N}}_0$$
15		0nn0	$$⊢0\in {\mathbb{N}}_0$$
16	14 15	deccl	$$⊢100\in {\mathbb{N}}_0$$
17	16	nn0cni	$$⊢100\in ℂ$$
18	14	nn0cni	$$⊢10\in ℂ$$
19	13 17 18	mulassi	Could not format ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) ) with typecode |-
20	1 2 8	dpmul100	Could not format ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) = ; ; A B _ C D : No typesetting found for |- ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) = ; ; A B _ C D with typecode |-
21	20	oveq1i	Could not format ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ; ; A B _ C D x. ; 1 0 ) : No typesetting found for |- ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ; ; A B _ C D x. ; 1 0 ) with typecode |-
22	16	dec0u	$$⊢10\cdot 100=1000$$
23	18 17 22	mulcomli	$$⊢100\cdot 10=1000$$
24	23	oveq2i	Could not format ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) with typecode |-
25	19 21 24	3eqtr3i	Could not format ( ; ; A B _ C D x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) : No typesetting found for |- ( ; ; A B _ C D x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) with typecode |-
26		dfdec10	Could not format ; ; A B _ C D = ( ( ; 1 0 x. ; A B ) + _ C D ) : No typesetting found for |- ; ; A B _ C D = ( ( ; 1 0 x. ; A B ) + _ C D ) with typecode |-
27	26	oveq1i	Could not format ( ; ; A B _ C D x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 ) : No typesetting found for |- ( ; ; A B _ C D x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 ) with typecode |-
28	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
29	28	nn0cni	Could not format ; A B e. CC : No typesetting found for |- ; A B e. CC with typecode |-
30	18 29	mulcli	Could not format ( ; 1 0 x. ; A B ) e. CC : No typesetting found for |- ( ; 1 0 x. ; A B ) e. CC with typecode |-
31	8	recni	Could not format _ C D e. CC : No typesetting found for |- _ C D e. CC with typecode |-
32	30 31 18	adddiri	Could not format ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) : No typesetting found for |- ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) with typecode |-
33	28 3 4	dfdec100	Could not format ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) : No typesetting found for |- ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) with typecode |-
34	14	dec0u	$$⊢10\cdot 10=100$$
35	34	oveq1i	Could not format ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ; ; 1 0 0 x. ; A B ) : No typesetting found for |- ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ; ; 1 0 0 x. ; A B ) with typecode |-
36	18 18 29	mul32i	Could not format ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) : No typesetting found for |- ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) with typecode |-
37	35 36	eqtr3i	Could not format ( ; ; 1 0 0 x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) : No typesetting found for |- ( ; ; 1 0 0 x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) with typecode |-
38	3 4	dpmul10	Could not format ( ( C . D ) x. ; 1 0 ) = ; C D : No typesetting found for |- ( ( C . D ) x. ; 1 0 ) = ; C D with typecode |-
39		dpval	Could not format ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D ) : No typesetting found for |- ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D ) with typecode |-
40	3 4 39	mp2an	Could not format ( C . D ) = _ C D : No typesetting found for |- ( C . D ) = _ C D with typecode |-
41	40	oveq1i	Could not format ( ( C . D ) x. ; 1 0 ) = ( _ C D x. ; 1 0 ) : No typesetting found for |- ( ( C . D ) x. ; 1 0 ) = ( _ C D x. ; 1 0 ) with typecode |-
42	38 41	eqtr3i	Could not format ; C D = ( _ C D x. ; 1 0 ) : No typesetting found for |- ; C D = ( _ C D x. ; 1 0 ) with typecode |-
43	37 42	oveq12i	Could not format ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) : No typesetting found for |- ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) with typecode |-
44	33 43	eqtr2i	Could not format ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) = ; ; ; A B C D : No typesetting found for |- ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) = ; ; ; A B C D with typecode |-
45	27 32 44	3eqtri	Could not format ( ; ; A B _ C D x. ; 1 0 ) = ; ; ; A B C D : No typesetting found for |- ( ; ; A B _ C D x. ; 1 0 ) = ; ; ; A B C D with typecode |-
46	25 45	eqtr3i	Could not format ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D : No typesetting found for |- ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D with typecode |-