Theorem addsqn2reurex2

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 .

Remark: This, together with addsq2reu , is an example showing that the pattern E! a e. A E! b e. B ph does not necessarily mean "There are unique sets a and b fulfilling ph ), as it is the case with the pattern ( E! a e. A E. b e. B ph /\ E! b e. B E. a e. A ph . See also comments for df-eu and 2eu4 . (Contributed by AV, 2-Jul-2023)

	Ref	Expression
Assertion	addsqn2reurex2	$$⊢C\in ℂ\to \neg \left(\exists !a\in ℂ\exists b\in ℂa+b^2=C\wedge \exists !b\in ℂ\exists a\in ℂa+b^2=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsq2nreurex	$$⊢C\in ℂ\to \neg \exists !a\in ℂ\exists b\in ℂa+b^2=C$$
2	1	intnanrd	$$⊢C\in ℂ\to \neg \left(\exists !a\in ℂ\exists b\in ℂa+b^2=C\wedge \exists !b\in ℂ\exists a\in ℂa+b^2=C\right)$$