Metamath Proof Explorer

Theorem constrrecl

Description: Constructible numbers are closed under taking the real part. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Hypothesis constrcjcl.1 
|- ( ph -> X e. Constr )
Assertion constrrecl 
|- ( ph -> ( Re ` X ) e. Constr )

Proof

Step Hyp Ref Expression
1 constrcjcl.1 
 |-  ( ph -> X e. Constr )
2 simpr 
 |-  ( ( ph /\ X e. RR ) -> X e. RR )
3 2 rered 
 |-  ( ( ph /\ X e. RR ) -> ( Re ` X ) = X )
4 1 adantr 
 |-  ( ( ph /\ X e. RR ) -> X e. Constr )
5 3 4 eqeltrd 
 |-  ( ( ph /\ X e. RR ) -> ( Re ` X ) e. Constr )
6 0zd 
 |-  ( ph -> 0 e. ZZ )
7 6 zconstr 
 |-  ( ph -> 0 e. Constr )
8 7 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> 0 e. Constr )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 9 zconstr 
 |-  ( ph -> 1 e. Constr )
11 10 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> 1 e. Constr )
12 1 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> X e. Constr )
13 1 constrcjcl 
 |-  ( ph -> ( * ` X ) e. Constr )
14 13 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( * ` X ) e. Constr )
15 1 constrcn 
 |-  ( ph -> X e. CC )
16 15 recld 
 |-  ( ph -> ( Re ` X ) e. RR )
17 16 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( Re ` X ) e. RR )
18 halfre 
 |-  ( 1 / 2 ) e. RR
19 18 a1i 
 |-  ( ( ph /\ -. X e. RR ) -> ( 1 / 2 ) e. RR )
20 16 recnd 
 |-  ( ph -> ( Re ` X ) e. CC )
21 20 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( Re ` X ) e. CC )
22 1cnd 
 |-  ( ph -> 1 e. CC )
23 22 subid1d 
 |-  ( ph -> ( 1 - 0 ) = 1 )
24 23 22 eqeltrd 
 |-  ( ph -> ( 1 - 0 ) e. CC )
25 20 24 mulcld 
 |-  ( ph -> ( ( Re ` X ) x. ( 1 - 0 ) ) e. CC )
26 25 addlidd 
 |-  ( ph -> ( 0 + ( ( Re ` X ) x. ( 1 - 0 ) ) ) = ( ( Re ` X ) x. ( 1 - 0 ) ) )
27 23 oveq2d 
 |-  ( ph -> ( ( Re ` X ) x. ( 1 - 0 ) ) = ( ( Re ` X ) x. 1 ) )
28 20 mulridd 
 |-  ( ph -> ( ( Re ` X ) x. 1 ) = ( Re ` X ) )
29 26 27 28 3eqtrrd 
 |-  ( ph -> ( Re ` X ) = ( 0 + ( ( Re ` X ) x. ( 1 - 0 ) ) ) )
30 29 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( Re ` X ) = ( 0 + ( ( Re ` X ) x. ( 1 - 0 ) ) ) )
31 15 cjcld 
 |-  ( ph -> ( * ` X ) e. CC )
32 15 31 addcld 
 |-  ( ph -> ( X + ( * ` X ) ) e. CC )
33 2cnd 
 |-  ( ph -> 2 e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( ph -> 2 =/= 0 )
36 32 33 35 divrec2d 
 |-  ( ph -> ( ( X + ( * ` X ) ) / 2 ) = ( ( 1 / 2 ) x. ( X + ( * ` X ) ) ) )
37 reval 
 |-  ( X e. CC -> ( Re ` X ) = ( ( X + ( * ` X ) ) / 2 ) )
38 15 37 syl 
 |-  ( ph -> ( Re ` X ) = ( ( X + ( * ` X ) ) / 2 ) )
39 18 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
40 39 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
41 40 31 15 subdid 
 |-  ( ph -> ( ( 1 / 2 ) x. ( ( * ` X ) - X ) ) = ( ( ( 1 / 2 ) x. ( * ` X ) ) - ( ( 1 / 2 ) x. X ) ) )
42 41 oveq2d 
 |-  ( ph -> ( X + ( ( 1 / 2 ) x. ( ( * ` X ) - X ) ) ) = ( X + ( ( ( 1 / 2 ) x. ( * ` X ) ) - ( ( 1 / 2 ) x. X ) ) ) )
43 40 15 mulcld 
 |-  ( ph -> ( ( 1 / 2 ) x. X ) e. CC )
