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 ⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion constrrecl ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ Constr )

Proof

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