Theorem constrresqrtcl

Description: If a positive real number X is constructible, then, so is its square root. (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypotheses	constrresqrtcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
	constrresqrtcl.2	$$⊢\phi \to X\in ℝ$$
	constrresqrtcl.3	$$⊢\phi \to 0\le X$$
Assertion	constrresqrtcl	$$⊢\phi \to \sqrt{X}\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrresqrtcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constrresqrtcl.2	$$⊢\phi \to X\in ℝ$$
3		constrresqrtcl.3	$$⊢\phi \to 0\le X$$
4		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
5	4	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
6		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
7	6	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
8		iconstr	$$⊢\mathrm{i}\in \mathrm{Constr}$$
9	8	a1i	$$⊢\phi \to \mathrm{i}\in \mathrm{Constr}$$
10	2	recnd	$$⊢\phi \to X\in ℂ$$
11		1cnd	$$⊢\phi \to 1\in ℂ$$
12	10 11	subcld	$$⊢\phi \to X-1\in ℂ$$
13		2cnd	$$⊢\phi \to 2\in ℂ$$
14		2ne0	$$⊢2\ne 0$$
15	14	a1i	$$⊢\phi \to 2\ne 0$$
16	12 13 15	divrecd	$$⊢\phi \to \frac{X-1}{2}=\left(X-1\right)\left(\frac{1}{2}\right)$$
17	10 11	negsubd	$$⊢\phi \to X+-1=X-1$$
18	7	constrnegcl	$$⊢\phi \to -1\in \mathrm{Constr}$$
19	1 18	constraddcl	$$⊢\phi \to X+-1\in \mathrm{Constr}$$
20	17 19	eqeltrrd	$$⊢\phi \to X-1\in \mathrm{Constr}$$
21		2z	$$⊢2\in \mathbb{Z}$$
22	21	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
23	22	zconstr	$$⊢\phi \to 2\in \mathrm{Constr}$$
24	23 15	constrinvcl	$$⊢\phi \to \frac{1}{2}\in \mathrm{Constr}$$
25	20 24	constrmulcl	$$⊢\phi \to \left(X-1\right)\left(\frac{1}{2}\right)\in \mathrm{Constr}$$
26	16 25	eqeltrd	$$⊢\phi \to \frac{X-1}{2}\in \mathrm{Constr}$$
27	9 26	constrmulcl	$$⊢\phi \to \mathrm{i}\left(\frac{X-1}{2}\right)\in \mathrm{Constr}$$
28	10 11	addcld	$$⊢\phi \to X+1\in ℂ$$
29	28 13 15	divrecd	$$⊢\phi \to \frac{X+1}{2}=\left(X+1\right)\left(\frac{1}{2}\right)$$
30	1 7	constraddcl	$$⊢\phi \to X+1\in \mathrm{Constr}$$
31	30 24	constrmulcl	$$⊢\phi \to \left(X+1\right)\left(\frac{1}{2}\right)\in \mathrm{Constr}$$
32	29 31	eqeltrd	$$⊢\phi \to \frac{X+1}{2}\in \mathrm{Constr}$$
33	2 3	resqrtcld	$$⊢\phi \to \sqrt{X}\in ℝ$$
34	33	recnd	$$⊢\phi \to \sqrt{X}\in ℂ$$
35	11	subid1d	$$⊢\phi \to 1-0=1$$
36	35 11	eqeltrd	$$⊢\phi \to 1-0\in ℂ$$
37	34 36	mulcld	$$⊢\phi \to \sqrt{X}\left(1-0\right)\in ℂ$$
38	37	addlidd	$$⊢\phi \to 0+\sqrt{X}\left(1-0\right)=\sqrt{X}\left(1-0\right)$$
39	35	oveq2d	$$⊢\phi \to \sqrt{X}\left(1-0\right)=\sqrt{X}\cdot 1$$
40	34	mulridd	$$⊢\phi \to \sqrt{X}\cdot 1=\sqrt{X}$$
41	38 39 40	3eqtrrd	$$⊢\phi \to \sqrt{X}=0+\sqrt{X}\left(1-0\right)$$
42		1red	$$⊢\phi \to 1\in ℝ$$
43	2 42	readdcld	$$⊢\phi \to X+1\in ℝ$$
44	43	rehalfcld	$$⊢\phi \to \frac{X+1}{2}\in ℝ$$
45		2rp	$$⊢2\in {ℝ}^{+}$$
46	45	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
47		0red	$$⊢\phi \to 0\in ℝ$$
48	2	lep1d	$$⊢\phi \to X\le X+1$$
49	47 2 43 3 48	letrd	$$⊢\phi \to 0\le X+1$$
50	43 46 49	divge0d	$$⊢\phi \to 0\le \frac{X+1}{2}$$
51	44 50	absidd	$$⊢\phi \to \left|\frac{X+1}{2}\right|=\frac{X+1}{2}$$
52	28	halfcld	$$⊢\phi \to \frac{X+1}{2}\in ℂ$$
53	52	subid1d	$$⊢\phi \to \left(\frac{X+1}{2}\right)-0=\frac{X+1}{2}$$
54	53	fveq2d	$$⊢\phi \to \left|\left(\frac{X+1}{2}\right)-0\right|=\left|\frac{X+1}{2}\right|$$
55		ax-icn	$$⊢\mathrm{i}\in ℂ$$
56	55	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
57	2 42	resubcld	$$⊢\phi \to X-1\in ℝ$$
58	57	rehalfcld	$$⊢\phi \to \frac{X-1}{2}\in ℝ$$
59	58	recnd	$$⊢\phi \to \frac{X-1}{2}\in ℂ$$
60	56 59	mulneg2d	$$⊢\phi \to \mathrm{i}\left(-\frac{X-1}{2}\right)=-\mathrm{i}\left(\frac{X-1}{2}\right)$$
61	60	oveq2d	$$⊢\phi \to \sqrt{X}+\mathrm{i}\left(-\frac{X-1}{2}\right)=\sqrt{X}+\left(-\mathrm{i}\left(\frac{X-1}{2}\right)\right)$$
62	27	constrcn	$$⊢\phi \to \mathrm{i}\left(\frac{X-1}{2}\right)\in ℂ$$
63	34 62	negsubd	$$⊢\phi \to \sqrt{X}+\left(-\mathrm{i}\left(\frac{X-1}{2}\right)\right)=\sqrt{X}-\mathrm{i}\left(\frac{X-1}{2}\right)$$
64	61 63	eqtr2d	$$⊢\phi \to \sqrt{X}-\mathrm{i}\left(\frac{X-1}{2}\right)=\sqrt{X}+\mathrm{i}\left(-\frac{X-1}{2}\right)$$
65	64	fveq2d	$$⊢\phi \to \left|\sqrt{X}-\mathrm{i}\left(\frac{X-1}{2}\right)\right|=\left|\sqrt{X}+\mathrm{i}\left(-\frac{X-1}{2}\right)\right|$$
66	58	renegcld	$$⊢\phi \to -\frac{X-1}{2}\in ℝ$$
67		absreim	$$⊢\left(\sqrt{X}\in ℝ\wedge -\frac{X-1}{2}\in ℝ\right)\to \left|\sqrt{X}+\mathrm{i}\left(-\frac{X-1}{2}\right)\right|=\sqrt{{\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2}$$
68	33 66 67	syl2anc	$$⊢\phi \to \left|\sqrt{X}+\mathrm{i}\left(-\frac{X-1}{2}\right)\right|=\sqrt{{\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2}$$
69		sq2	$$⊢2^2=4$$
70	69	a1i	$$⊢\phi \to 2^2=4$$
71	70	oveq2d	$$⊢\phi \to \frac{4X}{2^2}=\frac{4X}{4}$$
72		4cn	$$⊢4\in ℂ$$
73	72	a1i	$$⊢\phi \to 4\in ℂ$$
74	13 15 22	expne0d	$$⊢\phi \to 2^2\ne 0$$
75	69 74	eqnetrrid	$$⊢\phi \to 4\ne 0$$
76	10 73 75	divcan3d	$$⊢\phi \to \frac{4X}{4}=X$$
77	71 76	eqtr2d	$$⊢\phi \to X=\frac{4X}{2^2}$$
78	12 13 15	sqdivd	$$⊢\phi \to {\left(\frac{X-1}{2}\right)}^2=\frac{{\left(X-1\right)}^2}{2^2}$$
79	77 78	oveq12d	$$⊢\phi \to X+{\left(\frac{X-1}{2}\right)}^2=\left(\frac{4X}{2^2}\right)+\left(\frac{{\left(X-1\right)}^2}{2^2}\right)$$
80	10	sqsqrtd	$$⊢\phi \to {\sqrt{X}}^2=X$$
81	59	sqnegd	$$⊢\phi \to {\left(-\left(\frac{X-1}{2}\right)\right)}^2={\left(\frac{X-1}{2}\right)}^2$$
82	80 81	oveq12d	$$⊢\phi \to {\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2=X+{\left(\frac{X-1}{2}\right)}^2$$
83	28 13 15	sqdivd	$$⊢\phi \to {\left(\frac{X+1}{2}\right)}^2=\frac{{\left(X+1\right)}^2}{2^2}$$
84	28	sqcld	$$⊢\phi \to {\left(X+1\right)}^2\in ℂ$$
85	12	sqcld	$$⊢\phi \to {\left(X-1\right)}^2\in ℂ$$
86	73 10	mulcld	$$⊢\phi \to 4X\in ℂ$$
87	10 11	binom2subadd	$$⊢\phi \to {\left(X+1\right)}^2-{\left(X-1\right)}^2=4X\cdot 1$$
88	10	mulridd	$$⊢\phi \to X\cdot 1=X$$
89	88	oveq2d	$$⊢\phi \to 4X\cdot 1=4X$$
90	87 89	eqtrd	$$⊢\phi \to {\left(X+1\right)}^2-{\left(X-1\right)}^2=4X$$
91		subadd2	$$⊢\left({\left(X+1\right)}^2\in ℂ\wedge {\left(X-1\right)}^2\in ℂ\wedge 4X\in ℂ\right)\to \left({\left(X+1\right)}^2-{\left(X-1\right)}^2=4X\leftrightarrow 4X+{\left(X-1\right)}^2={\left(X+1\right)}^2\right)$$
92	91	biimpa	$$⊢\left(\left({\left(X+1\right)}^2\in ℂ\wedge {\left(X-1\right)}^2\in ℂ\wedge 4X\in ℂ\right)\wedge {\left(X+1\right)}^2-{\left(X-1\right)}^2=4X\right)\to 4X+{\left(X-1\right)}^2={\left(X+1\right)}^2$$
93	84 85 86 90 92	syl31anc	$$⊢\phi \to 4X+{\left(X-1\right)}^2={\left(X+1\right)}^2$$
94	93	oveq1d	$$⊢\phi \to \frac{4X+{\left(X-1\right)}^2}{2^2}=\frac{{\left(X+1\right)}^2}{2^2}$$
95	13	sqcld	$$⊢\phi \to 2^2\in ℂ$$
96	86 85 95 74	divdird	$$⊢\phi \to \frac{4X+{\left(X-1\right)}^2}{2^2}=\left(\frac{4X}{2^2}\right)+\left(\frac{{\left(X-1\right)}^2}{2^2}\right)$$
97	83 94 96	3eqtr2d	$$⊢\phi \to {\left(\frac{X+1}{2}\right)}^2=\left(\frac{4X}{2^2}\right)+\left(\frac{{\left(X-1\right)}^2}{2^2}\right)$$
98	79 82 97	3eqtr4d	$$⊢\phi \to {\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2={\left(\frac{X+1}{2}\right)}^2$$
99	98	fveq2d	$$⊢\phi \to \sqrt{{\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2}=\sqrt{{\left(\frac{X+1}{2}\right)}^2}$$
100	44 50	sqrtsqd	$$⊢\phi \to \sqrt{{\left(\frac{X+1}{2}\right)}^2}=\frac{X+1}{2}$$
101	99 100	eqtrd	$$⊢\phi \to \sqrt{{\sqrt{X}}^2+{\left(-\left(\frac{X-1}{2}\right)\right)}^2}=\frac{X+1}{2}$$
102	65 68 101	3eqtrd	$$⊢\phi \to \left|\sqrt{X}-\mathrm{i}\left(\frac{X-1}{2}\right)\right|=\frac{X+1}{2}$$
103	51 54 102	3eqtr4rd	$$⊢\phi \to \left|\sqrt{X}-\mathrm{i}\left(\frac{X-1}{2}\right)\right|=\left|\left(\frac{X+1}{2}\right)-0\right|$$
104	5 7 27 32 5 33 34 41 103	constrlccl	$$⊢\phi \to \sqrt{X}\in \mathrm{Constr}$$