Theorem reusq0

Description: A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023)

	Ref	Expression
Assertion	reusq0	$$⊢X\in ℂ\to \left(\exists !x\in ℂx^2=X\leftrightarrow X=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		2a1	$$⊢X=0\to \left(X\in ℂ\to \left(\exists !x\in ℂx^2=X\to X=0\right)\right)$$
2		sqrtcl	$$⊢X\in ℂ\to \sqrt{X}\in ℂ$$
3	2	adantr	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \sqrt{X}\in ℂ$$
4	2	negcld	$$⊢X\in ℂ\to -\sqrt{X}\in ℂ$$
5	4	adantr	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to -\sqrt{X}\in ℂ$$
6	2	eqnegd	$$⊢X\in ℂ\to \left(\sqrt{X}=-\sqrt{X}\leftrightarrow \sqrt{X}=0\right)$$
7		simpl	$$⊢\left(X\in ℂ\wedge \sqrt{X}=0\right)\to X\in ℂ$$
8		simpr	$$⊢\left(X\in ℂ\wedge \sqrt{X}=0\right)\to \sqrt{X}=0$$
9	7 8	sqr00d	$$⊢\left(X\in ℂ\wedge \sqrt{X}=0\right)\to X=0$$
10	9	ex	$$⊢X\in ℂ\to \left(\sqrt{X}=0\to X=0\right)$$
11	6 10	sylbid	$$⊢X\in ℂ\to \left(\sqrt{X}=-\sqrt{X}\to X=0\right)$$
12	11	necon3bd	$$⊢X\in ℂ\to \left(\neg X=0\to \sqrt{X}\ne -\sqrt{X}\right)$$
13	12	imp	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \sqrt{X}\ne -\sqrt{X}$$
14	3 5 13	3jca	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \left(\sqrt{X}\in ℂ\wedge -\sqrt{X}\in ℂ\wedge \sqrt{X}\ne -\sqrt{X}\right)$$
15		sqrtth	$$⊢X\in ℂ\to {\sqrt{X}}^2=X$$
16		sqneg	$$⊢\sqrt{X}\in ℂ\to {\left(-\sqrt{X}\right)}^2={\sqrt{X}}^2$$
17	2 16	syl	$$⊢X\in ℂ\to {\left(-\sqrt{X}\right)}^2={\sqrt{X}}^2$$
18	17 15	eqtrd	$$⊢X\in ℂ\to {\left(-\sqrt{X}\right)}^2=X$$
19	15 18	jca	$$⊢X\in ℂ\to \left({\sqrt{X}}^2=X\wedge {\left(-\sqrt{X}\right)}^2=X\right)$$
20	19	adantr	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \left({\sqrt{X}}^2=X\wedge {\left(-\sqrt{X}\right)}^2=X\right)$$
21		oveq1	$$⊢x=\sqrt{X}\to x^2={\sqrt{X}}^2$$
22	21	eqeq1d	$$⊢x=\sqrt{X}\to \left(x^2=X\leftrightarrow {\sqrt{X}}^2=X\right)$$
23		oveq1	$$⊢x=-\sqrt{X}\to x^2={\left(-\sqrt{X}\right)}^2$$
24	23	eqeq1d	$$⊢x=-\sqrt{X}\to \left(x^2=X\leftrightarrow {\left(-\sqrt{X}\right)}^2=X\right)$$
25	22 24	2nreu	$$⊢\left(\sqrt{X}\in ℂ\wedge -\sqrt{X}\in ℂ\wedge \sqrt{X}\ne -\sqrt{X}\right)\to \left(\left({\sqrt{X}}^2=X\wedge {\left(-\sqrt{X}\right)}^2=X\right)\to \neg \exists !x\in ℂx^2=X\right)$$
26	14 20 25	sylc	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \neg \exists !x\in ℂx^2=X$$
27	26	pm2.21d	$$⊢\left(X\in ℂ\wedge \neg X=0\right)\to \left(\exists !x\in ℂx^2=X\to X=0\right)$$
28	27	expcom	$$⊢\neg X=0\to \left(X\in ℂ\to \left(\exists !x\in ℂx^2=X\to X=0\right)\right)$$
29	1 28	pm2.61i	$$⊢X\in ℂ\to \left(\exists !x\in ℂx^2=X\to X=0\right)$$
30		2nn	$$⊢2\in \mathbb{N}$$
31		0cnd	$$⊢2\in \mathbb{N}\to 0\in ℂ$$
32		oveq1	$$⊢x=0\to x^2=0^2$$
33	32	eqeq1d	$$⊢x=0\to \left(x^2=0\leftrightarrow 0^2=0\right)$$
34		eqeq1	$$⊢x=0\to \left(x=y\leftrightarrow 0=y\right)$$
35	34	imbi2d	$$⊢x=0\to \left(\left(y^2=0\to x=y\right)\leftrightarrow \left(y^2=0\to 0=y\right)\right)$$
36	35	ralbidv	$$⊢x=0\to \left(\forall y\in ℂ\left(y^2=0\to x=y\right)\leftrightarrow \forall y\in ℂ\left(y^2=0\to 0=y\right)\right)$$
37	33 36	anbi12d	$$⊢x=0\to \left(\left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)\leftrightarrow \left(0^2=0\wedge \forall y\in ℂ\left(y^2=0\to 0=y\right)\right)\right)$$
38	37	adantl	$$⊢\left(2\in \mathbb{N}\wedge x=0\right)\to \left(\left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)\leftrightarrow \left(0^2=0\wedge \forall y\in ℂ\left(y^2=0\to 0=y\right)\right)\right)$$
39		0exp	$$⊢2\in \mathbb{N}\to 0^2=0$$
40		sqeq0	$$⊢y\in ℂ\to \left(y^2=0\leftrightarrow y=0\right)$$
41	40	biimpd	$$⊢y\in ℂ\to \left(y^2=0\to y=0\right)$$
42		eqcom	$$⊢0=y\leftrightarrow y=0$$
43	41 42	syl6ibr	$$⊢y\in ℂ\to \left(y^2=0\to 0=y\right)$$
44	43	adantl	$$⊢\left(2\in \mathbb{N}\wedge y\in ℂ\right)\to \left(y^2=0\to 0=y\right)$$
45	44	ralrimiva	$$⊢2\in \mathbb{N}\to \forall y\in ℂ\left(y^2=0\to 0=y\right)$$
46	39 45	jca	$$⊢2\in \mathbb{N}\to \left(0^2=0\wedge \forall y\in ℂ\left(y^2=0\to 0=y\right)\right)$$
47	31 38 46	rspcedvd	$$⊢2\in \mathbb{N}\to \exists x\in ℂ\left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)$$
48	30 47	mp1i	$$⊢X=0\to \exists x\in ℂ\left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)$$
49		eqeq2	$$⊢X=0\to \left(x^2=X\leftrightarrow x^2=0\right)$$
50		eqeq2	$$⊢X=0\to \left(y^2=X\leftrightarrow y^2=0\right)$$
51	50	imbi1d	$$⊢X=0\to \left(\left(y^2=X\to x=y\right)\leftrightarrow \left(y^2=0\to x=y\right)\right)$$
52	51	ralbidv	$$⊢X=0\to \left(\forall y\in ℂ\left(y^2=X\to x=y\right)\leftrightarrow \forall y\in ℂ\left(y^2=0\to x=y\right)\right)$$
53	49 52	anbi12d	$$⊢X=0\to \left(\left(x^2=X\wedge \forall y\in ℂ\left(y^2=X\to x=y\right)\right)\leftrightarrow \left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)\right)$$
54	53	rexbidv	$$⊢X=0\to \left(\exists x\in ℂ\left(x^2=X\wedge \forall y\in ℂ\left(y^2=X\to x=y\right)\right)\leftrightarrow \exists x\in ℂ\left(x^2=0\wedge \forall y\in ℂ\left(y^2=0\to x=y\right)\right)\right)$$
55	48 54	mpbird	$$⊢X=0\to \exists x\in ℂ\left(x^2=X\wedge \forall y\in ℂ\left(y^2=X\to x=y\right)\right)$$
56	55	a1i	$$⊢X\in ℂ\to \left(X=0\to \exists x\in ℂ\left(x^2=X\wedge \forall y\in ℂ\left(y^2=X\to x=y\right)\right)\right)$$
57		oveq1	$$⊢x=y\to x^2=y^2$$
58	57	eqeq1d	$$⊢x=y\to \left(x^2=X\leftrightarrow y^2=X\right)$$
59	58	reu8	$$⊢\exists !x\in ℂx^2=X\leftrightarrow \exists x\in ℂ\left(x^2=X\wedge \forall y\in ℂ\left(y^2=X\to x=y\right)\right)$$
60	56 59	syl6ibr	$$⊢X\in ℂ\to \left(X=0\to \exists !x\in ℂx^2=X\right)$$
61	29 60	impbid	$$⊢X\in ℂ\to \left(\exists !x\in ℂx^2=X\leftrightarrow X=0\right)$$