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	⊢ ( 𝐶 ∈ ℂ → ¬ ( ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑏 ∈ ℂ ∃ 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		addsq2nreurex	⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 )
2	1	intnanrd	⊢ ( 𝐶 ∈ ℂ → ¬ ( ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑏 ∈ ℂ ∃ 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )