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 (\exists! x \in ℂ x^{2} = X \leftrightarrow X = 0)$

Proof

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

Metamath Proof Explorer

Theorem reusq0

Proof