Metamath Proof Explorer

Theorem addsqnot2reu

Description: For each complex number C , there does not uniquely exist two complex numbers a and b , with b squared and added to a resulting in the given complex number C . Double restricted existential uniqueness variant of addsqn2reurex2 . (Contributed by AV, 5-Jul-2023)

		Ref	Expression
	Assertion	addsqnot2reu	$Math input error$

Proof

Step	Hyp	Ref	Expression
1		addsqn2reurex2	$⊢ C \in ℂ \to \neg (\exists! a \in ℂ \exists b \in ℂ a + b^{2} = C \land \exists! b \in ℂ \exists a \in ℂ a + b^{2} = C)$
2		df-2reu	$Math input error$
3	1 2	sylnibr	$Math input error$