constrresqrtcl - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > constrresqrtcl		Structured version Visualization version GIF version

Theorem constrresqrtcl 33727

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

**Hypotheses**
Ref	Expression
constrresqrtcl.1	⊢ (𝜑 → 𝑋 ∈ Constr)
constrresqrtcl.2	⊢ (𝜑 → 𝑋 ∈ ℝ)
constrresqrtcl.3	⊢ (𝜑 → 0 ≤ 𝑋)

**Assertion**
Ref	Expression
constrresqrtcl	⊢ (𝜑 → (√‘𝑋) ∈ Constr)

**Proof of Theorem constrresqrtcl**
Step	Hyp	Ref	Expression
1		0zd 12592	. . 3 ⊢ (𝜑 → 0 ∈ ℤ)
2	1	zconstr 33714	. 2 ⊢ (𝜑 → 0 ∈ Constr)
3		1zzd 12615	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
4	3	zconstr 33714	. 2 ⊢ (𝜑 → 1 ∈ Constr)
5		iconstr 33716	. . . 4 ⊢ i ∈ Constr
6	5	a1i 11	. . 3 ⊢ (𝜑 → i ∈ Constr)
7		constrresqrtcl.2	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ ℝ)
8	7	recnd 11255	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℂ)
9		1cnd 11222	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
10	8, 9	subcld 11586	. . . . 5 ⊢ (𝜑 → (𝑋 − 1) ∈ ℂ)
11		2cnd 12310	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
12		2ne0 12336	. . . . . 6 ⊢ 2 ≠ 0
13	12	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
14	10, 11, 13	divrecd 12012	. . . 4 ⊢ (𝜑 → ((𝑋 − 1) / 2) = ((𝑋 − 1) · (1 / 2)))
15	8, 9	negsubd 11592	. . . . . 6 ⊢ (𝜑 → (𝑋 + -1) = (𝑋 − 1))
16		constrresqrtcl.1	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ Constr)
17	4	constrnegcl 33713	. . . . . . 7 ⊢ (𝜑 → -1 ∈ Constr)
18	16, 17	constraddcl 33712	. . . . . 6 ⊢ (𝜑 → (𝑋 + -1) ∈ Constr)
19	15, 18	eqeltrrd 2834	. . . . 5 ⊢ (𝜑 → (𝑋 − 1) ∈ Constr)
20		2z 12616	. . . . . . . 8 ⊢ 2 ∈ ℤ
21	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℤ)
22	21	zconstr 33714	. . . . . 6 ⊢ (𝜑 → 2 ∈ Constr)
23	22, 13	constrinvcl 33723	. . . . 5 ⊢ (𝜑 → (1 / 2) ∈ Constr)
24	19, 23	constrmulcl 33721	. . . 4 ⊢ (𝜑 → ((𝑋 − 1) · (1 / 2)) ∈ Constr)
25	14, 24	eqeltrd 2833	. . 3 ⊢ (𝜑 → ((𝑋 − 1) / 2) ∈ Constr)
26	6, 25	constrmulcl 33721	. 2 ⊢ (𝜑 → (i · ((𝑋 − 1) / 2)) ∈ Constr)
27	8, 9	addcld 11246	. . . 4 ⊢ (𝜑 → (𝑋 + 1) ∈ ℂ)
28	27, 11, 13	divrecd 12012	. . 3 ⊢ (𝜑 → ((𝑋 + 1) / 2) = ((𝑋 + 1) · (1 / 2)))
29	16, 4	constraddcl 33712	. . . 4 ⊢ (𝜑 → (𝑋 + 1) ∈ Constr)
30	29, 23	constrmulcl 33721	. . 3 ⊢ (𝜑 → ((𝑋 + 1) · (1 / 2)) ∈ Constr)
31	28, 30	eqeltrd 2833	. 2 ⊢ (𝜑 → ((𝑋 + 1) / 2) ∈ Constr)
32		constrresqrtcl.3	. . 3 ⊢ (𝜑 → 0 ≤ 𝑋)
33	7, 32	resqrtcld 15423	. 2 ⊢ (𝜑 → (√‘𝑋) ∈ ℝ)
34	33	recnd 11255	. 2 ⊢ (𝜑 → (√‘𝑋) ∈ ℂ)
35	9	subid1d 11575	. . . . . 6 ⊢ (𝜑 → (1 − 0) = 1)
36	35, 9	eqeltrd 2833	. . . . 5 ⊢ (𝜑 → (1 − 0) ∈ ℂ)
37	34, 36	mulcld 11247	. . . 4 ⊢ (𝜑 → ((√‘𝑋) · (1 − 0)) ∈ ℂ)
38	37	addlidd 11428	. . 3 ⊢ (𝜑 → (0 + ((√‘𝑋) · (1 − 0))) = ((√‘𝑋) · (1 − 0)))
39	35	oveq2d 7415	. . 3 ⊢ (𝜑 → ((√‘𝑋) · (1 − 0)) = ((√‘𝑋) · 1))
40	34	mulridd 11244	. . 3 ⊢ (𝜑 → ((√‘𝑋) · 1) = (√‘𝑋))
41	38, 39, 40	3eqtrrd 2774	. 2 ⊢ (𝜑 → (√‘𝑋) = (0 + ((√‘𝑋) · (1 − 0))))
42		1red 11228	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
43	7, 42	readdcld 11256	. . . . 5 ⊢ (𝜑 → (𝑋 + 1) ∈ ℝ)
44	43	rehalfcld 12480	. . . 4 ⊢ (𝜑 → ((𝑋 + 1) / 2) ∈ ℝ)
45		2rp 13005	. . . . . 6 ⊢ 2 ∈ ℝ⁺
46	45	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℝ⁺)
47		0red 11230	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℝ)
48	7	lep1d 12165	. . . . . 6 ⊢ (𝜑 → 𝑋 ≤ (𝑋 + 1))
49	47, 7, 43, 32, 48	letrd 11384	. . . . 5 ⊢ (𝜑 → 0 ≤ (𝑋 + 1))
50	43, 46, 49	divge0d 13083	. . . 4 ⊢ (𝜑 → 0 ≤ ((𝑋 + 1) / 2))
51	44, 50	absidd 15428	. . 3 ⊢ (𝜑 → (abs‘((𝑋 + 1) / 2)) = ((𝑋 + 1) / 2))
52	27	halfcld 12478	. . . . 5 ⊢ (𝜑 → ((𝑋 + 1) / 2) ∈ ℂ)
53	52	subid1d 11575	. . . 4 ⊢ (𝜑 → (((𝑋 + 1) / 2) − 0) = ((𝑋 + 1) / 2))
54	53	fveq2d 6876	. . 3 ⊢ (𝜑 → (abs‘(((𝑋 + 1) / 2) − 0)) = (abs‘((𝑋 + 1) / 2)))
55		ax-icn 11180	. . . . . . . . 9 ⊢ i ∈ ℂ
56	55	a1i 11	. . . . . . . 8 ⊢ (𝜑 → i ∈ ℂ)
57	7, 42	resubcld 11657	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 − 1) ∈ ℝ)
58	57	rehalfcld 12480	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋 − 1) / 2) ∈ ℝ)
59	58	recnd 11255	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 − 1) / 2) ∈ ℂ)
60	56, 59	mulneg2d 11683	. . . . . . 7 ⊢ (𝜑 → (i · -((𝑋 − 1) / 2)) = -(i · ((𝑋 − 1) / 2)))
61	60	oveq2d 7415	. . . . . 6 ⊢ (𝜑 → ((√‘𝑋) + (i · -((𝑋 − 1) / 2))) = ((√‘𝑋) + -(i · ((𝑋 − 1) / 2))))
62	26	constrcn 33710	. . . . . . 7 ⊢ (𝜑 → (i · ((𝑋 − 1) / 2)) ∈ ℂ)
63	34, 62	negsubd 11592	. . . . . 6 ⊢ (𝜑 → ((√‘𝑋) + -(i · ((𝑋 − 1) / 2))) = ((√‘𝑋) − (i · ((𝑋 − 1) / 2))))
64	61, 63	eqtr2d 2770	. . . . 5 ⊢ (𝜑 → ((√‘𝑋) − (i · ((𝑋 − 1) / 2))) = ((√‘𝑋) + (i · -((𝑋 − 1) / 2))))
65	64	fveq2d 6876	. . . 4 ⊢ (𝜑 → (abs‘((√‘𝑋) − (i · ((𝑋 − 1) / 2)))) = (abs‘((√‘𝑋) + (i · -((𝑋 − 1) / 2)))))
66	58	renegcld 11656	. . . . 5 ⊢ (𝜑 → -((𝑋 − 1) / 2) ∈ ℝ)
67		absreim 15299	. . . . 5 ⊢ (((√‘𝑋) ∈ ℝ ∧ -((𝑋 − 1) / 2) ∈ ℝ) → (abs‘((√‘𝑋) + (i · -((𝑋 − 1) / 2)))) = (√‘(((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2))))
68	33, 66, 67	syl2anc 584	. . . 4 ⊢ (𝜑 → (abs‘((√‘𝑋) + (i · -((𝑋 − 1) / 2)))) = (√‘(((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2))))
69		sq2 14203	. . . . . . . . . . 11 ⊢ (2↑2) = 4
70	69	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (2↑2) = 4)
71	70	oveq2d 7415	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝑋) / (2↑2)) = ((4 · 𝑋) / 4))
72		4cn 12317	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
73	72	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℂ)
74	11, 13, 21	expne0d 14159	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑2) ≠ 0)
75	69, 74	eqnetrrid 3006	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
76	8, 73, 75	divcan3d 12014	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝑋) / 4) = 𝑋)
77	71, 76	eqtr2d 2770	. . . . . . . 8 ⊢ (𝜑 → 𝑋 = ((4 · 𝑋) / (2↑2)))
78	10, 11, 13	sqdivd 14166	. . . . . . . 8 ⊢ (𝜑 → (((𝑋 − 1) / 2)↑2) = (((𝑋 − 1)↑2) / (2↑2)))
79	77, 78	oveq12d 7417	. . . . . . 7 ⊢ (𝜑 → (𝑋 + (((𝑋 − 1) / 2)↑2)) = (((4 · 𝑋) / (2↑2)) + (((𝑋 − 1)↑2) / (2↑2))))
80	8	sqsqrtd 15445	. . . . . . . 8 ⊢ (𝜑 → ((√‘𝑋)↑2) = 𝑋)
81	59	sqnegd 14123	. . . . . . . 8 ⊢ (𝜑 → (-((𝑋 − 1) / 2)↑2) = (((𝑋 − 1) / 2)↑2))
82	80, 81	oveq12d 7417	. . . . . . 7 ⊢ (𝜑 → (((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2)) = (𝑋 + (((𝑋 − 1) / 2)↑2)))
83	27, 11, 13	sqdivd 14166	. . . . . . . 8 ⊢ (𝜑 → (((𝑋 + 1) / 2)↑2) = (((𝑋 + 1)↑2) / (2↑2)))
84	27	sqcld 14151	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 + 1)↑2) ∈ ℂ)
85	10	sqcld 14151	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋 − 1)↑2) ∈ ℂ)
86	73, 8	mulcld 11247	. . . . . . . . . 10 ⊢ (𝜑 → (4 · 𝑋) ∈ ℂ)
87	8, 9	binom2subadd 32653	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + 1)↑2) − ((𝑋 − 1)↑2)) = (4 · (𝑋 · 1)))
88	8	mulridd 11244	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 · 1) = 𝑋)
89	88	oveq2d 7415	. . . . . . . . . . 11 ⊢ (𝜑 → (4 · (𝑋 · 1)) = (4 · 𝑋))
90	87, 89	eqtrd 2769	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑋 + 1)↑2) − ((𝑋 − 1)↑2)) = (4 · 𝑋))
91		subadd2 11478	. . . . . . . . . . 11 ⊢ ((((𝑋 + 1)↑2) ∈ ℂ ∧ ((𝑋 − 1)↑2) ∈ ℂ ∧ (4 · 𝑋) ∈ ℂ) → ((((𝑋 + 1)↑2) − ((𝑋 − 1)↑2)) = (4 · 𝑋) ↔ ((4 · 𝑋) + ((𝑋 − 1)↑2)) = ((𝑋 + 1)↑2)))
92	91	biimpa 476	. . . . . . . . . 10 ⊢ (((((𝑋 + 1)↑2) ∈ ℂ ∧ ((𝑋 − 1)↑2) ∈ ℂ ∧ (4 · 𝑋) ∈ ℂ) ∧ (((𝑋 + 1)↑2) − ((𝑋 − 1)↑2)) = (4 · 𝑋)) → ((4 · 𝑋) + ((𝑋 − 1)↑2)) = ((𝑋 + 1)↑2))
93	84, 85, 86, 90, 92	syl31anc 1374	. . . . . . . . 9 ⊢ (𝜑 → ((4 · 𝑋) + ((𝑋 − 1)↑2)) = ((𝑋 + 1)↑2))
94	93	oveq1d 7414	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑋) + ((𝑋 − 1)↑2)) / (2↑2)) = (((𝑋 + 1)↑2) / (2↑2)))
95	11	sqcld 14151	. . . . . . . . 9 ⊢ (𝜑 → (2↑2) ∈ ℂ)
96	86, 85, 95, 74	divdird 12047	. . . . . . . 8 ⊢ (𝜑 → (((4 · 𝑋) + ((𝑋 − 1)↑2)) / (2↑2)) = (((4 · 𝑋) / (2↑2)) + (((𝑋 − 1)↑2) / (2↑2))))
97	83, 94, 96	3eqtr2d 2775	. . . . . . 7 ⊢ (𝜑 → (((𝑋 + 1) / 2)↑2) = (((4 · 𝑋) / (2↑2)) + (((𝑋 − 1)↑2) / (2↑2))))
98	79, 82, 97	3eqtr4d 2779	. . . . . 6 ⊢ (𝜑 → (((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2)) = (((𝑋 + 1) / 2)↑2))
99	98	fveq2d 6876	. . . . 5 ⊢ (𝜑 → (√‘(((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2))) = (√‘(((𝑋 + 1) / 2)↑2)))
100	44, 50	sqrtsqd 15425	. . . . 5 ⊢ (𝜑 → (√‘(((𝑋 + 1) / 2)↑2)) = ((𝑋 + 1) / 2))
101	99, 100	eqtrd 2769	. . . 4 ⊢ (𝜑 → (√‘(((√‘𝑋)↑2) + (-((𝑋 − 1) / 2)↑2))) = ((𝑋 + 1) / 2))
102	65, 68, 101	3eqtrd 2773	. . 3 ⊢ (𝜑 → (abs‘((√‘𝑋) − (i · ((𝑋 − 1) / 2)))) = ((𝑋 + 1) / 2))
103	51, 54, 102	3eqtr4rd 2780	. 2 ⊢ (𝜑 → (abs‘((√‘𝑋) − (i · ((𝑋 − 1) / 2)))) = (abs‘(((𝑋 + 1) / 2) − 0)))
104	2, 4, 26, 31, 2, 33, 34, 41, 103	constrlccl 33707	1 ⊢ (𝜑 → (√‘𝑋) ∈ Constr)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 class class class wbr 5116 ‘cfv 6527 (class class class)co 7399 ℂcc 11119 ℝcr 11120 0cc0 11121 1c1 11122 ici 11123 + caddc 11124 · cmul 11126 ≤ cle 11262 − cmin 11458 -cneg 11459 / cdiv 11886 2c2 12287 4c4 12289 ℤcz 12580 ℝ⁺crp 13000 ↑cexp 14068 √csqrt 15239 abscabs 15240 Constrcconstr 33679

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5246 ax-sep 5263 ax-nul 5273 ax-pow 5332 ax-pr 5399 ax-un 7723 ax-inf2 9647 ax-cnex 11177 ax-resscn 11178 ax-1cn 11179 ax-icn 11180 ax-addcl 11181 ax-addrcl 11182 ax-mulcl 11183 ax-mulrcl 11184 ax-mulcom 11185 ax-addass 11186 ax-mulass 11187 ax-distr 11188 ax-i2m1 11189 ax-1ne0 11190 ax-1rid 11191 ax-rnegex 11192 ax-rrecex 11193 ax-cnre 11194 ax-pre-lttri 11195 ax-pre-lttrn 11196 ax-pre-ltadd 11197 ax-pre-mulgt0 11198 ax-pre-sup 11199 ax-addf 11200

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3357 df-reu 3358 df-rab 3414 df-v 3459 df-sbc 3764 df-csb 3873 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-pss 3944 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-tp 4604 df-op 4606 df-uni 4881 df-int 4920 df-iun 4966 df-iin 4967 df-br 5117 df-opab 5179 df-mpt 5199 df-tr 5227 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6287 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6480 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7356 df-ov 7402 df-oprab 7403 df-mpo 7404 df-of 7665 df-om 7856 df-1st 7982 df-2nd 7983 df-supp 8154 df-frecs 8274 df-wrecs 8305 df-recs 8379 df-rdg 8418 df-1o 8474 df-2o 8475 df-er 8713 df-map 8836 df-pm 8837 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9368 df-fi 9417 df-sup 9448 df-inf 9449 df-oi 9516 df-card 9945 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11460 df-neg 11461 df-div 11887 df-nn 12233 df-2 12295 df-3 12296 df-4 12297 df-5 12298 df-6 12299 df-7 12300 df-8 12301 df-9 12302 df-n0 12494 df-z 12581 df-dec 12701 df-uz 12845 df-q 12957 df-rp 13001 df-xneg 13120 df-xadd 13121 df-xmul 13122 df-ioo 13357 df-ioc 13358 df-ico 13359 df-icc 13360 df-fz 13514 df-fzo 13661 df-fl 13798 df-mod 13876 df-seq 14009 df-exp 14069 df-fac 14280 df-bc 14309 df-hash 14337 df-shft 15073 df-cj 15105 df-re 15106 df-im 15107 df-sqrt 15241 df-abs 15242 df-limsup 15474 df-clim 15491 df-rlim 15492 df-sum 15690 df-ef 16070 df-sin 16072 df-cos 16073 df-pi 16075 df-struct 17151 df-sets 17168 df-slot 17186 df-ndx 17198 df-base 17214 df-ress 17237 df-plusg 17269 df-mulr 17270 df-starv 17271 df-sca 17272 df-vsca 17273 df-ip 17274 df-tset 17275 df-ple 17276 df-ds 17278 df-unif 17279 df-hom 17280 df-cco 17281 df-rest 17421 df-topn 17422 df-0g 17440 df-gsum 17441 df-topgen 17442 df-pt 17443 df-prds 17446 df-xrs 17501 df-qtop 17506 df-imas 17507 df-xps 17509 df-mre 17583 df-mrc 17584 df-acs 17586 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-mulg 19036 df-cntz 19285 df-cmn 19748 df-psmet 21292 df-xmet 21293 df-met 21294 df-bl 21295 df-mopn 21296 df-fbas 21297 df-fg 21298 df-cnfld 21301 df-top 22817 df-topon 22834 df-topsp 22856 df-bases 22869 df-cld 22942 df-ntr 22943 df-cls 22944 df-nei 23021 df-lp 23059 df-perf 23060 df-cn 23150 df-cnp 23151 df-haus 23238 df-tx 23485 df-hmeo 23678 df-fil 23769 df-fm 23861 df-flim 23862 df-flf 23863 df-xms 24244 df-ms 24245 df-tms 24246 df-cncf 24807 df-limc 25804 df-dv 25805 df-log 26501 df-constr 33680

This theorem is referenced by: constrsqrtcl 33729

W3C validator