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	⊢ ( 𝜑 → 𝑋 ∈ Constr )
	constrremulcl.2	⊢ ( 𝜑 → 𝑌 ∈ Constr )
	constrremulcl.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	constrremulcl.4	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion	constrremulcl	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ Constr )

Proof

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