constrsqrtcl

Description: Constructible numbers are closed under taking the square root. This is not generally the case for the cubic root operation, see 2sqr3nconstr . Item (5) of Theorem 7.10 of Stewart p. 96 (Proposed by Saveliy Skresanov, 3-Nov-2025.) (Contributed by Thierry Arnoux, 6-Nov-2025)

		Ref	Expression
	Hypothesis	constrabscl.1	$⊢ φ \to X \in Constr$
	Assertion	constrsqrtcl	$⊢ φ \to \sqrt{X} \in Constr$

Proof

Step	Hyp	Ref	Expression
1		constrabscl.1	$⊢ φ \to X \in Constr$
2		fveq2	$⊢ X = 0 \to \sqrt{X} = \sqrt{0}$
3		sqrt0	$⊢ \sqrt{0} = 0$
4	2 3	eqtrdi	$⊢ X = 0 \to \sqrt{X} = 0$
5		0zd	$⊢ X = 0 \to 0 \in ℤ$
6	5	zconstr	$⊢ X = 0 \to 0 \in Constr$
7	4 6	eqeltrd	$⊢ X = 0 \to \sqrt{X} \in Constr$
8	7	adantl	$⊢ (φ \land X = 0) \to \sqrt{X} \in Constr$
9	1	constrcn	$⊢ φ \to X \in ℂ$
10	9	adantr	$⊢ (φ \land - X \in ℝ^{+}) \to X \in ℂ$
11	10	negnegd	$⊢ (φ \land - X \in ℝ^{+}) \to - (- X) = X$
12	11	fveq2d	$⊢ (φ \land - X \in ℝ^{+}) \to \sqrt{- (- X)} = \sqrt{X}$
13		simpr	$⊢ (φ \land - X \in ℝ^{+}) \to - X \in ℝ^{+}$
14	13	rpred	$⊢ (φ \land - X \in ℝ^{+}) \to - X \in ℝ$
15	13	rpge0d	$⊢ (φ \land - X \in ℝ^{+}) \to 0 \leq - X$
16	14 15	sqrtnegd	$⊢ (φ \land - X \in ℝ^{+}) \to \sqrt{- (- X)} = i \sqrt{- X}$
17	12 16	eqtr3d	$⊢ (φ \land - X \in ℝ^{+}) \to \sqrt{X} = i \sqrt{- X}$
18		iconstr	$⊢ i \in Constr$
19	18	a1i	$⊢ (φ \land - X \in ℝ^{+}) \to i \in Constr$
20	1	adantr	$⊢ (φ \land - X \in ℝ^{+}) \to X \in Constr$
21	20	constrnegcl	$⊢ (φ \land - X \in ℝ^{+}) \to - X \in Constr$
22	21 14 15	constrresqrtcl	$⊢ (φ \land - X \in ℝ^{+}) \to \sqrt{- X} \in Constr$
23	19 22	constrmulcl	$⊢ (φ \land - X \in ℝ^{+}) \to i \sqrt{- X} \in Constr$
24	17 23	eqeltrd	$⊢ (φ \land - X \in ℝ^{+}) \to \sqrt{X} \in Constr$
25	24	adantlr	$⊢ ((φ \land X \neq 0) \land - X \in ℝ^{+}) \to \sqrt{X} \in Constr$
26	9	ad2antrr	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to X \in ℂ$
27	26	abscld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| \in ℝ$
28	27	recnd	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| \in ℂ$
29	28	sqrtcld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{\|X\|} \in ℂ$
30	28 26	addcld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| + X \in ℂ$
31	30	abscld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|\|X\| + X\| \in ℝ$
32	31	recnd	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|\|X\| + X\| \in ℂ$
33	9	ad2antrr	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to X \in ℂ$
34	9	abscld	$⊢ φ \to \|X\| \in ℝ$
35	34	ad2antrr	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \|X\| \in ℝ$
36	35	recnd	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \|X\| \in ℂ$
37		simpr	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \|X\| + X = 0$
38		addeq0	$⊢ (\|X\| \in ℂ \land X \in ℂ) \to (\|X\| + X = 0 \leftrightarrow \|X\| = - X)$
39	38	biimpa	$⊢ ((\|X\| \in ℂ \land X \in ℂ) \land \|X\| + X = 0) \to \|X\| = - X$
40	36 33 37 39	syl21anc	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \|X\| = - X$
41	40 35	eqeltrrd	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to - X \in ℝ$
42	33 41	negrebd	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to X \in ℝ$
43		0red	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to 0 \in ℝ$
44		simplr	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \neg - X \in ℝ^{+}$
45		negelrp	$⊢ X \in ℝ \to (- X \in ℝ^{+} \leftrightarrow X < 0)$
46	45	notbid	$⊢ X \in ℝ \to (\neg - X \in ℝ^{+} \leftrightarrow \neg X < 0)$
47	46	biimpa	$⊢ (X \in ℝ \land \neg - X \in ℝ^{+}) \to \neg X < 0$
48	42 44 47	syl2anc	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \neg X < 0$
49	43 42 48	nltled	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to 0 \leq X$
50	42 49	absidd	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to \|X\| = X$
51	50 40	eqtr3d	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to X = - X$
52	33 51	eqnegad	$⊢ ((φ \land \neg - X \in ℝ^{+}) \land \|X\| + X = 0) \to X = 0$
53	52	ex	$⊢ (φ \land \neg - X \in ℝ^{+}) \to (\|X\| + X = 0 \to X = 0)$
54	53	necon3d	$⊢ (φ \land \neg - X \in ℝ^{+}) \to (X \neq 0 \to \|X\| + X \neq 0)$
55	54	impancom	$⊢ (φ \land X \neq 0) \to (\neg - X \in ℝ^{+} \to \|X\| + X \neq 0)$
56	55	imp	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| + X \neq 0$
57	30 56	absne0d	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|\|X\| + X\| \neq 0$
58	30 32 57	divcld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \frac{\|X\| + X}{\|\|X\| + X\|} \in ℂ$
59	29 58	mulcld	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \in ℂ$
60		eqid	$⊢ \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) = \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})$
61	60	sqreulem	$⊢ (X \in ℂ \land \|X\| + X \neq 0) \to ({\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})}^{2} = X \land 0 \leq ℜ (\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})) \land i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \notin ℝ^{+})$
62	26 56 61	syl2anc	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to ({\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})}^{2} = X \land 0 \leq ℜ (\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})) \land i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \notin ℝ^{+})$
63	62	simp1d	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to {\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|})}^{2} = X$
64	62	simp2d	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to 0 \leq ℜ (\sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}))$
65	62	simp3d	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \notin ℝ^{+}$
66		df-nel	$⊢ i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \notin ℝ^{+} \leftrightarrow \neg i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \in ℝ^{+}$
67	65 66	sylib	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \neg i \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \in ℝ^{+}$
68	59 26 63 64 67	eqsqrtd	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) = \sqrt{X}$
69	1	ad2antrr	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to X \in Constr$
70	69	constrabscl	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| \in Constr$
71	26	absge0d	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to 0 \leq \|X\|$
72	70 27 71	constrresqrtcl	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{\|X\|} \in Constr$
73	70 69	constraddcl	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \|X\| + X \in Constr$
74	73 56	constrdircl	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \frac{\|X\| + X}{\|\|X\| + X\|} \in Constr$
75	72 74	constrmulcl	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{\|X\|} (\frac{\|X\| + X}{\|\|X\| + X\|}) \in Constr$
76	68 75	eqeltrrd	$⊢ ((φ \land X \neq 0) \land \neg - X \in ℝ^{+}) \to \sqrt{X} \in Constr$
77	25 76	pm2.61dan	$⊢ (φ \land X \neq 0) \to \sqrt{X} \in Constr$
78	8 77	pm2.61dane	$⊢ φ \to \sqrt{X} \in Constr$

Metamath Proof Explorer

Theorem constrsqrtcl

Proof