This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (X \in ℂ \land Y \in ℂ \land Y \neq 0) \to X + Y \neq X$

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