dpmul

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

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

Metamath Proof Explorer

Theorem dpmul

Proof