Description: For each complex number C , there exists a unique complex number a added to the square of a unique another complex number b resulting in the given complex number C . The unique complex number a is C , and the unique another complex number b is 0 .
Remark: This, together with addsqnreup , 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 ). See also comments for df-eu and 2eu4 . For more details see comment for addsqnreup . (Contributed by AV, 21-Jun-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | addsq2reu | |- ( C e. CC -> E! a e. CC E! b e. CC ( a + ( b ^ 2 ) ) = C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( C e. CC -> C e. CC ) |
|
| 2 | oveq1 | |- ( a = C -> ( a + ( b ^ 2 ) ) = ( C + ( b ^ 2 ) ) ) |
|
| 3 | 2 | eqeq1d | |- ( a = C -> ( ( a + ( b ^ 2 ) ) = C <-> ( C + ( b ^ 2 ) ) = C ) ) |
| 4 | 3 | reubidv | |- ( a = C -> ( E! b e. CC ( a + ( b ^ 2 ) ) = C <-> E! b e. CC ( C + ( b ^ 2 ) ) = C ) ) |
| 5 | eqeq1 | |- ( a = C -> ( a = c <-> C = c ) ) |
|
| 6 | 5 | imbi2d | |- ( a = C -> ( ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) <-> ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) ) |
| 7 | 6 | ralbidv | |- ( a = C -> ( A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) <-> A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) ) |
| 8 | 4 7 | anbi12d | |- ( a = C -> ( ( E! b e. CC ( a + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) ) <-> ( E! b e. CC ( C + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) ) ) |
| 9 | 8 | adantl | |- ( ( C e. CC /\ a = C ) -> ( ( E! b e. CC ( a + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) ) <-> ( E! b e. CC ( C + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) ) ) |
| 10 | 0cnd | |- ( C e. CC -> 0 e. CC ) |
|
| 11 | reueq | |- ( 0 e. CC <-> E! b e. CC b = 0 ) |
|
| 12 | 10 11 | sylib | |- ( C e. CC -> E! b e. CC b = 0 ) |
| 13 | subid | |- ( C e. CC -> ( C - C ) = 0 ) |
|
| 14 | 13 | adantr | |- ( ( C e. CC /\ b e. CC ) -> ( C - C ) = 0 ) |
| 15 | 14 | eqeq1d | |- ( ( C e. CC /\ b e. CC ) -> ( ( C - C ) = ( b ^ 2 ) <-> 0 = ( b ^ 2 ) ) ) |
| 16 | simpl | |- ( ( C e. CC /\ b e. CC ) -> C e. CC ) |
|
| 17 | simpr | |- ( ( C e. CC /\ b e. CC ) -> b e. CC ) |
|
| 18 | 17 | sqcld | |- ( ( C e. CC /\ b e. CC ) -> ( b ^ 2 ) e. CC ) |
| 19 | 16 16 18 | subaddd | |- ( ( C e. CC /\ b e. CC ) -> ( ( C - C ) = ( b ^ 2 ) <-> ( C + ( b ^ 2 ) ) = C ) ) |
| 20 | eqcom | |- ( 0 = ( b ^ 2 ) <-> ( b ^ 2 ) = 0 ) |
|
| 21 | sqeq0 | |- ( b e. CC -> ( ( b ^ 2 ) = 0 <-> b = 0 ) ) |
|
| 22 | 20 21 | syl5bb | |- ( b e. CC -> ( 0 = ( b ^ 2 ) <-> b = 0 ) ) |
| 23 | 22 | adantl | |- ( ( C e. CC /\ b e. CC ) -> ( 0 = ( b ^ 2 ) <-> b = 0 ) ) |
| 24 | 15 19 23 | 3bitr3d | |- ( ( C e. CC /\ b e. CC ) -> ( ( C + ( b ^ 2 ) ) = C <-> b = 0 ) ) |
| 25 | 24 | reubidva | |- ( C e. CC -> ( E! b e. CC ( C + ( b ^ 2 ) ) = C <-> E! b e. CC b = 0 ) ) |
| 26 | 12 25 | mpbird | |- ( C e. CC -> E! b e. CC ( C + ( b ^ 2 ) ) = C ) |
| 27 | simpr | |- ( ( C e. CC /\ c e. CC ) -> c e. CC ) |
|
| 28 | 27 | adantr | |- ( ( ( C e. CC /\ c e. CC ) /\ b e. CC ) -> c e. CC ) |
| 29 | sqcl | |- ( b e. CC -> ( b ^ 2 ) e. CC ) |
|
| 30 | 29 | adantl | |- ( ( ( C e. CC /\ c e. CC ) /\ b e. CC ) -> ( b ^ 2 ) e. CC ) |
| 31 | simpl | |- ( ( C e. CC /\ c e. CC ) -> C e. CC ) |
|
| 32 | 31 | adantr | |- ( ( ( C e. CC /\ c e. CC ) /\ b e. CC ) -> C e. CC ) |
| 33 | 28 30 32 | addrsub | |- ( ( ( C e. CC /\ c e. CC ) /\ b e. CC ) -> ( ( c + ( b ^ 2 ) ) = C <-> ( b ^ 2 ) = ( C - c ) ) ) |
| 34 | 33 | reubidva | |- ( ( C e. CC /\ c e. CC ) -> ( E! b e. CC ( c + ( b ^ 2 ) ) = C <-> E! b e. CC ( b ^ 2 ) = ( C - c ) ) ) |
| 35 | subcl | |- ( ( C e. CC /\ c e. CC ) -> ( C - c ) e. CC ) |
|
| 36 | reusq0 | |- ( ( C - c ) e. CC -> ( E! b e. CC ( b ^ 2 ) = ( C - c ) <-> ( C - c ) = 0 ) ) |
|
| 37 | 35 36 | syl | |- ( ( C e. CC /\ c e. CC ) -> ( E! b e. CC ( b ^ 2 ) = ( C - c ) <-> ( C - c ) = 0 ) ) |
| 38 | subeq0 | |- ( ( C e. CC /\ c e. CC ) -> ( ( C - c ) = 0 <-> C = c ) ) |
|
| 39 | 38 | biimpd | |- ( ( C e. CC /\ c e. CC ) -> ( ( C - c ) = 0 -> C = c ) ) |
| 40 | 37 39 | sylbid | |- ( ( C e. CC /\ c e. CC ) -> ( E! b e. CC ( b ^ 2 ) = ( C - c ) -> C = c ) ) |
| 41 | 34 40 | sylbid | |- ( ( C e. CC /\ c e. CC ) -> ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) |
| 42 | 41 | ralrimiva | |- ( C e. CC -> A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) |
| 43 | 26 42 | jca | |- ( C e. CC -> ( E! b e. CC ( C + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> C = c ) ) ) |
| 44 | 1 9 43 | rspcedvd | |- ( C e. CC -> E. a e. CC ( E! b e. CC ( a + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) ) ) |
| 45 | oveq1 | |- ( a = c -> ( a + ( b ^ 2 ) ) = ( c + ( b ^ 2 ) ) ) |
|
| 46 | 45 | eqeq1d | |- ( a = c -> ( ( a + ( b ^ 2 ) ) = C <-> ( c + ( b ^ 2 ) ) = C ) ) |
| 47 | 46 | reubidv | |- ( a = c -> ( E! b e. CC ( a + ( b ^ 2 ) ) = C <-> E! b e. CC ( c + ( b ^ 2 ) ) = C ) ) |
| 48 | 47 | reu8 | |- ( E! a e. CC E! b e. CC ( a + ( b ^ 2 ) ) = C <-> E. a e. CC ( E! b e. CC ( a + ( b ^ 2 ) ) = C /\ A. c e. CC ( E! b e. CC ( c + ( b ^ 2 ) ) = C -> a = c ) ) ) |
| 49 | 44 48 | sylibr | |- ( C e. CC -> E! a e. CC E! b e. CC ( a + ( b ^ 2 ) ) = C ) |