Metamath Proof Explorer

Theorem addcan2

Description: Cancellation law for addition. (Contributed by NM, 30-Jul-2004) (Revised by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion addcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C = B + C ↔ A = B

Proof

Step Hyp Ref Expression
1 cnegex ⊢ C ∈ ℂ → ∃ x ∈ ℂ C + x = 0
2 1 3ad2ant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → ∃ x ∈ ℂ C + x = 0
3 oveq1 ⊢ A + C = B + C → A + C + x = B + C + x
4 simpl1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A ∈ ℂ
5 simpl3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → C ∈ ℂ
6 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → x ∈ ℂ
7 4 5 6 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C + x = A + C + x
8 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → C + x = 0
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C + x = A + 0
10 addid1 ⊢ A ∈ ℂ → A + 0 = A
11 4 10 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + 0 = A
12 7 9 11 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C + x = A
13 simpl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → B ∈ ℂ
14 13 5 6 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → B + C + x = B + C + x
15 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → B + C + x = B + 0
16 addid1 ⊢ B ∈ ℂ → B + 0 = B
17 13 16 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → B + 0 = B
18 14 15 17 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → B + C + x = B
19 12 18 eqeq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C + x = B + C + x ↔ A = B
20 3 19 syl5ib ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C = B + C → A = B
21 oveq1 ⊢ A = B → A + C = B + C
22 20 21 impbid1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ x ∈ ℂ ∧ C + x = 0 → A + C = B + C ↔ A = B
23 2 22 rexlimddv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + C = B + C ↔ A = B