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 e. CC -> -. E! a e. CC , b e. CC ( a + ( b ^ 2 ) ) = C )

Proof

Step	Hyp	Ref	Expression
1		addsqn2reurex2	\|- ( C e. CC -> -. ( E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C /\ E! b e. CC E. a e. CC ( a + ( b ^ 2 ) ) = C ) )
2		df-2reu	\|- ( E! a e. CC , b e. CC ( a + ( b ^ 2 ) ) = C <-> ( E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C /\ E! b e. CC E. a e. CC ( a + ( b ^ 2 ) ) = C ) )
3	1 2	sylnibr	\|- ( C e. CC -> -. E! a e. CC , b e. CC ( a + ( b ^ 2 ) ) = C )

Step

Hyp

Ref

Expression

addsqn2reurex2

 |-  ( C e. CC -> -. ( E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C /\ E! b e. CC E. a e. CC ( a + ( b ^ 2 ) ) = C ) )

df-2reu

 |-  ( E! a e. CC , b e. CC ( a + ( b ^ 2 ) ) = C <-> ( E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C /\ E! b e. CC E. a e. CC ( a + ( b ^ 2 ) ) = C ) )

1 2

sylnibr

 |-  ( C e. CC -> -. E! a e. CC , b e. CC ( a + ( b ^ 2 ) ) = C )