Theorem decsubi

Description: Difference between a numeral M and a nonnegative integer N (no underflow). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decaddi.1	$$⊢A\in {\mathbb{N}}_0$$
	decaddi.2	$$⊢B\in {\mathbb{N}}_0$$
	decaddi.3	$$⊢N\in {\mathbb{N}}_0$$
	decaddi.4	No typesetting found for |- M = ; A B with typecode |-
	decaddci.5	$$⊢A+1=D$$
	decsubi.5	$$⊢B-N=C$$
Assertion	decsubi	Could not format assertion : No typesetting found for |- ( M - N ) = ; A C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decaddi.1	$$⊢A\in {\mathbb{N}}_0$$
2		decaddi.2	$$⊢B\in {\mathbb{N}}_0$$
3		decaddi.3	$$⊢N\in {\mathbb{N}}_0$$
4		decaddi.4	Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
5		decaddci.5	$$⊢A+1=D$$
6		decsubi.5	$$⊢B-N=C$$
7		10nn0	$$⊢10\in {\mathbb{N}}_0$$
8	7 1	nn0mulcli	$$⊢10A\in {\mathbb{N}}_0$$
9	8	nn0cni	$$⊢10A\in ℂ$$
10	2	nn0cni	$$⊢B\in ℂ$$
11	3	nn0cni	$$⊢N\in ℂ$$
12	9 10 11	addsubassi	$$⊢10A+B-N=10A+B-N$$
13		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
14	4 13	eqtri	$$⊢M=10A+B$$
15	14	oveq1i	$$⊢M-N=10A+B-N$$
16		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
17	6	eqcomi	$$⊢C=B-N$$
18	17	oveq2i	$$⊢10A+C=10A+B-N$$
19	16 18	eqtri	Could not format ; A C = ( ( ; 1 0 x. A ) + ( B - N ) ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + ( B - N ) ) with typecode |-
20	12 15 19	3eqtr4i	Could not format ( M - N ) = ; A C : No typesetting found for |- ( M - N ) = ; A C with typecode |-