Theorem constrimcl

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

	Ref	Expression
Hypothesis	constrcjcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
Assertion	constrimcl	$$⊢\phi \to \Im \left(X\right)\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
3	2	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
4		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
5	4	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
6	1	constrcn	$$⊢\phi \to X\in ℂ$$
7	6	recld	$$⊢\phi \to \Re \left(X\right)\in ℝ$$
8	7	recnd	$$⊢\phi \to \Re \left(X\right)\in ℂ$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10	9	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
11	6	imcld	$$⊢\phi \to \Im \left(X\right)\in ℝ$$
12	11	recnd	$$⊢\phi \to \Im \left(X\right)\in ℂ$$
13	10 12	mulcld	$$⊢\phi \to \mathrm{i}\Im \left(X\right)\in ℂ$$
14	6	replimd	$$⊢\phi \to X=\Re \left(X\right)+\mathrm{i}\Im \left(X\right)$$
15	8 13 14	mvrladdd	$$⊢\phi \to X-\Re \left(X\right)=\mathrm{i}\Im \left(X\right)$$
16	6 8	negsubd	$$⊢\phi \to X+\left(-\Re \left(X\right)\right)=X-\Re \left(X\right)$$
17	1	constrrecl	$$⊢\phi \to \Re \left(X\right)\in \mathrm{Constr}$$
18	17	constrnegcl	$$⊢\phi \to -\Re \left(X\right)\in \mathrm{Constr}$$
19	1 18	constraddcl	$$⊢\phi \to X+\left(-\Re \left(X\right)\right)\in \mathrm{Constr}$$
20	16 19	eqeltrrd	$$⊢\phi \to X-\Re \left(X\right)\in \mathrm{Constr}$$
21	15 20	eqeltrrd	$$⊢\phi \to \mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
22		1m0e1	$$⊢1-0=1$$
23		1cnd	$$⊢\phi \to 1\in ℂ$$
24	22 23	eqeltrid	$$⊢\phi \to 1-0\in ℂ$$
25	12 24	mulcld	$$⊢\phi \to \Im \left(X\right)\left(1-0\right)\in ℂ$$
26	25	addlidd	$$⊢\phi \to 0+\Im \left(X\right)\left(1-0\right)=\Im \left(X\right)\left(1-0\right)$$
27	22	a1i	$$⊢\phi \to 1-0=1$$
28	27	oveq2d	$$⊢\phi \to \Im \left(X\right)\left(1-0\right)=\Im \left(X\right)\cdot 1$$
29	12	mulridd	$$⊢\phi \to \Im \left(X\right)\cdot 1=\Im \left(X\right)$$
30	26 28 29	3eqtrrd	$$⊢\phi \to \Im \left(X\right)=0+\Im \left(X\right)\left(1-0\right)$$
31	10 12	absmuld	$$⊢\phi \to \left|\mathrm{i}\Im \left(X\right)\right|=\left|\mathrm{i}\right|\left|\Im \left(X\right)\right|$$
32		absi	$$⊢\left|\mathrm{i}\right|=1$$
33	32	a1i	$$⊢\phi \to \left|\mathrm{i}\right|=1$$
34	33	oveq1d	$$⊢\phi \to \left|\mathrm{i}\right|\left|\Im \left(X\right)\right|=1\left|\Im \left(X\right)\right|$$
35	12	abscld	$$⊢\phi \to \left|\Im \left(X\right)\right|\in ℝ$$
36	35	recnd	$$⊢\phi \to \left|\Im \left(X\right)\right|\in ℂ$$
37	36	mullidd	$$⊢\phi \to 1\left|\Im \left(X\right)\right|=\left|\Im \left(X\right)\right|$$
38	31 34 37	3eqtrd	$$⊢\phi \to \left|\mathrm{i}\Im \left(X\right)\right|=\left|\Im \left(X\right)\right|$$
39	13	subid1d	$$⊢\phi \to \mathrm{i}\Im \left(X\right)-0=\mathrm{i}\Im \left(X\right)$$
40	39	fveq2d	$$⊢\phi \to \left|\mathrm{i}\Im \left(X\right)-0\right|=\left|\mathrm{i}\Im \left(X\right)\right|$$
41	12	subid1d	$$⊢\phi \to \Im \left(X\right)-0=\Im \left(X\right)$$
42	41	fveq2d	$$⊢\phi \to \left|\Im \left(X\right)-0\right|=\left|\Im \left(X\right)\right|$$
43	38 40 42	3eqtr4rd	$$⊢\phi \to \left|\Im \left(X\right)-0\right|=\left|\mathrm{i}\Im \left(X\right)-0\right|$$
44	3 5 3 21 3 11 12 30 43	constrlccl	$$⊢\phi \to \Im \left(X\right)\in \mathrm{Constr}$$