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 addrid ⊢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 addrid ⊢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 imbitrid ⊢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