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

Proof

Step	Hyp	Ref	Expression
1		addsqn2reurex2	⊢ ( 𝐶 ∈ ℂ → ¬ ( ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑏 ∈ ℂ ∃ 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
2		df-2reu	⊢ ( ∃! 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃! 𝑏 ∈ ℂ ∃ 𝑎 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
3	1 2	sylnibr	⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑎 ∈ ℂ , 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 )