Metamath Proof Explorer


Theorem cnm2m1cnm3

Description: Subtracting 2 and afterwards 1 from a number results in the difference between the number and 3. (Contributed by Alexander van der Vekens, 16-Sep-2018)

Ref Expression
Assertion cnm2m1cnm3 ⊢ A ∈ ℂ → A - 2 - 1 = A − 3

Proof

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