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	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0 ) → ( 𝑋 + 𝑌 ) ≠ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		addid0	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 + 𝑌 ) = 𝑋 ↔ 𝑌 = 0 ) )
2	1	biimpd	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑋 + 𝑌 ) = 𝑋 → 𝑌 = 0 ) )
3	2	necon3d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( 𝑌 ≠ 0 → ( 𝑋 + 𝑌 ) ≠ 𝑋 ) )
4	3	3impia	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0 ) → ( 𝑋 + 𝑌 ) ≠ 𝑋 )