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	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X+Y=X\leftrightarrow Y=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to X\in ℂ$$
2		simpr	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to Y\in ℂ$$
3	1 1 2	subaddd	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X-X=Y\leftrightarrow X+Y=X\right)$$
4		eqcom	$$⊢X-X=Y\leftrightarrow Y=X-X$$
5		simpr	$$⊢\left(X\in ℂ\wedge Y=X-X\right)\to Y=X-X$$
6		subid	$$⊢X\in ℂ\to X-X=0$$
7	6	adantr	$$⊢\left(X\in ℂ\wedge Y=X-X\right)\to X-X=0$$
8	5 7	eqtrd	$$⊢\left(X\in ℂ\wedge Y=X-X\right)\to Y=0$$
9	8	ex	$$⊢X\in ℂ\to \left(Y=X-X\to Y=0\right)$$
10	4 9	biimtrid	$$⊢X\in ℂ\to \left(X-X=Y\to Y=0\right)$$
11	10	adantr	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X-X=Y\to Y=0\right)$$
12	3 11	sylbird	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X+Y=X\to Y=0\right)$$
13		oveq2	$$⊢Y=0\to X+Y=X+0$$
14		addrid	$$⊢X\in ℂ\to X+0=X$$
15	13 14	sylan9eqr	$$⊢\left(X\in ℂ\wedge Y=0\right)\to X+Y=X$$
16	15	ex	$$⊢X\in ℂ\to \left(Y=0\to X+Y=X\right)$$
17	16	adantr	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(Y=0\to X+Y=X\right)$$
18	12 17	impbid	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X+Y=X\leftrightarrow Y=0\right)$$