Theorem sqreu

Description: Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Assertion	sqreu	$$⊢A\in ℂ\to \exists !x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$

Proof

Step	Hyp	Ref	Expression
1		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
2	1	recnd	$$⊢A\in ℂ\to \left|A\right|\in ℂ$$
3		subneg	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \left|A\right|-\left(-A\right)=\left|A\right|+A$$
4	2 3	mpancom	$$⊢A\in ℂ\to \left|A\right|-\left(-A\right)=\left|A\right|+A$$
5	4	eqeq1d	$$⊢A\in ℂ\to \left(\left|A\right|-\left(-A\right)=0\leftrightarrow \left|A\right|+A=0\right)$$
6		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
7	2 6	subeq0ad	$$⊢A\in ℂ\to \left(\left|A\right|-\left(-A\right)=0\leftrightarrow \left|A\right|=-A\right)$$
8	5 7	bitr3d	$$⊢A\in ℂ\to \left(\left|A\right|+A=0\leftrightarrow \left|A\right|=-A\right)$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
11	1 10	jca	$$⊢A\in ℂ\to \left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)$$
12		eleq1	$$⊢\left|A\right|=-A\to \left(\left|A\right|\in ℝ\leftrightarrow -A\in ℝ\right)$$
13		breq2	$$⊢\left|A\right|=-A\to \left(0\le \left|A\right|\leftrightarrow 0\le -A\right)$$
14	12 13	anbi12d	$$⊢\left|A\right|=-A\to \left(\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\leftrightarrow \left(-A\in ℝ\wedge 0\le -A\right)\right)$$
15	11 14	imbitrid	$$⊢\left|A\right|=-A\to \left(A\in ℂ\to \left(-A\in ℝ\wedge 0\le -A\right)\right)$$
16	15	impcom	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \left(-A\in ℝ\wedge 0\le -A\right)$$
17		resqrtcl	$$⊢\left(-A\in ℝ\wedge 0\le -A\right)\to \sqrt{-A}\in ℝ$$
18	16 17	syl	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \sqrt{-A}\in ℝ$$
19	18	recnd	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \sqrt{-A}\in ℂ$$
20		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \sqrt{-A}\in ℂ\right)\to \mathrm{i}\sqrt{-A}\in ℂ$$
21	9 19 20	sylancr	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \mathrm{i}\sqrt{-A}\in ℂ$$
22		sqrtneglem	$$⊢\left(-A\in ℝ\wedge 0\le -A\right)\to \left({\mathrm{i}\sqrt{-A}}^2=-\left(-A\right)\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)$$
23	16 22	syl	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \left({\mathrm{i}\sqrt{-A}}^2=-\left(-A\right)\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)$$
24		negneg	$$⊢A\in ℂ\to -\left(-A\right)=A$$
25	24	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to -\left(-A\right)=A$$
26	25	eqeq2d	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \left({\mathrm{i}\sqrt{-A}}^2=-\left(-A\right)\leftrightarrow {\mathrm{i}\sqrt{-A}}^2=A\right)$$
27	26	3anbi1d	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \left(\left({\mathrm{i}\sqrt{-A}}^2=-\left(-A\right)\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)\leftrightarrow \left({\mathrm{i}\sqrt{-A}}^2=A\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)\right)$$
28	23 27	mpbid	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \left({\mathrm{i}\sqrt{-A}}^2=A\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)$$
29		oveq1	$$⊢x=\mathrm{i}\sqrt{-A}\to x^2={\mathrm{i}\sqrt{-A}}^2$$
30	29	eqeq1d	$$⊢x=\mathrm{i}\sqrt{-A}\to \left(x^2=A\leftrightarrow {\mathrm{i}\sqrt{-A}}^2=A\right)$$
31		fveq2	$$⊢x=\mathrm{i}\sqrt{-A}\to \Re \left(x\right)=\Re \left(\mathrm{i}\sqrt{-A}\right)$$
32	31	breq2d	$$⊢x=\mathrm{i}\sqrt{-A}\to \left(0\le \Re \left(x\right)\leftrightarrow 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\right)$$
33		oveq2	$$⊢x=\mathrm{i}\sqrt{-A}\to \mathrm{i}x=\mathrm{i}\mathrm{i}\sqrt{-A}$$
34		neleq1	$$⊢\mathrm{i}x=\mathrm{i}\mathrm{i}\sqrt{-A}\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)$$
35	33 34	syl	$$⊢x=\mathrm{i}\sqrt{-A}\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)$$
36	30 32 35	3anbi123d	$$⊢x=\mathrm{i}\sqrt{-A}\to \left(\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left({\mathrm{i}\sqrt{-A}}^2=A\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)\right)$$
37	36	rspcev	$$⊢\left(\mathrm{i}\sqrt{-A}\in ℂ\wedge \left({\mathrm{i}\sqrt{-A}}^2=A\wedge 0\le \Re \left(\mathrm{i}\sqrt{-A}\right)\wedge \mathrm{i}\mathrm{i}\sqrt{-A}\notin {ℝ}^{+}\right)\right)\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
38	21 28 37	syl2anc	$$⊢\left(A\in ℂ\wedge \left|A\right|=-A\right)\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
39	38	ex	$$⊢A\in ℂ\to \left(\left|A\right|=-A\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
40	8 39	sylbid	$$⊢A\in ℂ\to \left(\left|A\right|+A=0\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
41		resqrtcl	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to \sqrt{\left|A\right|}\in ℝ$$
42	1 10 41	syl2anc	$$⊢A\in ℂ\to \sqrt{\left|A\right|}\in ℝ$$
43	42	recnd	$$⊢A\in ℂ\to \sqrt{\left|A\right|}\in ℂ$$
44	43	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\in ℂ$$
45		addcl	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \left|A\right|+A\in ℂ$$
46	2 45	mpancom	$$⊢A\in ℂ\to \left|A\right|+A\in ℂ$$
47	46	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|+A\in ℂ$$
48		abscl	$$⊢\left|A\right|+A\in ℂ\to \left|\left|A\right|+A\right|\in ℝ$$
49	46 48	syl	$$⊢A\in ℂ\to \left|\left|A\right|+A\right|\in ℝ$$
50	49	recnd	$$⊢A\in ℂ\to \left|\left|A\right|+A\right|\in ℂ$$
51	50	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|\left|A\right|+A\right|\in ℂ$$
52	46	abs00ad	$$⊢A\in ℂ\to \left(\left|\left|A\right|+A\right|=0\leftrightarrow \left|A\right|+A=0\right)$$
53	52	necon3bid	$$⊢A\in ℂ\to \left(\left|\left|A\right|+A\right|\ne 0\leftrightarrow \left|A\right|+A\ne 0\right)$$
54	53	biimpar	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|\left|A\right|+A\right|\ne 0$$
55	47 51 54	divcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\in ℂ$$
56	44 55	mulcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\in ℂ$$
57		eqid	$$⊢\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)$$
58	57	sqreulem	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left({\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=A\wedge 0\le \Re \left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\right)\wedge \mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\notin {ℝ}^{+}\right)$$
59		oveq1	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to x^2={\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2$$
60	59	eqeq1d	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \left(x^2=A\leftrightarrow {\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=A\right)$$
61		fveq2	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \Re \left(x\right)=\Re \left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\right)$$
62	61	breq2d	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \left(0\le \Re \left(x\right)\leftrightarrow 0\le \Re \left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\right)\right)$$
63		oveq2	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \mathrm{i}x=\mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)$$
64		neleq1	$$⊢\mathrm{i}x=\mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\notin {ℝ}^{+}\right)$$
65	63 64	syl	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \left(\mathrm{i}x\notin {ℝ}^{+}\leftrightarrow \mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\notin {ℝ}^{+}\right)$$
66	60 62 65	3anbi123d	$$⊢x=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\to \left(\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left({\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=A\wedge 0\le \Re \left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\right)\wedge \mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\notin {ℝ}^{+}\right)\right)$$
67	66	rspcev	$$⊢\left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\in ℂ\wedge \left({\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=A\wedge 0\le \Re \left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\right)\wedge \mathrm{i}\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\notin {ℝ}^{+}\right)\right)\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
68	56 58 67	syl2anc	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
69	68	ex	$$⊢A\in ℂ\to \left(\left|A\right|+A\ne 0\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
70	40 69	pm2.61dne	$$⊢A\in ℂ\to \exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
71		sqrmo	$$⊢A\in ℂ\to {\exists }^{*}x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$
72		reu5	$$⊢\exists !x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\leftrightarrow \left(\exists x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\wedge {\exists }^{*}x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)\right)$$
73	70 71 72	sylanbrc	$$⊢A\in ℂ\to \exists !x\in ℂ\left(x^2=A\wedge 0\le \Re \left(x\right)\wedge \mathrm{i}x\notin {ℝ}^{+}\right)$$