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 . (Proposed by Saveliy Skresanov, 3-Nov-2025.) (Contributed by Thierry Arnoux, 6-Nov-2025)

Ref Expression
Hypothesis constrabscl.1 
|- ( ph -> X e. Constr )
Assertion constrsqrtcl 
|- ( ph -> ( sqrt ` X ) e. Constr )

Proof

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