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 e. NN0
	decaddi.2	\|- B e. NN0
	decaddi.3	\|- N e. NN0
	decaddi.4	\|- M = ; A B
	decaddci.5	\|- ( A + 1 ) = D
	decsubi.5	\|- ( B - N ) = C
Assertion	decsubi	\|- ( M - N ) = ; A C

Proof

Step	Hyp	Ref	Expression
1		decaddi.1	\|- A e. NN0
2		decaddi.2	\|- B e. NN0
3		decaddi.3	\|- N e. NN0
4		decaddi.4	\|- M = ; A B
5		decaddci.5	\|- ( A + 1 ) = D
6		decsubi.5	\|- ( B - N ) = C
7		10nn0	\|- ; 1 0 e. NN0
8	7 1	nn0mulcli	\|- ( ; 1 0 x. A ) e. NN0
9	8	nn0cni	\|- ( ; 1 0 x. A ) e. CC
10	2	nn0cni	\|- B e. CC
11	3	nn0cni	\|- N e. CC
12	9 10 11	addsubassi	\|- ( ( ( ; 1 0 x. A ) + B ) - N ) = ( ( ; 1 0 x. A ) + ( B - N ) )
13		dfdec10	\|- ; A B = ( ( ; 1 0 x. A ) + B )
14	4 13	eqtri	\|- M = ( ( ; 1 0 x. A ) + B )
15	14	oveq1i	\|- ( M - N ) = ( ( ( ; 1 0 x. A ) + B ) - N )
16		dfdec10	\|- ; A C = ( ( ; 1 0 x. A ) + C )
17	6	eqcomi	\|- C = ( B - N )
18	17	oveq2i	\|- ( ( ; 1 0 x. A ) + C ) = ( ( ; 1 0 x. A ) + ( B - N ) )
19	16 18	eqtri	\|- ; A C = ( ( ; 1 0 x. A ) + ( B - N ) )
20	12 15 19	3eqtr4i	\|- ( M - N ) = ; A C

Metamath Proof Explorer

Theorem decsubi

Proof