Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion constrsqrtcl ( 𝜑 → ( √ ‘ 𝑋 ) ∈ Constr )

Proof

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