44 40 31 mulcld 
 |-  ( ph -> ( ( 1 / 2 ) x. ( * ` X ) ) e. CC )
45 15 43 44 subadd23d 
 |-  ( ph -> ( ( X - ( ( 1 / 2 ) x. X ) ) + ( ( 1 / 2 ) x. ( * ` X ) ) ) = ( X + ( ( ( 1 / 2 ) x. ( * ` X ) ) - ( ( 1 / 2 ) x. X ) ) ) )
46 22 40 15 subdird 
 |-  ( ph -> ( ( 1 - ( 1 / 2 ) ) x. X ) = ( ( 1 x. X ) - ( ( 1 / 2 ) x. X ) ) )
47 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
48 47 a1i 
 |-  ( ph -> ( 1 - ( 1 / 2 ) ) = ( 1 / 2 ) )
49 48 oveq1d 
 |-  ( ph -> ( ( 1 - ( 1 / 2 ) ) x. X ) = ( ( 1 / 2 ) x. X ) )
50 15 mullidd 
 |-  ( ph -> ( 1 x. X ) = X )
51 50 oveq1d 
 |-  ( ph -> ( ( 1 x. X ) - ( ( 1 / 2 ) x. X ) ) = ( X - ( ( 1 / 2 ) x. X ) ) )
52 46 49 51 3eqtr3rd 
 |-  ( ph -> ( X - ( ( 1 / 2 ) x. X ) ) = ( ( 1 / 2 ) x. X ) )
53 52 oveq1d 
 |-  ( ph -> ( ( X - ( ( 1 / 2 ) x. X ) ) + ( ( 1 / 2 ) x. ( * ` X ) ) ) = ( ( ( 1 / 2 ) x. X ) + ( ( 1 / 2 ) x. ( * ` X ) ) ) )
54 40 15 31 adddid 
 |-  ( ph -> ( ( 1 / 2 ) x. ( X + ( * ` X ) ) ) = ( ( ( 1 / 2 ) x. X ) + ( ( 1 / 2 ) x. ( * ` X ) ) ) )
55 53 54 eqtr4d 
 |-  ( ph -> ( ( X - ( ( 1 / 2 ) x. X ) ) + ( ( 1 / 2 ) x. ( * ` X ) ) ) = ( ( 1 / 2 ) x. ( X + ( * ` X ) ) ) )
56 42 45 55 3eqtr2d 
 |-  ( ph -> ( X + ( ( 1 / 2 ) x. ( ( * ` X ) - X ) ) ) = ( ( 1 / 2 ) x. ( X + ( * ` X ) ) ) )
57 36 38 56 3eqtr4d 
 |-  ( ph -> ( Re ` X ) = ( X + ( ( 1 / 2 ) x. ( ( * ` X ) - X ) ) ) )
58 57 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( Re ` X ) = ( X + ( ( 1 / 2 ) x. ( ( * ` X ) - X ) ) ) )
59 23 fveq2d 
 |-  ( ph -> ( * ` ( 1 - 0 ) ) = ( * ` 1 ) )
60 1red 
 |-  ( ph -> 1 e. RR )
61 60 cjred 
 |-  ( ph -> ( * ` 1 ) = 1 )
62 59 61 eqtrd 
 |-  ( ph -> ( * ` ( 1 - 0 ) ) = 1 )
63 62 oveq1d 
 |-  ( ph -> ( ( * ` ( 1 - 0 ) ) x. ( ( * ` X ) - X ) ) = ( 1 x. ( ( * ` X ) - X ) ) )
64 31 15 subcld 
 |-  ( ph -> ( ( * ` X ) - X ) e. CC )
65 64 mullidd 
 |-  ( ph -> ( 1 x. ( ( * ` X ) - X ) ) = ( ( * ` X ) - X ) )
66 63 65 eqtrd 
 |-  ( ph -> ( ( * ` ( 1 - 0 ) ) x. ( ( * ` X ) - X ) ) = ( ( * ` X ) - X ) )
67 66 fveq2d 
 |-  ( ph -> ( Im ` ( ( * ` ( 1 - 0 ) ) x. ( ( * ` X ) - X ) ) ) = ( Im ` ( ( * ` X ) - X ) ) )
68 67 adantr 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( ( * ` ( 1 - 0 ) ) x. ( ( * ` X ) - X ) ) ) = ( Im ` ( ( * ` X ) - X ) ) )
69 15 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> X e. CC )
70 imval2 
 |-  ( X e. CC -> ( Im ` X ) = ( ( X - ( * ` X ) ) / ( 2 x. _i ) ) )
71 15 70 syl 
 |-  ( ph -> ( Im ` X ) = ( ( X - ( * ` X ) ) / ( 2 x. _i ) ) )
72 71 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` X ) = ( ( X - ( * ` X ) ) / ( 2 x. _i ) ) )
73 15 31 subcld 
 |-  ( ph -> ( X - ( * ` X ) ) e. CC )
74 73 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( X - ( * ` X ) ) e. CC )
75 64 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( ( * ` X ) - X ) e. CC )
76 75 imnegd 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` -u ( ( * ` X ) - X ) ) = -u ( Im ` ( ( * ` X ) - X ) ) )
77 31 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( * ` X ) e. CC )
78 77 69 negsubdi2d 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> -u ( ( * ` X ) - X ) = ( X - ( * ` X ) ) )
79 78 fveq2d 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` -u ( ( * ` X ) - X ) ) = ( Im ` ( X - ( * ` X ) ) ) )
80 simpr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` ( ( * ` X ) - X ) ) = 0 )
81 80 negeqd 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> -u ( Im ` ( ( * ` X ) - X ) ) = -u 0 )
82 76 79 81 3eqtr3d 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` ( X - ( * ` X ) ) ) = -u 0 )
83 neg0 
 |-  -u 0 = 0
84 82 83 eqtrdi 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` ( X - ( * ` X ) ) ) = 0 )
85 74 84 reim0bd 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( X - ( * ` X ) ) e. RR )
86 cjth 
 |-  ( X e. CC -> ( ( X + ( * ` X ) ) e. RR /\ ( _i x. ( X - ( * ` X ) ) ) e. RR ) )
87 15 86 syl 
 |-  ( ph -> ( ( X + ( * ` X ) ) e. RR /\ ( _i x. ( X - ( * ` X ) ) ) e. RR ) )
88 87 simprd 
 |-  ( ph -> ( _i x. ( X - ( * ` X ) ) ) e. RR )
89 88 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( _i x. ( X - ( * ` X ) ) ) e. RR )
90 rimul 
 |-  ( ( ( X - ( * ` X ) ) e. RR /\ ( _i x. ( X - ( * ` X ) ) ) e. RR ) -> ( X - ( * ` X ) ) = 0 )
91 85 89 90 syl2anc 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( X - ( * ` X ) ) = 0 )
92 91 oveq1d 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( ( X - ( * ` X ) ) / ( 2 x. _i ) ) = ( 0 / ( 2 x. _i ) ) )
93 ax-icn 
 |-  _i e. CC
94 93 a1i 
 |-  ( ph -> _i e. CC )
95 33 94 mulcld 
 |-  ( ph -> ( 2 x. _i ) e. CC )
96 95 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( 2 x. _i ) e. CC )
97 ine0 
 |-  _i =/= 0
98 97 a1i 
 |-  ( ph -> _i =/= 0 )
99 33 94 35 98 mulne0d 
 |-  ( ph -> ( 2 x. _i ) =/= 0 )
100 99 adantr 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( 2 x. _i ) =/= 0 )
101 96 100 div0d 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( 0 / ( 2 x. _i ) ) = 0 )
102 72 92 101 3eqtrd 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> ( Im ` X ) = 0 )
103 69 102 reim0bd 
 |-  ( ( ph /\ ( Im ` ( ( * ` X ) - X ) ) = 0 ) -> X e. RR )
104 103 ex 
 |-  ( ph -> ( ( Im ` ( ( * ` X ) - X ) ) = 0 -> X e. RR ) )
105 104 necon3bd 
 |-  ( ph -> ( -. X e. RR -> ( Im ` ( ( * ` X ) - X ) ) =/= 0 ) )
106 105 imp 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( ( * ` X ) - X ) ) =/= 0 )
107 68 106 eqnetrd 
 |-  ( ( ph /\ -. X e. RR ) -> ( Im ` ( ( * ` ( 1 - 0 ) ) x. ( ( * ` X ) - X ) ) ) =/= 0 )
108 8 11 12 14 17 19 21 30 58 107 constrllcl 
 |-  ( ( ph /\ -. X e. RR ) -> ( Re ` X ) e. Constr )
109 5 108 pm2.61dan 
 |-  ( ph -> ( Re ` X ) e. Constr )