Theorem constrmulcl

Description: Constructible numbers are closed under complex multiplication. (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypotheses	constrmulcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
	constrmulcl.2	$$⊢\phi \to Y\in \mathrm{Constr}$$
Assertion	constrmulcl	$$⊢\phi \to XY\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrmulcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constrmulcl.2	$$⊢\phi \to Y\in \mathrm{Constr}$$
3	1	constrcn	$$⊢\phi \to X\in ℂ$$
4	3	replimd	$$⊢\phi \to X=\Re \left(X\right)+\mathrm{i}\Im \left(X\right)$$
5	2	constrcn	$$⊢\phi \to Y\in ℂ$$
6	5	replimd	$$⊢\phi \to Y=\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)$$
7	4 6	oveq12d	$$⊢\phi \to XY=\left(\Re \left(X\right)+\mathrm{i}\Im \left(X\right)\right)\left(\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\right)$$
8	3	recld	$$⊢\phi \to \Re \left(X\right)\in ℝ$$
9	8	recnd	$$⊢\phi \to \Re \left(X\right)\in ℂ$$
10		ax-icn	$$⊢\mathrm{i}\in ℂ$$
11	10	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
12	3	imcld	$$⊢\phi \to \Im \left(X\right)\in ℝ$$
13	12	recnd	$$⊢\phi \to \Im \left(X\right)\in ℂ$$
14	11 13	mulcld	$$⊢\phi \to \mathrm{i}\Im \left(X\right)\in ℂ$$
15	5	recld	$$⊢\phi \to \Re \left(Y\right)\in ℝ$$
16	15	recnd	$$⊢\phi \to \Re \left(Y\right)\in ℂ$$
17	5	imcld	$$⊢\phi \to \Im \left(Y\right)\in ℝ$$
18	17	recnd	$$⊢\phi \to \Im \left(Y\right)\in ℂ$$
19	11 18	mulcld	$$⊢\phi \to \mathrm{i}\Im \left(Y\right)\in ℂ$$
20	9 14 16 19	muladdd	$$⊢\phi \to \left(\Re \left(X\right)+\mathrm{i}\Im \left(X\right)\right)\left(\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\right)=\Re \left(X\right)\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)+\Re \left(X\right)\mathrm{i}\Im \left(Y\right)+\Re \left(Y\right)\mathrm{i}\Im \left(X\right)$$
21	1	constrrecl	$$⊢\phi \to \Re \left(X\right)\in \mathrm{Constr}$$
22	2	constrrecl	$$⊢\phi \to \Re \left(Y\right)\in \mathrm{Constr}$$
23	21 22 8 15	constrremulcl	$$⊢\phi \to \Re \left(X\right)\Re \left(Y\right)\in \mathrm{Constr}$$
24	11 18 11 13	mul4d	$$⊢\phi \to \mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)=\mathrm{i}\mathrm{i}\Im \left(Y\right)\Im \left(X\right)$$
25		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
26	25	oveq1i	$$⊢\mathrm{i}\mathrm{i}\Im \left(Y\right)\Im \left(X\right)=-1\Im \left(Y\right)\Im \left(X\right)$$
27	24 26	eqtrdi	$$⊢\phi \to \mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)=-1\Im \left(Y\right)\Im \left(X\right)$$
28		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
29	28	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
30	29	constrnegcl	$$⊢\phi \to -1\in \mathrm{Constr}$$
31	2	constrimcl	$$⊢\phi \to \Im \left(Y\right)\in \mathrm{Constr}$$
32	1	constrimcl	$$⊢\phi \to \Im \left(X\right)\in \mathrm{Constr}$$
33	31 32 17 12	constrremulcl	$$⊢\phi \to \Im \left(Y\right)\Im \left(X\right)\in \mathrm{Constr}$$
34		1red	$$⊢\phi \to 1\in ℝ$$
35	34	renegcld	$$⊢\phi \to -1\in ℝ$$
36	17 12	remulcld	$$⊢\phi \to \Im \left(Y\right)\Im \left(X\right)\in ℝ$$
37	30 33 35 36	constrremulcl	$$⊢\phi \to -1\Im \left(Y\right)\Im \left(X\right)\in \mathrm{Constr}$$
38	27 37	eqeltrd	$$⊢\phi \to \mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
39	23 38	constraddcl	$$⊢\phi \to \Re \left(X\right)\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
40	9 11 18	mul12d	$$⊢\phi \to \Re \left(X\right)\mathrm{i}\Im \left(Y\right)=\mathrm{i}\Re \left(X\right)\Im \left(Y\right)$$
41		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
42	41	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
43		iconstr	$$⊢\mathrm{i}\in \mathrm{Constr}$$
44	43	a1i	$$⊢\phi \to \mathrm{i}\in \mathrm{Constr}$$
45	21 31 8 17	constrremulcl	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\in \mathrm{Constr}$$
46	8 17	remulcld	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\in ℝ$$
47	9 18	mulcld	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\in ℂ$$
48	11 47	mulcld	$$⊢\phi \to \mathrm{i}\Re \left(X\right)\Im \left(Y\right)\in ℂ$$
49		0cnd	$$⊢\phi \to 0\in ℂ$$
50	11 49	subcld	$$⊢\phi \to \mathrm{i}-0\in ℂ$$
51	47 50	mulcld	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\left(\mathrm{i}-0\right)\in ℂ$$
52	51	addlidd	$$⊢\phi \to 0+\Re \left(X\right)\Im \left(Y\right)\left(\mathrm{i}-0\right)=\Re \left(X\right)\Im \left(Y\right)\left(\mathrm{i}-0\right)$$
53	11	subid1d	$$⊢\phi \to \mathrm{i}-0=\mathrm{i}$$
54	53	oveq2d	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\left(\mathrm{i}-0\right)=\Re \left(X\right)\Im \left(Y\right)\mathrm{i}$$
55	47 11	mulcomd	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)\mathrm{i}=\mathrm{i}\Re \left(X\right)\Im \left(Y\right)$$
56	52 54 55	3eqtrrd	$$⊢\phi \to \mathrm{i}\Re \left(X\right)\Im \left(Y\right)=0+\Re \left(X\right)\Im \left(Y\right)\left(\mathrm{i}-0\right)$$
57	11 47	absmuld	$$⊢\phi \to \left|\mathrm{i}\Re \left(X\right)\Im \left(Y\right)\right|=\left|\mathrm{i}\right|\left|\Re \left(X\right)\Im \left(Y\right)\right|$$
58		absi	$$⊢\left|\mathrm{i}\right|=1$$
59	58	a1i	$$⊢\phi \to \left|\mathrm{i}\right|=1$$
60	59	oveq1d	$$⊢\phi \to \left|\mathrm{i}\right|\left|\Re \left(X\right)\Im \left(Y\right)\right|=1\left|\Re \left(X\right)\Im \left(Y\right)\right|$$
61	47	abscld	$$⊢\phi \to \left|\Re \left(X\right)\Im \left(Y\right)\right|\in ℝ$$
62	61	recnd	$$⊢\phi \to \left|\Re \left(X\right)\Im \left(Y\right)\right|\in ℂ$$
63	62	mullidd	$$⊢\phi \to 1\left|\Re \left(X\right)\Im \left(Y\right)\right|=\left|\Re \left(X\right)\Im \left(Y\right)\right|$$
64	57 60 63	3eqtrd	$$⊢\phi \to \left|\mathrm{i}\Re \left(X\right)\Im \left(Y\right)\right|=\left|\Re \left(X\right)\Im \left(Y\right)\right|$$
65	48	subid1d	$$⊢\phi \to \mathrm{i}\Re \left(X\right)\Im \left(Y\right)-0=\mathrm{i}\Re \left(X\right)\Im \left(Y\right)$$
66	65	fveq2d	$$⊢\phi \to \left|\mathrm{i}\Re \left(X\right)\Im \left(Y\right)-0\right|=\left|\mathrm{i}\Re \left(X\right)\Im \left(Y\right)\right|$$
67	47	subid1d	$$⊢\phi \to \Re \left(X\right)\Im \left(Y\right)-0=\Re \left(X\right)\Im \left(Y\right)$$
68	67	fveq2d	$$⊢\phi \to \left|\Re \left(X\right)\Im \left(Y\right)-0\right|=\left|\Re \left(X\right)\Im \left(Y\right)\right|$$
69	64 66 68	3eqtr4d	$$⊢\phi \to \left|\mathrm{i}\Re \left(X\right)\Im \left(Y\right)-0\right|=\left|\Re \left(X\right)\Im \left(Y\right)-0\right|$$
70	42 44 42 45 42 46 48 56 69	constrlccl	$$⊢\phi \to \mathrm{i}\Re \left(X\right)\Im \left(Y\right)\in \mathrm{Constr}$$
71	40 70	eqeltrd	$$⊢\phi \to \Re \left(X\right)\mathrm{i}\Im \left(Y\right)\in \mathrm{Constr}$$
72	16 11 13	mul12d	$$⊢\phi \to \Re \left(Y\right)\mathrm{i}\Im \left(X\right)=\mathrm{i}\Re \left(Y\right)\Im \left(X\right)$$
73	22 32 15 12	constrremulcl	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\in \mathrm{Constr}$$
74	15 12	remulcld	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\in ℝ$$
75	16 13	mulcld	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\in ℂ$$
76	11 75	mulcld	$$⊢\phi \to \mathrm{i}\Re \left(Y\right)\Im \left(X\right)\in ℂ$$
77	75 50	mulcld	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\left(\mathrm{i}-0\right)\in ℂ$$
78	77	addlidd	$$⊢\phi \to 0+\Re \left(Y\right)\Im \left(X\right)\left(\mathrm{i}-0\right)=\Re \left(Y\right)\Im \left(X\right)\left(\mathrm{i}-0\right)$$
79	53	oveq2d	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\left(\mathrm{i}-0\right)=\Re \left(Y\right)\Im \left(X\right)\mathrm{i}$$
80	75 11	mulcomd	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)\mathrm{i}=\mathrm{i}\Re \left(Y\right)\Im \left(X\right)$$
81	78 79 80	3eqtrrd	$$⊢\phi \to \mathrm{i}\Re \left(Y\right)\Im \left(X\right)=0+\Re \left(Y\right)\Im \left(X\right)\left(\mathrm{i}-0\right)$$
82	11 75	absmuld	$$⊢\phi \to \left|\mathrm{i}\Re \left(Y\right)\Im \left(X\right)\right|=\left|\mathrm{i}\right|\left|\Re \left(Y\right)\Im \left(X\right)\right|$$
83	59	oveq1d	$$⊢\phi \to \left|\mathrm{i}\right|\left|\Re \left(Y\right)\Im \left(X\right)\right|=1\left|\Re \left(Y\right)\Im \left(X\right)\right|$$
84	75	abscld	$$⊢\phi \to \left|\Re \left(Y\right)\Im \left(X\right)\right|\in ℝ$$
85	84	recnd	$$⊢\phi \to \left|\Re \left(Y\right)\Im \left(X\right)\right|\in ℂ$$
86	85	mullidd	$$⊢\phi \to 1\left|\Re \left(Y\right)\Im \left(X\right)\right|=\left|\Re \left(Y\right)\Im \left(X\right)\right|$$
87	82 83 86	3eqtrd	$$⊢\phi \to \left|\mathrm{i}\Re \left(Y\right)\Im \left(X\right)\right|=\left|\Re \left(Y\right)\Im \left(X\right)\right|$$
88	76	subid1d	$$⊢\phi \to \mathrm{i}\Re \left(Y\right)\Im \left(X\right)-0=\mathrm{i}\Re \left(Y\right)\Im \left(X\right)$$
89	88	fveq2d	$$⊢\phi \to \left|\mathrm{i}\Re \left(Y\right)\Im \left(X\right)-0\right|=\left|\mathrm{i}\Re \left(Y\right)\Im \left(X\right)\right|$$
90	75	subid1d	$$⊢\phi \to \Re \left(Y\right)\Im \left(X\right)-0=\Re \left(Y\right)\Im \left(X\right)$$
91	90	fveq2d	$$⊢\phi \to \left|\Re \left(Y\right)\Im \left(X\right)-0\right|=\left|\Re \left(Y\right)\Im \left(X\right)\right|$$
92	87 89 91	3eqtr4d	$$⊢\phi \to \left|\mathrm{i}\Re \left(Y\right)\Im \left(X\right)-0\right|=\left|\Re \left(Y\right)\Im \left(X\right)-0\right|$$
93	42 44 42 73 42 74 76 81 92	constrlccl	$$⊢\phi \to \mathrm{i}\Re \left(Y\right)\Im \left(X\right)\in \mathrm{Constr}$$
94	72 93	eqeltrd	$$⊢\phi \to \Re \left(Y\right)\mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
95	71 94	constraddcl	$$⊢\phi \to \Re \left(X\right)\mathrm{i}\Im \left(Y\right)+\Re \left(Y\right)\mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
96	39 95	constraddcl	$$⊢\phi \to \Re \left(X\right)\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\mathrm{i}\Im \left(X\right)+\Re \left(X\right)\mathrm{i}\Im \left(Y\right)+\Re \left(Y\right)\mathrm{i}\Im \left(X\right)\in \mathrm{Constr}$$
97	20 96	eqeltrd	$$⊢\phi \to \left(\Re \left(X\right)+\mathrm{i}\Im \left(X\right)\right)\left(\Re \left(Y\right)+\mathrm{i}\Im \left(Y\right)\right)\in \mathrm{Constr}$$
98	7 97	eqeltrd	$$⊢\phi \to XY\in \mathrm{Constr}$$