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 | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑎 ∈ ℂ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ ℂ ) | |
| 2 | oveq1 | ⊢ ( 𝑎 = 𝐶 → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( 𝐶 + ( 𝑏 ↑ 2 ) ) ) | |
| 3 | 2 | eqeq1d | ⊢ ( 𝑎 = 𝐶 → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 4 | 3 | reubidv | ⊢ ( 𝑎 = 𝐶 → ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 5 | eqeq1 | ⊢ ( 𝑎 = 𝐶 → ( 𝑎 = 𝑐 ↔ 𝐶 = 𝑐 ) ) | |
| 6 | 5 | imbi2d | ⊢ ( 𝑎 = 𝐶 → ( ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ↔ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) ) |
| 7 | 6 | ralbidv | ⊢ ( 𝑎 = 𝐶 → ( ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ↔ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) ) |
| 8 | 4 7 | anbi12d | ⊢ ( 𝑎 = 𝐶 → ( ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ) ↔ ( ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) ) ) |
| 9 | 8 | adantl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 = 𝐶 ) → ( ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ) ↔ ( ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) ) ) |
| 10 | 0cnd | ⊢ ( 𝐶 ∈ ℂ → 0 ∈ ℂ ) | |
| 11 | reueq | ⊢ ( 0 ∈ ℂ ↔ ∃! 𝑏 ∈ ℂ 𝑏 = 0 ) | |
| 12 | 10 11 | sylib | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑏 ∈ ℂ 𝑏 = 0 ) |
| 13 | subid | ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 𝐶 ) = 0 ) | |
| 14 | 13 | adantr | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝐶 − 𝐶 ) = 0 ) |
| 15 | 14 | eqeq1d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝐶 − 𝐶 ) = ( 𝑏 ↑ 2 ) ↔ 0 = ( 𝑏 ↑ 2 ) ) ) |
| 16 | simpl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → 𝐶 ∈ ℂ ) | |
| 17 | simpr | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → 𝑏 ∈ ℂ ) | |
| 18 | 17 | sqcld | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑏 ↑ 2 ) ∈ ℂ ) |
| 19 | 16 16 18 | subaddd | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝐶 − 𝐶 ) = ( 𝑏 ↑ 2 ) ↔ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 20 | eqcom | ⊢ ( 0 = ( 𝑏 ↑ 2 ) ↔ ( 𝑏 ↑ 2 ) = 0 ) | |
| 21 | sqeq0 | ⊢ ( 𝑏 ∈ ℂ → ( ( 𝑏 ↑ 2 ) = 0 ↔ 𝑏 = 0 ) ) | |
| 22 | 20 21 | bitrid | ⊢ ( 𝑏 ∈ ℂ → ( 0 = ( 𝑏 ↑ 2 ) ↔ 𝑏 = 0 ) ) |
| 23 | 22 | adantl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 0 = ( 𝑏 ↑ 2 ) ↔ 𝑏 = 0 ) ) |
| 24 | 15 19 23 | 3bitr3d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ 𝑏 = 0 ) ) |
| 25 | 24 | reubidva | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ 𝑏 = 0 ) ) |
| 26 | 12 25 | mpbird | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |
| 27 | simpr | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → 𝑐 ∈ ℂ ) | |
| 28 | 27 | adantr | ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ 𝑏 ∈ ℂ ) → 𝑐 ∈ ℂ ) |
| 29 | sqcl | ⊢ ( 𝑏 ∈ ℂ → ( 𝑏 ↑ 2 ) ∈ ℂ ) | |
| 30 | 29 | adantl | ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ 𝑏 ∈ ℂ ) → ( 𝑏 ↑ 2 ) ∈ ℂ ) |
| 31 | simpl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → 𝐶 ∈ ℂ ) | |
| 32 | 31 | adantr | ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ 𝑏 ∈ ℂ ) → 𝐶 ∈ ℂ ) |
| 33 | 28 30 32 | addrsub | ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ 𝑏 ∈ ℂ ) → ( ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( 𝑏 ↑ 2 ) = ( 𝐶 − 𝑐 ) ) ) |
| 34 | 33 | reubidva | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ ( 𝑏 ↑ 2 ) = ( 𝐶 − 𝑐 ) ) ) |
| 35 | subcl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝐶 − 𝑐 ) ∈ ℂ ) | |
| 36 | reusq0 | ⊢ ( ( 𝐶 − 𝑐 ) ∈ ℂ → ( ∃! 𝑏 ∈ ℂ ( 𝑏 ↑ 2 ) = ( 𝐶 − 𝑐 ) ↔ ( 𝐶 − 𝑐 ) = 0 ) ) | |
| 37 | 35 36 | syl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃! 𝑏 ∈ ℂ ( 𝑏 ↑ 2 ) = ( 𝐶 − 𝑐 ) ↔ ( 𝐶 − 𝑐 ) = 0 ) ) |
| 38 | subeq0 | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝐶 − 𝑐 ) = 0 ↔ 𝐶 = 𝑐 ) ) | |
| 39 | 38 | biimpd | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝐶 − 𝑐 ) = 0 → 𝐶 = 𝑐 ) ) |
| 40 | 37 39 | sylbid | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃! 𝑏 ∈ ℂ ( 𝑏 ↑ 2 ) = ( 𝐶 − 𝑐 ) → 𝐶 = 𝑐 ) ) |
| 41 | 34 40 | sylbid | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) |
| 42 | 41 | ralrimiva | ⊢ ( 𝐶 ∈ ℂ → ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) |
| 43 | 26 42 | jca | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑏 ∈ ℂ ( 𝐶 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝐶 = 𝑐 ) ) ) |
| 44 | 1 9 43 | rspcedvd | ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑎 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ) ) |
| 45 | oveq1 | ⊢ ( 𝑎 = 𝑐 → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( 𝑐 + ( 𝑏 ↑ 2 ) ) ) | |
| 46 | 45 | eqeq1d | ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 47 | 46 | reubidv | ⊢ ( 𝑎 = 𝑐 → ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 48 | 47 | reu8 | ⊢ ( ∃! 𝑎 ∈ ℂ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃ 𝑎 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∀ 𝑐 ∈ ℂ ( ∃! 𝑏 ∈ ℂ ( 𝑐 + ( 𝑏 ↑ 2 ) ) = 𝐶 → 𝑎 = 𝑐 ) ) ) |
| 49 | 44 48 | sylibr | ⊢ ( 𝐶 ∈ ℂ → ∃! 𝑎 ∈ ℂ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |