Metamath Proof Explorer

Theorem addsqrexnreu

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 ⊢ C ∈ ℂ → ∃ a ∈ ℂ ¬ ∃! b ∈ ℂ a + b 2 = C

Proof

Step Hyp Ref Expression
1 peano2cnm ⊢ C ∈ ℂ → C − 1 ∈ ℂ
2 oveq1 ⊢ a = C − 1 → a + b 2 = C - 1 + b 2
3 2 eqeq1d ⊢ a = C − 1 → a + b 2 = C ↔ C - 1 + b 2 = C
4 3 reubidv ⊢ a = C − 1 → ∃! b ∈ ℂ a + b 2 = C ↔ ∃! b ∈ ℂ C - 1 + b 2 = C
5 4 notbid ⊢ a = C − 1 → ¬ ∃! b ∈ ℂ a + b 2 = C ↔ ¬ ∃! b ∈ ℂ C - 1 + b 2 = C
6 5 adantl ⊢ C ∈ ℂ ∧ a = C − 1 → ¬ ∃! b ∈ ℂ a + b 2 = C ↔ ¬ ∃! b ∈ ℂ C - 1 + b 2 = C
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 ⊢ b = 1 → b 2 = 1 2
19 18 eqeq2d ⊢ b = 1 → 1 = b 2 ↔ 1 = 1 2
20 oveq1 ⊢ b = − 1 → b 2 = − 1 2
21 20 eqeq2d ⊢ b = − 1 → 1 = b 2 ↔ 1 = − 1 2
22 19 21 2nreu ⊢ 1 ∈ ℂ ∧ − 1 ∈ ℂ ∧ 1 ≠ − 1 → 1 = 1 2 ∧ 1 = − 1 2 → ¬ ∃! b ∈ ℂ 1 = b 2
23 12 17 22 mp2 ⊢ ¬ ∃! b ∈ ℂ 1 = b 2
24 simpl ⊢ C ∈ ℂ ∧ b ∈ ℂ → C ∈ ℂ
25 1 adantr ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − 1 ∈ ℂ
26 sqcl ⊢ b ∈ ℂ → b 2 ∈ ℂ
27 26 adantl ⊢ C ∈ ℂ ∧ b ∈ ℂ → b 2 ∈ ℂ
28 24 25 27 subaddd ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C − 1 = b 2 ↔ C - 1 + b 2 = C
29 id ⊢ C ∈ ℂ → C ∈ ℂ
30 1cnd ⊢ C ∈ ℂ → 1 ∈ ℂ
31 29 30 nncand ⊢ C ∈ ℂ → C − C − 1 = 1
32 31 adantr ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C − 1 = 1
33 32 eqeq1d ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C − 1 = b 2 ↔ 1 = b 2
34 28 33 bitr3d ⊢ C ∈ ℂ ∧ b ∈ ℂ → C - 1 + b 2 = C ↔ 1 = b 2
35 34 reubidva ⊢ C ∈ ℂ → ∃! b ∈ ℂ C - 1 + b 2 = C ↔ ∃! b ∈ ℂ 1 = b 2
36 23 35 mtbiri ⊢ C ∈ ℂ → ¬ ∃! b ∈ ℂ C - 1 + b 2 = C
37 1 6 36 rspcedvd ⊢ C ∈ ℂ → ∃ a ∈ ℂ ¬ ∃! b ∈ ℂ a + b 2 = C