Theorem sub1m1

Description: Subtracting two times 1 from a number. (Contributed by AV, 23-Oct-2018)

	Ref	Expression
Assertion	sub1m1	$$⊢N\in ℂ\to N-1-1=N-2$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢N\in ℂ\to N\in ℂ$$
2		1cnd	$$⊢N\in ℂ\to 1\in ℂ$$
3	1 2 2	subsub4d	$$⊢N\in ℂ\to N-1-1=N-\left(1+1\right)$$
4		1p1e2	$$⊢1+1=2$$
5	4	a1i	$$⊢N\in ℂ\to 1+1=2$$
6	5	oveq2d	$$⊢N\in ℂ\to N-\left(1+1\right)=N-2$$
7	3 6	eqtrd	$$⊢N\in ℂ\to N-1-1=N-2$$