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 
|- ( ph -> X e. Constr )
constrresqrtcl.2 
|- ( ph -> X e. RR )
constrresqrtcl.3 
|- ( ph -> 0 <_ X )
Assertion constrresqrtcl 
|- ( ph -> ( sqrt ` X ) e. Constr )

Proof

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