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 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 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addsq2nreurex | |- ( C e. CC -> -. E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C ) |
|
| 2 | 1 | intnanrd | |- ( 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 ) ) |