Theorem dpmul

Description: Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021)

	Ref	Expression
Hypotheses	dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
	dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
	dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
	dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
	dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
	dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
	dpmul.j	$$⊢J\in {\mathbb{N}}_0$$
	dpmul.k	$$⊢K\in {\mathbb{N}}_0$$
	dpmul.1	$$⊢AC=F$$
	dpmul.2	$$⊢AD=M$$
	dpmul.3	$$⊢BC=L$$
	dpmul.4	No typesetting found for |- ( B x. D ) = ; E K with typecode |-
	dpmul.5	No typesetting found for |- ( ( L + M ) + E ) = ; G J with typecode |-
	dpmul.6	$$⊢F+G=I$$
Assertion	dpmul	Could not format assertion : No typesetting found for |- ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpmul.b	$$⊢B\in {\mathbb{N}}_0$$
3		dpmul.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpmul.d	$$⊢D\in {\mathbb{N}}_0$$
5		dpmul.e	$$⊢E\in {\mathbb{N}}_0$$
6		dpmul.g	$$⊢G\in {\mathbb{N}}_0$$
7		dpmul.j	$$⊢J\in {\mathbb{N}}_0$$
8		dpmul.k	$$⊢K\in {\mathbb{N}}_0$$
9		dpmul.1	$$⊢AC=F$$
10		dpmul.2	$$⊢AD=M$$
11		dpmul.3	$$⊢BC=L$$
12		dpmul.4	Could not format ( B x. D ) = ; E K : No typesetting found for |- ( B x. D ) = ; E K with typecode |-
13		dpmul.5	Could not format ( ( L + M ) + E ) = ; G J : No typesetting found for |- ( ( L + M ) + E ) = ; G J with typecode |-
14		dpmul.6	$$⊢F+G=I$$
15	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
16		eqid	Could not format ; C D = ; C D : No typesetting found for |- ; C D = ; C D with typecode |-
17	1 4	nn0mulcli	$$⊢AD\in {\mathbb{N}}_0$$
18	10 17	eqeltrri	$$⊢M\in {\mathbb{N}}_0$$
19	18 5	nn0addcli	$$⊢M+E\in {\mathbb{N}}_0$$
20		eqid	Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
21	3 1 2 20 9 11	decmul1	Could not format ( ; A B x. C ) = ; F L : No typesetting found for |- ( ; A B x. C ) = ; F L with typecode |-
22	21	oveq1i	Could not format ( ( ; A B x. C ) + ( M + E ) ) = ( ; F L + ( M + E ) ) : No typesetting found for |- ( ( ; A B x. C ) + ( M + E ) ) = ( ; F L + ( M + E ) ) with typecode |-
23		dfdec10	Could not format ; F L = ( ( ; 1 0 x. F ) + L ) : No typesetting found for |- ; F L = ( ( ; 1 0 x. F ) + L ) with typecode |-
24	23	oveq1i	Could not format ( ; F L + ( M + E ) ) = ( ( ( ; 1 0 x. F ) + L ) + ( M + E ) ) : No typesetting found for |- ( ; F L + ( M + E ) ) = ( ( ( ; 1 0 x. F ) + L ) + ( M + E ) ) with typecode |-
25		10nn0	$$⊢10\in {\mathbb{N}}_0$$
26	25	nn0cni	$$⊢10\in ℂ$$
27	1 3	nn0mulcli	$$⊢AC\in {\mathbb{N}}_0$$
28	9 27	eqeltrri	$$⊢F\in {\mathbb{N}}_0$$
29	28	nn0cni	$$⊢F\in ℂ$$
30	26 29	mulcli	$$⊢10F\in ℂ$$
31	2 3	nn0mulcli	$$⊢BC\in {\mathbb{N}}_0$$
32	11 31	eqeltrri	$$⊢L\in {\mathbb{N}}_0$$
33	32	nn0cni	$$⊢L\in ℂ$$
34	19	nn0cni	$$⊢M+E\in ℂ$$
35	30 33 34	addassi	$$⊢10F+L+M+E=10F+L+\left(M+E\right)$$
36	18	nn0cni	$$⊢M\in ℂ$$
37	5	nn0cni	$$⊢E\in ℂ$$
38	33 36 37	addassi	$$⊢L+M+E=L+M+E$$
39		dfdec10	Could not format ; G J = ( ( ; 1 0 x. G ) + J ) : No typesetting found for |- ; G J = ( ( ; 1 0 x. G ) + J ) with typecode |-
40	13 38 39	3eqtr3ri	$$⊢10G+J=L+M+E$$
41	40	oveq2i	$$⊢10F+10G+J=10F+L+\left(M+E\right)$$
42		dfdec10	$$⊢\mathrm{<mi\; mathcolor="\#808">I</mi><mi\; mathcolor="\#808">J</mi>}=10\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}+J$$
43	6	nn0cni	$$⊢G\in ℂ$$
44	26 29 43	adddii	$$⊢10\left(F+G\right)=10F+10G$$
45	14	oveq2i	$$⊢10\left(F+G\right)=10\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}$$
46	44 45	eqtr3i	$$⊢10F+10G=10\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}$$
47	46	oveq1i	$$⊢10F+10G+J=10\cdot \mathrm{<mi\; mathcolor="\#808">I</mi>}+J$$
48	26 43	mulcli	$$⊢10G\in ℂ$$
49	7	nn0cni	$$⊢J\in ℂ$$
50	30 48 49	addassi	$$⊢10F+10G+J=10F+10G+J$$
51	42 47 50	3eqtr2ri	$$⊢10F+10G+J=\mathrm{<mi\; mathcolor="\#808">I</mi><mi\; mathcolor="\#808">J</mi>}$$
52	35 41 51	3eqtr2i	$$⊢10F+L+M+E=\mathrm{<mi\; mathcolor="\#808">I</mi><mi\; mathcolor="\#808">J</mi>}$$
53	22 24 52	3eqtri	Could not format ( ( ; A B x. C ) + ( M + E ) ) = ; I J : No typesetting found for |- ( ( ; A B x. C ) + ( M + E ) ) = ; I J with typecode |-
54	10	oveq1i	$$⊢AD+E=M+E$$
55	4 1 2 20 8 5 54 12	decmul1c	Could not format ( ; A B x. D ) = ; ( M + E ) K : No typesetting found for |- ( ; A B x. D ) = ; ( M + E ) K with typecode |-
56	15 3 4 16 8 19 53 55	decmul2c	Could not format ( ; A B x. ; C D ) = ; ; I J K : No typesetting found for |- ( ; A B x. ; C D ) = ; ; I J K with typecode |-
57	2	nn0rei	$$⊢B\in ℝ$$
58		dpcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$
59	1 57 58	mp2an	$$⊢A.B\in ℝ$$
60	59	recni	$$⊢A.B\in ℂ$$
61	4	nn0rei	$$⊢D\in ℝ$$
62		dpcl	$$⊢\left(C\in {\mathbb{N}}_0\wedge D\in ℝ\right)\to C.D\in ℝ$$
63	3 61 62	mp2an	$$⊢C.D\in ℝ$$
64	63	recni	$$⊢C.D\in ℂ$$
65	60 64 26 26	mul4i	$$⊢\left(A.B\right)\left(C.D\right)10\cdot 10=\left(A.B\right)\cdot 10\left(C.D\right)\cdot 10$$
66	25	dec0u	$$⊢10\cdot 10=100$$
67	66	oveq2i	$$⊢\left(A.B\right)\left(C.D\right)10\cdot 10=\left(A.B\right)\left(C.D\right)\cdot 100$$
68	1 57	dpmul10	Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-
69	3 61	dpmul10	Could not format ( ( C . D ) x. ; 1 0 ) = ; C D : No typesetting found for |- ( ( C . D ) x. ; 1 0 ) = ; C D with typecode |-
70	68 69	oveq12i	Could not format ( ( ( A . B ) x. ; 1 0 ) x. ( ( C . D ) x. ; 1 0 ) ) = ( ; A B x. ; C D ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) x. ( ( C . D ) x. ; 1 0 ) ) = ( ; A B x. ; C D ) with typecode |-
71	65 67 70	3eqtr3i	Could not format ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ; A B x. ; C D ) : No typesetting found for |- ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ; A B x. ; C D ) with typecode |-
72	28 6	nn0addcli	$$⊢F+G\in {\mathbb{N}}_0$$
73	14 72	eqeltrri	$$⊢I\in {\mathbb{N}}_0$$
74	8	nn0rei	$$⊢K\in ℝ$$
75	73 7 74	dpmul100	Could not format ( ( I . _ J K ) x. ; ; 1 0 0 ) = ; ; I J K : No typesetting found for |- ( ( I . _ J K ) x. ; ; 1 0 0 ) = ; ; I J K with typecode |-
76	56 71 75	3eqtr4i	Could not format ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) : No typesetting found for |- ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) with typecode |-
77	60 64	mulcli	$$⊢\left(A.B\right)\left(C.D\right)\in ℂ$$
78	7	nn0rei	$$⊢J\in ℝ$$
79		dp2cl	Could not format ( ( J e. RR /\ K e. RR ) -> _ J K e. RR ) : No typesetting found for |- ( ( J e. RR /\ K e. RR ) -> _ J K e. RR ) with typecode |-
80	78 74 79	mp2an	Could not format _ J K e. RR : No typesetting found for |- _ J K e. RR with typecode |-
81		dpcl	Could not format ( ( I e. NN0 /\ _ J K e. RR ) -> ( I . _ J K ) e. RR ) : No typesetting found for |- ( ( I e. NN0 /\ _ J K e. RR ) -> ( I . _ J K ) e. RR ) with typecode |-
82	73 80 81	mp2an	Could not format ( I . _ J K ) e. RR : No typesetting found for |- ( I . _ J K ) e. RR with typecode |-
83	82	recni	Could not format ( I . _ J K ) e. CC : No typesetting found for |- ( I . _ J K ) e. CC with typecode |-
84		10nn	$$⊢10\in \mathbb{N}$$
85	84	decnncl2	$$⊢100\in \mathbb{N}$$
86	85	nncni	$$⊢100\in ℂ$$
87	85	nnne0i	$$⊢100\ne 0$$
88	86 87	pm3.2i	$$⊢\left(100\in ℂ\wedge 100\ne 0\right)$$
89		mulcan2	Could not format ( ( ( ( A . B ) x. ( C . D ) ) e. CC /\ ( I . _ J K ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) ) : No typesetting found for |- ( ( ( ( A . B ) x. ( C . D ) ) e. CC /\ ( I . _ J K ) e. CC /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) ) with typecode |-
90	77 83 88 89	mp3an	Could not format ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) : No typesetting found for |- ( ( ( ( A . B ) x. ( C . D ) ) x. ; ; 1 0 0 ) = ( ( I . _ J K ) x. ; ; 1 0 0 ) <-> ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) ) with typecode |-
91	76 90	mpbi	Could not format ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) : No typesetting found for |- ( ( A . B ) x. ( C . D ) ) = ( I . _ J K ) with typecode |-