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

Metamath Proof Explorer

Theorem decmul1

Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021) Remove hypothesis D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)

		Ref	Expression
	Hypotheses	decmul1.p	$⊢ P \in ℕ_{0}$
		decmul1.a	$⊢ A \in ℕ_{0}$
		decmul1.b	$⊢ B \in ℕ_{0}$
		decmul1.n	No typesetting found for \|- N = ; A B with typecode \|-
		decmul1.c	$⊢ A P = C$
		decmul1.d	$⊢ B P = D$
	Assertion	decmul1	Could not format assertion : No typesetting found for \|- ( N x. P ) = ; C D with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		decmul1.p	$⊢ P \in ℕ_{0}$
2		decmul1.a	$⊢ A \in ℕ_{0}$
3		decmul1.b	$⊢ B \in ℕ_{0}$
4		decmul1.n	Could not format N = ; A B : No typesetting found for \|- N = ; A B with typecode \|-
5		decmul1.c	$⊢ A P = C$
6		decmul1.d	$⊢ B P = D$
7	2 3	deccl	Could not format ; A B e. NN0 : No typesetting found for \|- ; A B e. NN0 with typecode \|-
8	4 7	eqeltri	$⊢ N \in ℕ_{0}$
9	8 1	num0u	$⊢ N P = N P + 0$
10		0nn0	$⊢ 0 \in ℕ_{0}$
11	3 1	nn0mulcli	$⊢ B P \in ℕ_{0}$
12	11	nn0cni	$⊢ B P \in ℂ$
13	12	addridi	$⊢ B P + 0 = B P$
14	13 6	eqtri	$⊢ B P + 0 = D$
15	2 3 10 4 1 5 14	decrmanc	Could not format ( ( N x. P ) + 0 ) = ; C D : No typesetting found for \|- ( ( N x. P ) + 0 ) = ; C D with typecode \|-
16	9 15	eqtri	Could not format ( N x. P ) = ; C D : No typesetting found for \|- ( N x. P ) = ; C D with typecode \|-