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 ℕ_{0}$
	decaddi.2	$⊢ B \in ℕ_{0}$
	decaddi.3	$⊢ N \in ℕ_{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 ℕ_{0}$
2		decaddi.2	$⊢ B \in ℕ_{0}$
3		decaddi.3	$⊢ N \in ℕ_{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 ℕ_{0}$
8	7 1	nn0mulcli	$⊢ 10 A \in ℕ_{0}$
9	8	nn0cni	$⊢ 10 A \in ℂ$
10	2	nn0cni	$⊢ B \in ℂ$
11	3	nn0cni	$⊢ N \in ℂ$
12	9 10 11	addsubassi	$⊢ 10 A + B - N = 10 A + 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 = 10 A + B$
15	14	oveq1i	$⊢ M - N = 10 A + 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	$⊢ 10 A + C = 10 A + 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 \|-

Metamath Proof Explorer

Theorem decsubi

Proof