This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sub1m1

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

Ref Expression
Assertion sub1m1 ⊢ N ∈ ℂ → N - 1 - 1 = N − 2

Proof

Step Hyp Ref Expression
1 id ⊢ N ∈ ℂ → N ∈ ℂ
2 1cnd ⊢ N ∈ ℂ → 1 ∈ ℂ
3 1 2 2 subsub4d ⊢ N ∈ ℂ → N - 1 - 1 = N − 1 + 1
4 1p1e2 ⊢ 1 + 1 = 2
5 4 a1i ⊢ N ∈ ℂ → 1 + 1 = 2
6 5 oveq2d ⊢ N ∈ ℂ → N − 1 + 1 = N − 2
7 3 6 eqtrd ⊢ N ∈ ℂ → N - 1 - 1 = N − 2