Theorem decmul2c

Description: The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decmul1.p	$$⊢P\in {\mathbb{N}}_0$$
	decmul1.a	$$⊢A\in {\mathbb{N}}_0$$
	decmul1.b	$$⊢B\in {\mathbb{N}}_0$$
	decmul1.n	No typesetting found for |- N = ; A B with typecode |-
	decmul1.0	$$⊢D\in {\mathbb{N}}_0$$
	decmul1c.e	$$⊢E\in {\mathbb{N}}_0$$
	decmul2c.c	$$⊢PA+E=C$$
	decmul2c.2	No typesetting found for |- ( P x. B ) = ; E D with typecode |-
Assertion	decmul2c	Could not format assertion : No typesetting found for |- ( P x. N ) = ; C D with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decmul1.p	$$⊢P\in {\mathbb{N}}_0$$
2		decmul1.a	$$⊢A\in {\mathbb{N}}_0$$
3		decmul1.b	$$⊢B\in {\mathbb{N}}_0$$
4		decmul1.n	Could not format N = ; A B : No typesetting found for |- N = ; A B with typecode |-
5		decmul1.0	$$⊢D\in {\mathbb{N}}_0$$
6		decmul1c.e	$$⊢E\in {\mathbb{N}}_0$$
7		decmul2c.c	$$⊢PA+E=C$$
8		decmul2c.2	Could not format ( P x. B ) = ; E D : No typesetting found for |- ( P x. B ) = ; E D with typecode |-
9		10nn0	$$⊢10\in {\mathbb{N}}_0$$
10		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
11	4 10	eqtri	$$⊢N=10A+B$$
12		dfdec10	Could not format ; E D = ( ( ; 1 0 x. E ) + D ) : No typesetting found for |- ; E D = ( ( ; 1 0 x. E ) + D ) with typecode |-
13	8 12	eqtri	$$⊢PB=10E+D$$
14	9 1 2 3 11 5 6 7 13	nummul2c	$$⊢P\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=10C+D$$
15		dfdec10	Could not format ; C D = ( ( ; 1 0 x. C ) + D ) : No typesetting found for |- ; C D = ( ( ; 1 0 x. C ) + D ) with typecode |-
16	14 15	eqtr4i	Could not format ( P x. N ) = ; C D : No typesetting found for |- ( P x. N ) = ; C D with typecode |-