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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

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