Metamath Proof Explorer

Theorem addcan

Description: Cancellation law for addition. Theorem I.1 of Apostol p. 18. (Contributed by NM, 22-Nov-1994) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

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