Theorem constrremulcl

Description: If two real numbers X and Y are constructible, then, so is their product. (Contributed by Thierry Arnoux, 2-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		constrremulcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constrremulcl.2	$$⊢\phi \to Y\in \mathrm{Constr}$$
3		constrremulcl.3	$$⊢\phi \to X\in ℝ$$
4		constrremulcl.4	$$⊢\phi \to Y\in ℝ$$
5		simpr	$$⊢\left(\phi \wedge X=0\right)\to X=0$$
6	5	oveq1d	$$⊢\left(\phi \wedge X=0\right)\to XY=0\cdot Y$$
7	4	recnd	$$⊢\phi \to Y\in ℂ$$
8	7	adantr	$$⊢\left(\phi \wedge X=0\right)\to Y\in ℂ$$
9	8	mul02d	$$⊢\left(\phi \wedge X=0\right)\to 0\cdot Y=0$$
10	6 9	eqtrd	$$⊢\left(\phi \wedge X=0\right)\to XY=0$$
11		0nn0	$$⊢0\in {\mathbb{N}}_0$$
12	11	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
13	12	nn0constr	$$⊢\phi \to 0\in \mathrm{Constr}$$
14	13	adantr	$$⊢\left(\phi \wedge X=0\right)\to 0\in \mathrm{Constr}$$
15	10 14	eqeltrd	$$⊢\left(\phi \wedge X=0\right)\to XY\in \mathrm{Constr}$$
16	13	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to 0\in \mathrm{Constr}$$
17	1	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to X\in \mathrm{Constr}$$
18		iconstr	$$⊢\mathrm{i}\in \mathrm{Constr}$$
19	18	a1i	$$⊢\phi \to \mathrm{i}\in \mathrm{Constr}$$
20	19	constrcn	$$⊢\phi \to \mathrm{i}\in ℂ$$
21	20 7	mulcld	$$⊢\phi \to \mathrm{i}Y\in ℂ$$
22	20	subid1d	$$⊢\phi \to \mathrm{i}-0=\mathrm{i}$$
23	22	oveq2d	$$⊢\phi \to Y\left(\mathrm{i}-0\right)=Y\mathrm{i}$$
24	22 20	eqeltrd	$$⊢\phi \to \mathrm{i}-0\in ℂ$$
25	7 24	mulcld	$$⊢\phi \to Y\left(\mathrm{i}-0\right)\in ℂ$$
26	25	addlidd	$$⊢\phi \to 0+Y\left(\mathrm{i}-0\right)=Y\left(\mathrm{i}-0\right)$$
27	20 7	mulcomd	$$⊢\phi \to \mathrm{i}Y=Y\mathrm{i}$$
28	23 26 27	3eqtr4rd	$$⊢\phi \to \mathrm{i}Y=0+Y\left(\mathrm{i}-0\right)$$
29	20 7	absmuld	$$⊢\phi \to \left|\mathrm{i}Y\right|=\left|\mathrm{i}\right|\left|Y\right|$$
30		absi	$$⊢\left|\mathrm{i}\right|=1$$
31	30	a1i	$$⊢\phi \to \left|\mathrm{i}\right|=1$$
32	31	oveq1d	$$⊢\phi \to \left|\mathrm{i}\right|\left|Y\right|=1\left|Y\right|$$
33	7	abscld	$$⊢\phi \to \left|Y\right|\in ℝ$$
34	33	recnd	$$⊢\phi \to \left|Y\right|\in ℂ$$
35	34	mullidd	$$⊢\phi \to 1\left|Y\right|=\left|Y\right|$$
36	29 32 35	3eqtrd	$$⊢\phi \to \left|\mathrm{i}Y\right|=\left|Y\right|$$
37	21	subid1d	$$⊢\phi \to \mathrm{i}Y-0=\mathrm{i}Y$$
38	37	fveq2d	$$⊢\phi \to \left|\mathrm{i}Y-0\right|=\left|\mathrm{i}Y\right|$$
39	7	subid1d	$$⊢\phi \to Y-0=Y$$
40	39	fveq2d	$$⊢\phi \to \left|Y-0\right|=\left|Y\right|$$
41	36 38 40	3eqtr4d	$$⊢\phi \to \left|\mathrm{i}Y-0\right|=\left|Y-0\right|$$
42	13 19 13 2 13 4 21 28 41	constrlccl	$$⊢\phi \to \mathrm{i}Y\in \mathrm{Constr}$$
43	42	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to \mathrm{i}Y\in \mathrm{Constr}$$
44	3	recnd	$$⊢\phi \to X\in ℂ$$
45	44 20	negsubd	$$⊢\phi \to X+\left(-\mathrm{i}\right)=X-\mathrm{i}$$
46	19	constrnegcl	$$⊢\phi \to -\mathrm{i}\in \mathrm{Constr}$$
47	1 46	constraddcl	$$⊢\phi \to X+\left(-\mathrm{i}\right)\in \mathrm{Constr}$$
48	45 47	eqeltrrd	$$⊢\phi \to X-\mathrm{i}\in \mathrm{Constr}$$
49	48 42	constraddcl	$$⊢\phi \to X-\mathrm{i}+\mathrm{i}Y\in \mathrm{Constr}$$
50	49	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to X-\mathrm{i}+\mathrm{i}Y\in \mathrm{Constr}$$
51	4	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to Y\in ℝ$$
52	44 7	mulcld	$$⊢\phi \to XY\in ℂ$$
53	52	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to XY\in ℂ$$
54	44	subid1d	$$⊢\phi \to X-0=X$$
55	54	oveq2d	$$⊢\phi \to Y\left(X-0\right)=YX$$
56	54 44	eqeltrd	$$⊢\phi \to X-0\in ℂ$$
57	7 56	mulcld	$$⊢\phi \to Y\left(X-0\right)\in ℂ$$
58	57	addlidd	$$⊢\phi \to 0+Y\left(X-0\right)=Y\left(X-0\right)$$
59	44 7	mulcomd	$$⊢\phi \to XY=YX$$
60	55 58 59	3eqtr4rd	$$⊢\phi \to XY=0+Y\left(X-0\right)$$
61	60	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to XY=0+Y\left(X-0\right)$$
62	44 20	subcld	$$⊢\phi \to X-\mathrm{i}\in ℂ$$
63	62 21	pncand	$$⊢\phi \to \left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y=X-\mathrm{i}$$
64	63	oveq2d	$$⊢\phi \to Y\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)=Y\left(X-\mathrm{i}\right)$$
65	64	oveq2d	$$⊢\phi \to \mathrm{i}Y+Y\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)=\mathrm{i}Y+Y\left(X-\mathrm{i}\right)$$
66	7 44 20	subdid	$$⊢\phi \to Y\left(X-\mathrm{i}\right)=YX-Y\mathrm{i}$$
67	59 27	oveq12d	$$⊢\phi \to XY-\mathrm{i}Y=YX-Y\mathrm{i}$$
68	66 67	eqtr4d	$$⊢\phi \to Y\left(X-\mathrm{i}\right)=XY-\mathrm{i}Y$$
69	68	oveq2d	$$⊢\phi \to \mathrm{i}Y+Y\left(X-\mathrm{i}\right)=\mathrm{i}Y+XY-\mathrm{i}Y$$
70	21 52	pncan3d	$$⊢\phi \to \mathrm{i}Y+XY-\mathrm{i}Y=XY$$
71	65 69 70	3eqtrrd	$$⊢\phi \to XY=\mathrm{i}Y+Y\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)$$
72	71	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to XY=\mathrm{i}Y+Y\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)$$
73	54	fveq2d	$$⊢\phi \to \overline{X-0}=\bar{X}$$
74	3	cjred	$$⊢\phi \to \bar{X}=X$$
75	73 74	eqtrd	$$⊢\phi \to \overline{X-0}=X$$
76	63 45	eqtr4d	$$⊢\phi \to \left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y=X+\left(-\mathrm{i}\right)$$
77	75 76	oveq12d	$$⊢\phi \to \overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)=X\left(X+\left(-\mathrm{i}\right)\right)$$
78	20	negcld	$$⊢\phi \to -\mathrm{i}\in ℂ$$
79	44 44 78	adddid	$$⊢\phi \to X\left(X+\left(-\mathrm{i}\right)\right)=XX+X\left(-\mathrm{i}\right)$$
80	44 78	mulcomd	$$⊢\phi \to X\left(-\mathrm{i}\right)=\left(-\mathrm{i}\right)X$$
81		mulneg12	$$⊢\left(\mathrm{i}\in ℂ\wedge X\in ℂ\right)\to \left(-\mathrm{i}\right)X=\mathrm{i}\left(-X\right)$$
82	20 44 81	syl2anc	$$⊢\phi \to \left(-\mathrm{i}\right)X=\mathrm{i}\left(-X\right)$$
83	80 82	eqtrd	$$⊢\phi \to X\left(-\mathrm{i}\right)=\mathrm{i}\left(-X\right)$$
84	83	oveq2d	$$⊢\phi \to XX+X\left(-\mathrm{i}\right)=XX+\mathrm{i}\left(-X\right)$$
85	77 79 84	3eqtrd	$$⊢\phi \to \overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)=XX+\mathrm{i}\left(-X\right)$$
86	85	fveq2d	$$⊢\phi \to \Im \left(\overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)\right)=\Im \left(XX+\mathrm{i}\left(-X\right)\right)$$
87	3 3	remulcld	$$⊢\phi \to XX\in ℝ$$
88	3	renegcld	$$⊢\phi \to -X\in ℝ$$
89	87 88	crimd	$$⊢\phi \to \Im \left(XX+\mathrm{i}\left(-X\right)\right)=-X$$
90	86 89	eqtrd	$$⊢\phi \to \Im \left(\overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)\right)=-X$$
91	90	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to \Im \left(\overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)\right)=-X$$
92	44	adantr	$$⊢\left(\phi \wedge X\ne 0\right)\to X\in ℂ$$
93		simpr	$$⊢\left(\phi \wedge X\ne 0\right)\to X\ne 0$$
94	92 93	negne0d	$$⊢\left(\phi \wedge X\ne 0\right)\to -X\ne 0$$
95	91 94	eqnetrd	$$⊢\left(\phi \wedge X\ne 0\right)\to \Im \left(\overline{X-0}\left(\left(X-\mathrm{i}\right)+\mathrm{i}Y-\mathrm{i}Y\right)\right)\ne 0$$
96	16 17 43 50 51 51 53 61 72 95	constrllcl	$$⊢\left(\phi \wedge X\ne 0\right)\to XY\in \mathrm{Constr}$$
97	15 96	pm2.61dane	$$⊢\phi \to XY\in \mathrm{Constr}$$