Theorem dpmul

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

	Ref	Expression
Hypotheses	dpmul.a	⊢ 𝐴 ∈ ℕ0
	dpmul.b	⊢ 𝐵 ∈ ℕ0
	dpmul.c	⊢ 𝐶 ∈ ℕ0
	dpmul.d	⊢ 𝐷 ∈ ℕ0
	dpmul.e	⊢ 𝐸 ∈ ℕ0
	dpmul.g	⊢ 𝐺 ∈ ℕ0
	dpmul.j	⊢ 𝐽 ∈ ℕ0
	dpmul.k	⊢ 𝐾 ∈ ℕ0
	dpmul.1	⊢ ( 𝐴 · 𝐶 ) = 𝐹
	dpmul.2	⊢ ( 𝐴 · 𝐷 ) = 𝑀
	dpmul.3	⊢ ( 𝐵 · 𝐶 ) = 𝐿
	dpmul.4	⊢ ( 𝐵 · 𝐷 ) = ; 𝐸 𝐾
	dpmul.5	⊢ ( ( 𝐿 + 𝑀 ) + 𝐸 ) = ; 𝐺 𝐽
	dpmul.6	⊢ ( 𝐹 + 𝐺 ) = 𝐼
Assertion	dpmul	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) = ( 𝐼 . _ 𝐽 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		dpmul.a	⊢ 𝐴 ∈ ℕ0
2		dpmul.b	⊢ 𝐵 ∈ ℕ0
3		dpmul.c	⊢ 𝐶 ∈ ℕ0
4		dpmul.d	⊢ 𝐷 ∈ ℕ0
5		dpmul.e	⊢ 𝐸 ∈ ℕ0
6		dpmul.g	⊢ 𝐺 ∈ ℕ0
7		dpmul.j	⊢ 𝐽 ∈ ℕ0
8		dpmul.k	⊢ 𝐾 ∈ ℕ0
9		dpmul.1	⊢ ( 𝐴 · 𝐶 ) = 𝐹
10		dpmul.2	⊢ ( 𝐴 · 𝐷 ) = 𝑀
11		dpmul.3	⊢ ( 𝐵 · 𝐶 ) = 𝐿
12		dpmul.4	⊢ ( 𝐵 · 𝐷 ) = ; 𝐸 𝐾
13		dpmul.5	⊢ ( ( 𝐿 + 𝑀 ) + 𝐸 ) = ; 𝐺 𝐽
14		dpmul.6	⊢ ( 𝐹 + 𝐺 ) = 𝐼
15	1 2	deccl	⊢ ; 𝐴 𝐵 ∈ ℕ0
16		eqid	⊢ ; 𝐶 𝐷 = ; 𝐶 𝐷
17	1 4	nn0mulcli	⊢ ( 𝐴 · 𝐷 ) ∈ ℕ0
18	10 17	eqeltrri	⊢ 𝑀 ∈ ℕ0
19	18 5	nn0addcli	⊢ ( 𝑀 + 𝐸 ) ∈ ℕ0
20		eqid	⊢ ; 𝐴 𝐵 = ; 𝐴 𝐵
21	3 1 2 20 9 11	decmul1	⊢ ( ; 𝐴 𝐵 · 𝐶 ) = ; 𝐹 𝐿
22	21	oveq1i	⊢ ( ( ; 𝐴 𝐵 · 𝐶 ) + ( 𝑀 + 𝐸 ) ) = ( ; 𝐹 𝐿 + ( 𝑀 + 𝐸 ) )
23		dfdec10	⊢ ; 𝐹 𝐿 = ( ( ; 1 0 · 𝐹 ) + 𝐿 )
24	23	oveq1i	⊢ ( ; 𝐹 𝐿 + ( 𝑀 + 𝐸 ) ) = ( ( ( ; 1 0 · 𝐹 ) + 𝐿 ) + ( 𝑀 + 𝐸 ) )
25		10nn0	⊢ ; 1 0 ∈ ℕ0
26	25	nn0cni	⊢ ; 1 0 ∈ ℂ
27	1 3	nn0mulcli	⊢ ( 𝐴 · 𝐶 ) ∈ ℕ0
28	9 27	eqeltrri	⊢ 𝐹 ∈ ℕ0
29	28	nn0cni	⊢ 𝐹 ∈ ℂ
30	26 29	mulcli	⊢ ( ; 1 0 · 𝐹 ) ∈ ℂ
31	2 3	nn0mulcli	⊢ ( 𝐵 · 𝐶 ) ∈ ℕ0
32	11 31	eqeltrri	⊢ 𝐿 ∈ ℕ0
33	32	nn0cni	⊢ 𝐿 ∈ ℂ
34	19	nn0cni	⊢ ( 𝑀 + 𝐸 ) ∈ ℂ
35	30 33 34	addassi	⊢ ( ( ( ; 1 0 · 𝐹 ) + 𝐿 ) + ( 𝑀 + 𝐸 ) ) = ( ( ; 1 0 · 𝐹 ) + ( 𝐿 + ( 𝑀 + 𝐸 ) ) )
36	18	nn0cni	⊢ 𝑀 ∈ ℂ
37	5	nn0cni	⊢ 𝐸 ∈ ℂ
38	33 36 37	addassi	⊢ ( ( 𝐿 + 𝑀 ) + 𝐸 ) = ( 𝐿 + ( 𝑀 + 𝐸 ) )
39		dfdec10	⊢ ; 𝐺 𝐽 = ( ( ; 1 0 · 𝐺 ) + 𝐽 )
40	13 38 39	3eqtr3ri	⊢ ( ( ; 1 0 · 𝐺 ) + 𝐽 ) = ( 𝐿 + ( 𝑀 + 𝐸 ) )
41	40	oveq2i	⊢ ( ( ; 1 0 · 𝐹 ) + ( ( ; 1 0 · 𝐺 ) + 𝐽 ) ) = ( ( ; 1 0 · 𝐹 ) + ( 𝐿 + ( 𝑀 + 𝐸 ) ) )
42		dfdec10	⊢ ; 𝐼 𝐽 = ( ( ; 1 0 · 𝐼 ) + 𝐽 )
43	6	nn0cni	⊢ 𝐺 ∈ ℂ
44	26 29 43	adddii	⊢ ( ; 1 0 · ( 𝐹 + 𝐺 ) ) = ( ( ; 1 0 · 𝐹 ) + ( ; 1 0 · 𝐺 ) )
45	14	oveq2i	⊢ ( ; 1 0 · ( 𝐹 + 𝐺 ) ) = ( ; 1 0 · 𝐼 )
46	44 45	eqtr3i	⊢ ( ( ; 1 0 · 𝐹 ) + ( ; 1 0 · 𝐺 ) ) = ( ; 1 0 · 𝐼 )
47	46	oveq1i	⊢ ( ( ( ; 1 0 · 𝐹 ) + ( ; 1 0 · 𝐺 ) ) + 𝐽 ) = ( ( ; 1 0 · 𝐼 ) + 𝐽 )
48	26 43	mulcli	⊢ ( ; 1 0 · 𝐺 ) ∈ ℂ
49	7	nn0cni	⊢ 𝐽 ∈ ℂ
50	30 48 49	addassi	⊢ ( ( ( ; 1 0 · 𝐹 ) + ( ; 1 0 · 𝐺 ) ) + 𝐽 ) = ( ( ; 1 0 · 𝐹 ) + ( ( ; 1 0 · 𝐺 ) + 𝐽 ) )
51	42 47 50	3eqtr2ri	⊢ ( ( ; 1 0 · 𝐹 ) + ( ( ; 1 0 · 𝐺 ) + 𝐽 ) ) = ; 𝐼 𝐽
52	35 41 51	3eqtr2i	⊢ ( ( ( ; 1 0 · 𝐹 ) + 𝐿 ) + ( 𝑀 + 𝐸 ) ) = ; 𝐼 𝐽
53	22 24 52	3eqtri	⊢ ( ( ; 𝐴 𝐵 · 𝐶 ) + ( 𝑀 + 𝐸 ) ) = ; 𝐼 𝐽
54	10	oveq1i	⊢ ( ( 𝐴 · 𝐷 ) + 𝐸 ) = ( 𝑀 + 𝐸 )
55	4 1 2 20 8 5 54 12	decmul1c	⊢ ( ; 𝐴 𝐵 · 𝐷 ) = ; ( 𝑀 + 𝐸 ) 𝐾
56	15 3 4 16 8 19 53 55	decmul2c	⊢ ( ; 𝐴 𝐵 · ; 𝐶 𝐷 ) = ; ; 𝐼 𝐽 𝐾
57	2	nn0rei	⊢ 𝐵 ∈ ℝ
58		dpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )
59	1 57 58	mp2an	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ
60	59	recni	⊢ ( 𝐴 . 𝐵 ) ∈ ℂ
61	4	nn0rei	⊢ 𝐷 ∈ ℝ
62		dpcl	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ ) → ( 𝐶 . 𝐷 ) ∈ ℝ )
63	3 61 62	mp2an	⊢ ( 𝐶 . 𝐷 ) ∈ ℝ
64	63	recni	⊢ ( 𝐶 . 𝐷 ) ∈ ℂ
65	60 64 26 26	mul4i	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ( ; 1 0 · ; 1 0 ) ) = ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) · ( ( 𝐶 . 𝐷 ) · ; 1 0 ) )
66	25	dec0u	⊢ ( ; 1 0 · ; 1 0 ) = ; ; 1 0 0
67	66	oveq2i	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ( ; 1 0 · ; 1 0 ) ) = ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ; ; 1 0 0 )
68	1 57	dpmul10	⊢ ( ( 𝐴 . 𝐵 ) · ; 1 0 ) = ; 𝐴 𝐵
69	3 61	dpmul10	⊢ ( ( 𝐶 . 𝐷 ) · ; 1 0 ) = ; 𝐶 𝐷
70	68 69	oveq12i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) · ( ( 𝐶 . 𝐷 ) · ; 1 0 ) ) = ( ; 𝐴 𝐵 · ; 𝐶 𝐷 )
71	65 67 70	3eqtr3i	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ; ; 1 0 0 ) = ( ; 𝐴 𝐵 · ; 𝐶 𝐷 )
72	28 6	nn0addcli	⊢ ( 𝐹 + 𝐺 ) ∈ ℕ0
73	14 72	eqeltrri	⊢ 𝐼 ∈ ℕ0
74	8	nn0rei	⊢ 𝐾 ∈ ℝ
75	73 7 74	dpmul100	⊢ ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) = ; ; 𝐼 𝐽 𝐾
76	56 71 75	3eqtr4i	⊢ ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ; ; 1 0 0 ) = ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 )
77	60 64	mulcli	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) ∈ ℂ
78	7	nn0rei	⊢ 𝐽 ∈ ℝ
79		dp2cl	⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → _ 𝐽 𝐾 ∈ ℝ )
80	78 74 79	mp2an	⊢ _ 𝐽 𝐾 ∈ ℝ
81		dpcl	⊢ ( ( 𝐼 ∈ ℕ0 ∧ _ 𝐽 𝐾 ∈ ℝ ) → ( 𝐼 . _ 𝐽 𝐾 ) ∈ ℝ )
82	73 80 81	mp2an	⊢ ( 𝐼 . _ 𝐽 𝐾 ) ∈ ℝ
83	82	recni	⊢ ( 𝐼 . _ 𝐽 𝐾 ) ∈ ℂ
84		10nn	⊢ ; 1 0 ∈ ℕ
85	84	decnncl2	⊢ ; ; 1 0 0 ∈ ℕ
86	85	nncni	⊢ ; ; 1 0 0 ∈ ℂ
87	85	nnne0i	⊢ ; ; 1 0 0 ≠ 0
88	86 87	pm3.2i	⊢ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 )
89		mulcan2	⊢ ( ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) ∈ ℂ ∧ ( 𝐼 . _ 𝐽 𝐾 ) ∈ ℂ ∧ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 ) ) → ( ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ; ; 1 0 0 ) = ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) ↔ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) = ( 𝐼 . _ 𝐽 𝐾 ) ) )
90	77 83 88 89	mp3an	⊢ ( ( ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) · ; ; 1 0 0 ) = ( ( 𝐼 . _ 𝐽 𝐾 ) · ; ; 1 0 0 ) ↔ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) = ( 𝐼 . _ 𝐽 𝐾 ) )
91	76 90	mpbi	⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) = ( 𝐼 . _ 𝐽 𝐾 )