Theorem constrimcl

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

	Ref	Expression
Hypothesis	constrcjcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
Assertion	constrimcl	⊢ ( 𝜑 → ( ℑ ‘ 𝑋 ) ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
3	2	zconstr	⊢ ( 𝜑 → 0 ∈ Constr )
4		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
5	4	zconstr	⊢ ( 𝜑 → 1 ∈ Constr )
6	1	constrcn	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
7	6	recld	⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ ℂ )
9		ax-icn	⊢ i ∈ ℂ
10	9	a1i	⊢ ( 𝜑 → i ∈ ℂ )
11	6	imcld	⊢ ( 𝜑 → ( ℑ ‘ 𝑋 ) ∈ ℝ )
12	11	recnd	⊢ ( 𝜑 → ( ℑ ‘ 𝑋 ) ∈ ℂ )
13	10 12	mulcld	⊢ ( 𝜑 → ( i · ( ℑ ‘ 𝑋 ) ) ∈ ℂ )
14	6	replimd	⊢ ( 𝜑 → 𝑋 = ( ( ℜ ‘ 𝑋 ) + ( i · ( ℑ ‘ 𝑋 ) ) ) )
15	8 13 14	mvrladdd	⊢ ( 𝜑 → ( 𝑋 − ( ℜ ‘ 𝑋 ) ) = ( i · ( ℑ ‘ 𝑋 ) ) )
16	6 8	negsubd	⊢ ( 𝜑 → ( 𝑋 + - ( ℜ ‘ 𝑋 ) ) = ( 𝑋 − ( ℜ ‘ 𝑋 ) ) )
17	1	constrrecl	⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ Constr )
18	17	constrnegcl	⊢ ( 𝜑 → - ( ℜ ‘ 𝑋 ) ∈ Constr )
19	1 18	constraddcl	⊢ ( 𝜑 → ( 𝑋 + - ( ℜ ‘ 𝑋 ) ) ∈ Constr )
20	16 19	eqeltrrd	⊢ ( 𝜑 → ( 𝑋 − ( ℜ ‘ 𝑋 ) ) ∈ Constr )
21	15 20	eqeltrrd	⊢ ( 𝜑 → ( i · ( ℑ ‘ 𝑋 ) ) ∈ Constr )
22		1m0e1	⊢ ( 1 − 0 ) = 1
23		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
24	22 23	eqeltrid	⊢ ( 𝜑 → ( 1 − 0 ) ∈ ℂ )
25	12 24	mulcld	⊢ ( 𝜑 → ( ( ℑ ‘ 𝑋 ) · ( 1 − 0 ) ) ∈ ℂ )
26	25	addlidd	⊢ ( 𝜑 → ( 0 + ( ( ℑ ‘ 𝑋 ) · ( 1 − 0 ) ) ) = ( ( ℑ ‘ 𝑋 ) · ( 1 − 0 ) ) )
27	22	a1i	⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
28	27	oveq2d	⊢ ( 𝜑 → ( ( ℑ ‘ 𝑋 ) · ( 1 − 0 ) ) = ( ( ℑ ‘ 𝑋 ) · 1 ) )
29	12	mulridd	⊢ ( 𝜑 → ( ( ℑ ‘ 𝑋 ) · 1 ) = ( ℑ ‘ 𝑋 ) )
30	26 28 29	3eqtrrd	⊢ ( 𝜑 → ( ℑ ‘ 𝑋 ) = ( 0 + ( ( ℑ ‘ 𝑋 ) · ( 1 − 0 ) ) ) )
31	10 12	absmuld	⊢ ( 𝜑 → ( abs ‘ ( i · ( ℑ ‘ 𝑋 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ 𝑋 ) ) ) )
32		absi	⊢ ( abs ‘ i ) = 1
33	32	a1i	⊢ ( 𝜑 → ( abs ‘ i ) = 1 )
34	33	oveq1d	⊢ ( 𝜑 → ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ 𝑋 ) ) ) = ( 1 · ( abs ‘ ( ℑ ‘ 𝑋 ) ) ) )
35	12	abscld	⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝑋 ) ) ∈ ℝ )
36	35	recnd	⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝑋 ) ) ∈ ℂ )
37	36	mullidd	⊢ ( 𝜑 → ( 1 · ( abs ‘ ( ℑ ‘ 𝑋 ) ) ) = ( abs ‘ ( ℑ ‘ 𝑋 ) ) )
38	31 34 37	3eqtrd	⊢ ( 𝜑 → ( abs ‘ ( i · ( ℑ ‘ 𝑋 ) ) ) = ( abs ‘ ( ℑ ‘ 𝑋 ) ) )
39	13	subid1d	⊢ ( 𝜑 → ( ( i · ( ℑ ‘ 𝑋 ) ) − 0 ) = ( i · ( ℑ ‘ 𝑋 ) ) )
40	39	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( i · ( ℑ ‘ 𝑋 ) ) − 0 ) ) = ( abs ‘ ( i · ( ℑ ‘ 𝑋 ) ) ) )
41	12	subid1d	⊢ ( 𝜑 → ( ( ℑ ‘ 𝑋 ) − 0 ) = ( ℑ ‘ 𝑋 ) )
42	41	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( ℑ ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( ℑ ‘ 𝑋 ) ) )
43	38 40 42	3eqtr4rd	⊢ ( 𝜑 → ( abs ‘ ( ( ℑ ‘ 𝑋 ) − 0 ) ) = ( abs ‘ ( ( i · ( ℑ ‘ 𝑋 ) ) − 0 ) ) )
44	3 5 3 21 3 11 12 30 43	constrlccl	⊢ ( 𝜑 → ( ℑ ‘ 𝑋 ) ∈ Constr )