Theorem addn0nid

Description: Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021)

	Ref	Expression
Assertion	addn0nid	$$⊢\left(X\in ℂ\wedge Y\in ℂ\wedge Y\ne 0\right)\to X+Y\ne X$$

Proof

Step	Hyp	Ref	Expression
1		addid0	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X+Y=X\leftrightarrow Y=0\right)$$
2	1	biimpd	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(X+Y=X\to Y=0\right)$$
3	2	necon3d	$$⊢\left(X\in ℂ\wedge Y\in ℂ\right)\to \left(Y\ne 0\to X+Y\ne X\right)$$
4	3	3impia	$$⊢\left(X\in ℂ\wedge Y\in ℂ\wedge Y\ne 0\right)\to X+Y\ne X$$