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

Proof

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