Description: For each complex number, there exists a complex number to which the square of more than one (or no) other complex numbers can be added to result in the given complex number.
Remark: This theorem, together with addsq2reu , shows that there are cases in which there is a set together with a not unique other set fulfilling a wff, although there is a unique set fulfilling the wff together with another unique set (see addsq2reu ). For more details see comment for addsqnreup . (Contributed by AV, 20-Jun-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | addsqrexnreu | ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑎 ∈ ℂ ¬ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano2cnm | ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 1 ) ∈ ℂ ) | |
| 2 | oveq1 | ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) ) | |
| 3 | 2 | eqeq1d | ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 4 | 3 | reubidv | ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 5 | 4 | notbid | ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( ¬ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ¬ ∃! 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 6 | 5 | adantl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑎 = ( 𝐶 − 1 ) ) → ( ¬ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ¬ ∃! 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 7 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 8 | neg1cn | ⊢ - 1 ∈ ℂ | |
| 9 | 1nn | ⊢ 1 ∈ ℕ | |
| 10 | nnneneg | ⊢ ( 1 ∈ ℕ → 1 ≠ - 1 ) | |
| 11 | 9 10 | ax-mp | ⊢ 1 ≠ - 1 |
| 12 | 7 8 11 | 3pm3.2i | ⊢ ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 1 ≠ - 1 ) |
| 13 | sq1 | ⊢ ( 1 ↑ 2 ) = 1 | |
| 14 | 13 | eqcomi | ⊢ 1 = ( 1 ↑ 2 ) |
| 15 | neg1sqe1 | ⊢ ( - 1 ↑ 2 ) = 1 | |
| 16 | 15 | eqcomi | ⊢ 1 = ( - 1 ↑ 2 ) |
| 17 | 14 16 | pm3.2i | ⊢ ( 1 = ( 1 ↑ 2 ) ∧ 1 = ( - 1 ↑ 2 ) ) |
| 18 | oveq1 | ⊢ ( 𝑏 = 1 → ( 𝑏 ↑ 2 ) = ( 1 ↑ 2 ) ) | |
| 19 | 18 | eqeq2d | ⊢ ( 𝑏 = 1 → ( 1 = ( 𝑏 ↑ 2 ) ↔ 1 = ( 1 ↑ 2 ) ) ) |
| 20 | oveq1 | ⊢ ( 𝑏 = - 1 → ( 𝑏 ↑ 2 ) = ( - 1 ↑ 2 ) ) | |
| 21 | 20 | eqeq2d | ⊢ ( 𝑏 = - 1 → ( 1 = ( 𝑏 ↑ 2 ) ↔ 1 = ( - 1 ↑ 2 ) ) ) |
| 22 | 19 21 | 2nreu | ⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 1 ≠ - 1 ) → ( ( 1 = ( 1 ↑ 2 ) ∧ 1 = ( - 1 ↑ 2 ) ) → ¬ ∃! 𝑏 ∈ ℂ 1 = ( 𝑏 ↑ 2 ) ) ) |
| 23 | 12 17 22 | mp2 | ⊢ ¬ ∃! 𝑏 ∈ ℂ 1 = ( 𝑏 ↑ 2 ) |
| 24 | simpl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → 𝐶 ∈ ℂ ) | |
| 25 | 1 | adantr | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝐶 − 1 ) ∈ ℂ ) |
| 26 | sqcl | ⊢ ( 𝑏 ∈ ℂ → ( 𝑏 ↑ 2 ) ∈ ℂ ) | |
| 27 | 26 | adantl | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑏 ↑ 2 ) ∈ ℂ ) |
| 28 | 24 25 27 | subaddd | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝐶 − ( 𝐶 − 1 ) ) = ( 𝑏 ↑ 2 ) ↔ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) |
| 29 | id | ⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ ℂ ) | |
| 30 | 1cnd | ⊢ ( 𝐶 ∈ ℂ → 1 ∈ ℂ ) | |
| 31 | 29 30 | nncand | ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − ( 𝐶 − 1 ) ) = 1 ) |
| 32 | 31 | adantr | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝐶 − ( 𝐶 − 1 ) ) = 1 ) |
| 33 | 32 | eqeq1d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝐶 − ( 𝐶 − 1 ) ) = ( 𝑏 ↑ 2 ) ↔ 1 = ( 𝑏 ↑ 2 ) ) ) |
| 34 | 28 33 | bitr3d | ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ 1 = ( 𝑏 ↑ 2 ) ) ) |
| 35 | 34 | reubidva | ⊢ ( 𝐶 ∈ ℂ → ( ∃! 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃! 𝑏 ∈ ℂ 1 = ( 𝑏 ↑ 2 ) ) ) |
| 36 | 23 35 | mtbiri | ⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |
| 37 | 1 6 36 | rspcedvd | ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑎 ∈ ℂ ¬ ∃! 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) |