Metamath Proof Explorer


Theorem dpmul

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

Ref Expression
Hypotheses dpmul.a A 0
dpmul.b B 0
dpmul.c C 0
dpmul.d D 0
dpmul.e E 0
dpmul.g G 0
dpmul.j J 0
dpmul.k K 0
dpmul.1 A C = F
dpmul.2 A D = M
dpmul.3 B C = 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 0
2 dpmul.b B 0
3 dpmul.c C 0
4 dpmul.d D 0
5 dpmul.e E 0
6 dpmul.g G 0
7 dpmul.j J 0
8 dpmul.k K 0
9 dpmul.1 A C = F
10 dpmul.2 A D = M
11 dpmul.3 B C = 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 A D 0
18 10 17 eqeltrri M 0
19 18 5 nn0addcli M + E 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 0
26 25 nn0cni 10
27 1 3 nn0mulcli A C 0
28 9 27 eqeltrri F 0
29 28 nn0cni F
30 26 29 mulcli 10 F
31 2 3 nn0mulcli B C 0
32 11 31 eqeltrri L 0
33 32 nn0cni L
34 19 nn0cni M + E
35 30 33 34 addassi 10 F + L + M + E = 10 F + L + M + E
36 18 nn0cni M
37 5 nn0cni E
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 10 G + J = L + M + E
41 40 oveq2i 10 F + 10 G + J = 10 F + L + M + E
42 dfdec10 IJ = 10 I + J
43 6 nn0cni G
44 26 29 43 adddii 10 F + G = 10 F + 10 G
45 14 oveq2i 10 F + G = 10 I
46 44 45 eqtr3i 10 F + 10 G = 10 I
47 46 oveq1i 10 F + 10 G + J = 10 I + J
48 26 43 mulcli 10 G
49 7 nn0cni J
50 30 48 49 addassi 10 F + 10 G + J = 10 F + 10 G + J
51 42 47 50 3eqtr2ri 10 F + 10 G + J = IJ
52 35 41 51 3eqtr2i 10 F + L + M + E = IJ
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 A D + 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
58 dpcl A 0 B A . B
59 1 57 58 mp2an A . B
60 59 recni A . B
61 4 nn0rei D
62 dpcl C 0 D C . D
63 3 61 62 mp2an C . D
64 63 recni C . D
65 60 64 26 26 mul4i A . B C . D 10 10 = A . B 10 C . D 10
66 25 dec0u 10 10 = 100
67 66 oveq2i A . B C . D 10 10 = A . B C . D 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 0
73 14 72 eqeltrri I 0
74 8 nn0rei K
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 A . B C . D
78 7 nn0rei J
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
85 84 decnncl2 100
86 85 nncni 100
87 85 nnne0i 100 0
88 86 87 pm3.2i 100 100 0
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 |-