Theorem addsq2nreurex

Description: For each complex number C , there is no unique complex number a added to the square of another complex number b resulting in the given complex number C . (Contributed by AV, 2-Jul-2023)

	Ref	Expression
Assertion	addsq2nreurex	$$⊢C\in ℂ\to \neg \exists !a\in ℂ\exists b\in ℂa+b^2=C$$

Proof

Step	Hyp	Ref	Expression
1		peano2cnm	$$⊢C\in ℂ\to C-1\in ℂ$$
2		id	$$⊢C\in ℂ\to C\in ℂ$$
3		4cn	$$⊢4\in ℂ$$
4	3	a1i	$$⊢C\in ℂ\to 4\in ℂ$$
5	2 4	subcld	$$⊢C\in ℂ\to C-4\in ℂ$$
6		1cnd	$$⊢C\in ℂ\to 1\in ℂ$$
7		1re	$$⊢1\in ℝ$$
8		1lt4	$$⊢1<4$$
9	7 8	ltneii	$$⊢1\ne 4$$
10	9	a1i	$$⊢C\in ℂ\to 1\ne 4$$
11	2 6 4 10	subneintrd	$$⊢C\in ℂ\to C-1\ne C-4$$
12		oveq1	$$⊢b=1\to b^2=1^2$$
13	12	oveq2d	$$⊢b=1\to C-1+b^2=C-1+1^2$$
14	13	eqeq1d	$$⊢b=1\to \left(C-1+b^2=C\leftrightarrow C-1+1^2=C\right)$$
15	14	adantl	$$⊢\left(C\in ℂ\wedge b=1\right)\to \left(C-1+b^2=C\leftrightarrow C-1+1^2=C\right)$$
16		sq1	$$⊢1^2=1$$
17	16	oveq2i	$$⊢C-1+1^2=C-1+1$$
18		npcan1	$$⊢C\in ℂ\to C-1+1=C$$
19	17 18	syl5eq	$$⊢C\in ℂ\to C-1+1^2=C$$
20	6 15 19	rspcedvd	$$⊢C\in ℂ\to \exists b\in ℂC-1+b^2=C$$
21		2cnd	$$⊢C\in ℂ\to 2\in ℂ$$
22		oveq1	$$⊢b=2\to b^2=2^2$$
23	22	oveq2d	$$⊢b=2\to C-4+b^2=C-4+2^2$$
24	23	eqeq1d	$$⊢b=2\to \left(C-4+b^2=C\leftrightarrow C-4+2^2=C\right)$$
25	24	adantl	$$⊢\left(C\in ℂ\wedge b=2\right)\to \left(C-4+b^2=C\leftrightarrow C-4+2^2=C\right)$$
26		2cn	$$⊢2\in ℂ$$
27	26	sqcli	$$⊢2^2\in ℂ$$
28	27	a1i	$$⊢C\in ℂ\to 2^2\in ℂ$$
29	2 4 28	subadd23d	$$⊢C\in ℂ\to C-4+2^2=C+2^2-4$$
30		sq2	$$⊢2^2=4$$
31	30	a1i	$$⊢C\in ℂ\to 2^2=4$$
32	28 31	subeq0bd	$$⊢C\in ℂ\to 2^2-4=0$$
33	27 3	subcli	$$⊢2^2-4\in ℂ$$
34		addid0	$$⊢\left(C\in ℂ\wedge 2^2-4\in ℂ\right)\to \left(C+2^2-4=C\leftrightarrow 2^2-4=0\right)$$
35	33 34	mpan2	$$⊢C\in ℂ\to \left(C+2^2-4=C\leftrightarrow 2^2-4=0\right)$$
36	32 35	mpbird	$$⊢C\in ℂ\to C+2^2-4=C$$
37	29 36	eqtrd	$$⊢C\in ℂ\to C-4+2^2=C$$
38	21 25 37	rspcedvd	$$⊢C\in ℂ\to \exists b\in ℂC-4+b^2=C$$
39		oveq1	$$⊢a=C-1\to a+b^2=C-1+b^2$$
40	39	eqeq1d	$$⊢a=C-1\to \left(a+b^2=C\leftrightarrow C-1+b^2=C\right)$$
41	40	rexbidv	$$⊢a=C-1\to \left(\exists b\in ℂa+b^2=C\leftrightarrow \exists b\in ℂC-1+b^2=C\right)$$
42		oveq1	$$⊢a=C-4\to a+b^2=C-4+b^2$$
43	42	eqeq1d	$$⊢a=C-4\to \left(a+b^2=C\leftrightarrow C-4+b^2=C\right)$$
44	43	rexbidv	$$⊢a=C-4\to \left(\exists b\in ℂa+b^2=C\leftrightarrow \exists b\in ℂC-4+b^2=C\right)$$
45	41 44	2nreu	$$⊢\left(C-1\in ℂ\wedge C-4\in ℂ\wedge C-1\ne C-4\right)\to \left(\left(\exists b\in ℂC-1+b^2=C\wedge \exists b\in ℂC-4+b^2=C\right)\to \neg \exists !a\in ℂ\exists b\in ℂa+b^2=C\right)$$
46	45	imp	$$⊢\left(\left(C-1\in ℂ\wedge C-4\in ℂ\wedge C-1\ne C-4\right)\wedge \left(\exists b\in ℂC-1+b^2=C\wedge \exists b\in ℂC-4+b^2=C\right)\right)\to \neg \exists !a\in ℂ\exists b\in ℂa+b^2=C$$
47	1 5 11 20 38 46	syl32anc	$$⊢C\in ℂ\to \neg \exists !a\in ℂ\exists b\in ℂa+b^2=C$$