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 ⊢ C ∈ ℂ → ¬ ∃! a ∈ ℂ , b ∈ ℂ a + b 2 = C

Proof

Step Hyp Ref Expression
1 addsqn2reurex2 ⊢ C ∈ ℂ → ¬ ∃! a ∈ ℂ ∃ b ∈ ℂ a + b 2 = C ∧ ∃! b ∈ ℂ ∃ a ∈ ℂ a + b 2 = C
2 df-2reu ⊢ ∃! a ∈ ℂ , b ∈ ℂ a + b 2 = C ↔ ∃! a ∈ ℂ ∃ b ∈ ℂ a + b 2 = C ∧ ∃! b ∈ ℂ ∃ a ∈ ℂ a + b 2 = C
3 1 2 sylnibr ⊢ C ∈ ℂ → ¬ ∃! a ∈ ℂ , b ∈ ℂ a + b 2 = C