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+b2=C

Proof

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