This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )