Metamath Proof Explorer


Theorem dpmul

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

Ref Expression
Hypotheses dpmul.a
|- A e. NN0
dpmul.b
|- B e. NN0
dpmul.c
|- C e. NN0
dpmul.d
|- D e. NN0
dpmul.e
|- E e. NN0
dpmul.g
|- G e. NN0
dpmul.j
|- J e. NN0
dpmul.k
|- K e. NN0
dpmul.1
|- ( A x. C ) = F
dpmul.2
|- ( A x. D ) = M
dpmul.3
|- ( B x. C ) = L
dpmul.4
|- ( B x. D ) = ; E K
dpmul.5
|- ( ( L + M ) + E ) = ; G J
dpmul.6
|- ( F + G ) = I
Assertion dpmul
|- ( ( A . B ) x. ( C . D ) ) = ( I . _ J K )

Proof

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