Theorem addid0

Description: If adding a number to a another number yields the other number, the added number must be 0 . This shows that 0 is the unique (right) identity of the complex numbers. (Contributed by AV, 17-Jan-2021)

	Ref	Expression
Assertion	addid0	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 + 𝑌 ) = 𝑋 ↔ 𝑌 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → 𝑋 ∈ ℂ )
2		simpr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → 𝑌 ∈ ℂ )
3	1 1 2	subaddd	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 − 𝑋 ) = 𝑌 ↔ ( 𝑋 + 𝑌 ) = 𝑋 ) )
4		eqcom	⊢ ( ( 𝑋 − 𝑋 ) = 𝑌 ↔ 𝑌 = ( 𝑋 − 𝑋 ) )
5		simpr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 = ( 𝑋 − 𝑋 ) ) → 𝑌 = ( 𝑋 − 𝑋 ) )
6		subid	⊢ ( 𝑋 ∈ ℂ → ( 𝑋 − 𝑋 ) = 0 )
7	6	adantr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 = ( 𝑋 − 𝑋 ) ) → ( 𝑋 − 𝑋 ) = 0 )
8	5 7	eqtrd	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 = ( 𝑋 − 𝑋 ) ) → 𝑌 = 0 )
9	8	ex	⊢ ( 𝑋 ∈ ℂ → ( 𝑌 = ( 𝑋 − 𝑋 ) → 𝑌 = 0 ) )
10	4 9	syl5bi	⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 − 𝑋 ) = 𝑌 → 𝑌 = 0 ) )
11	10	adantr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 − 𝑋 ) = 𝑌 → 𝑌 = 0 ) )
12	3 11	sylbird	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 + 𝑌 ) = 𝑋 → 𝑌 = 0 ) )
13		oveq2	⊢ ( 𝑌 = 0 → ( 𝑋 + 𝑌 ) = ( 𝑋 + 0 ) )
14		addid1	⊢ ( 𝑋 ∈ ℂ → ( 𝑋 + 0 ) = 𝑋 )
15	13 14	sylan9eqr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 = 0 ) → ( 𝑋 + 𝑌 ) = 𝑋 )
16	15	ex	⊢ ( 𝑋 ∈ ℂ → ( 𝑌 = 0 → ( 𝑋 + 𝑌 ) = 𝑋 ) )
17	16	adantr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( 𝑌 = 0 → ( 𝑋 + 𝑌 ) = 𝑋 ) )
18	12 17	impbid	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 + 𝑌 ) = 𝑋 ↔ 𝑌 = 0 ) )