Metamath Proof Explorer

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 ⊢ ( ( 𝐴 . 𝐵 ) · ( 𝐶 . 𝐷 ) ) = ( 𝐼 . 𝐽 𝐾 )