Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
constrresqrtcl.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
constrresqrtcl.3 ⊢ ( 𝜑 → 0 ≤ 𝑋 )
Assertion constrresqrtcl ( 𝜑 → ( √ ‘ 𝑋 ) ∈ Constr )

Proof

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