constrrecl

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

		Ref	Expression
	Hypothesis	constrcjcl.1	$⊢ φ \to X \in Constr$
	Assertion	constrrecl	$⊢ φ \to ℜ (X) \in Constr$

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.1	$⊢ φ \to X \in Constr$
2		simpr	$⊢ (φ \land X \in ℝ) \to X \in ℝ$
3	2	rered	$⊢ (φ \land X \in ℝ) \to ℜ (X) = X$
4	1	adantr	$⊢ (φ \land X \in ℝ) \to X \in Constr$
5	3 4	eqeltrd	$⊢ (φ \land X \in ℝ) \to ℜ (X) \in Constr$
6		0zd	$⊢ φ \to 0 \in ℤ$
7	6	zconstr	$⊢ φ \to 0 \in Constr$
8	7	adantr	$⊢ (φ \land \neg X \in ℝ) \to 0 \in Constr$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10	9	zconstr	$⊢ φ \to 1 \in Constr$
11	10	adantr	$⊢ (φ \land \neg X \in ℝ) \to 1 \in Constr$
12	1	adantr	$⊢ (φ \land \neg X \in ℝ) \to X \in Constr$
13	1	constrcjcl	$⊢ φ \to \overline{X} \in Constr$
14	13	adantr	$⊢ (φ \land \neg X \in ℝ) \to \overline{X} \in Constr$
15	1	constrcn	$⊢ φ \to X \in ℂ$
16	15	recld	$⊢ φ \to ℜ (X) \in ℝ$
17	16	adantr	$⊢ (φ \land \neg X \in ℝ) \to ℜ (X) \in ℝ$
18		halfre	$⊢ \frac{1}{2} \in ℝ$
19	18	a1i	$⊢ (φ \land \neg X \in ℝ) \to \frac{1}{2} \in ℝ$
20	16	recnd	$⊢ φ \to ℜ (X) \in ℂ$
21	20	adantr	$⊢ (φ \land \neg X \in ℝ) \to ℜ (X) \in ℂ$
22		1cnd	$⊢ φ \to 1 \in ℂ$
23	22	subid1d	$⊢ φ \to 1 - 0 = 1$
24	23 22	eqeltrd	$⊢ φ \to 1 - 0 \in ℂ$
25	20 24	mulcld	$⊢ φ \to ℜ (X) (1 - 0) \in ℂ$
26	25	addlidd	$⊢ φ \to 0 + ℜ (X) (1 - 0) = ℜ (X) (1 - 0)$
27	23	oveq2d	$⊢ φ \to ℜ (X) (1 - 0) = ℜ (X) \cdot 1$
28	20	mulridd	$⊢ φ \to ℜ (X) \cdot 1 = ℜ (X)$
29	26 27 28	3eqtrrd	$⊢ φ \to ℜ (X) = 0 + ℜ (X) (1 - 0)$
30	29	adantr	$⊢ (φ \land \neg X \in ℝ) \to ℜ (X) = 0 + ℜ (X) (1 - 0)$
31	15	cjcld	$⊢ φ \to \overline{X} \in ℂ$
32	15 31	addcld	$⊢ φ \to X + \overline{X} \in ℂ$
33		2cnd	$⊢ φ \to 2 \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35	34	a1i	$⊢ φ \to 2 \neq 0$
36	32 33 35	divrec2d	$⊢ φ \to \frac{X + \overline{X}}{2} = (\frac{1}{2}) (X + \overline{X})$
37		reval	$⊢ X \in ℂ \to ℜ (X) = \frac{X + \overline{X}}{2}$
38	15 37	syl	$⊢ φ \to ℜ (X) = \frac{X + \overline{X}}{2}$
39	18	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
40	39	recnd	$⊢ φ \to \frac{1}{2} \in ℂ$
41	40 31 15	subdid	$⊢ φ \to (\frac{1}{2}) (\overline{X} - X) = (\frac{1}{2}) \overline{X} - (\frac{1}{2}) X$
42	41	oveq2d	$⊢ φ \to X + (\frac{1}{2}) (\overline{X} - X) = X + (\frac{1}{2}) \overline{X} - (\frac{1}{2}) X$
43	40 15	mulcld	$⊢ φ \to (\frac{1}{2}) X \in ℂ$
44	40 31	mulcld	$⊢ φ \to (\frac{1}{2}) \overline{X} \in ℂ$
45	15 43 44	subadd23d	$⊢ φ \to X - (\frac{1}{2}) X + (\frac{1}{2}) \overline{X} = X + (\frac{1}{2}) \overline{X} - (\frac{1}{2}) X$
46	22 40 15	subdird	$⊢ φ \to (1 - (\frac{1}{2})) X = 1 X - (\frac{1}{2}) X$
47		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
48	47	a1i	$⊢ φ \to 1 - (\frac{1}{2}) = \frac{1}{2}$
49	48	oveq1d	$⊢ φ \to (1 - (\frac{1}{2})) X = (\frac{1}{2}) X$
50	15	mullidd	$⊢ φ \to 1 X = X$
51	50	oveq1d	$⊢ φ \to 1 X - (\frac{1}{2}) X = X - (\frac{1}{2}) X$
52	46 49 51	3eqtr3rd	$⊢ φ \to X - (\frac{1}{2}) X = (\frac{1}{2}) X$
53	52	oveq1d	$⊢ φ \to X - (\frac{1}{2}) X + (\frac{1}{2}) \overline{X} = (\frac{1}{2}) X + (\frac{1}{2}) \overline{X}$
54	40 15 31	adddid	$⊢ φ \to (\frac{1}{2}) (X + \overline{X}) = (\frac{1}{2}) X + (\frac{1}{2}) \overline{X}$
55	53 54	eqtr4d	$⊢ φ \to X - (\frac{1}{2}) X + (\frac{1}{2}) \overline{X} = (\frac{1}{2}) (X + \overline{X})$
56	42 45 55	3eqtr2d	$⊢ φ \to X + (\frac{1}{2}) (\overline{X} - X) = (\frac{1}{2}) (X + \overline{X})$
57	36 38 56	3eqtr4d	$⊢ φ \to ℜ (X) = X + (\frac{1}{2}) (\overline{X} - X)$
58	57	adantr	$⊢ (φ \land \neg X \in ℝ) \to ℜ (X) = X + (\frac{1}{2}) (\overline{X} - X)$
59	23	fveq2d	$⊢ φ \to \overline{1 - 0} = \overline{1}$
60		1red	$⊢ φ \to 1 \in ℝ$
61	60	cjred	$⊢ φ \to \overline{1} = 1$
62	59 61	eqtrd	$⊢ φ \to \overline{1 - 0} = 1$
63	62	oveq1d	$⊢ φ \to \overline{1 - 0} (\overline{X} - X) = 1 (\overline{X} - X)$
64	31 15	subcld	$⊢ φ \to \overline{X} - X \in ℂ$
65	64	mullidd	$⊢ φ \to 1 (\overline{X} - X) = \overline{X} - X$
66	63 65	eqtrd	$⊢ φ \to \overline{1 - 0} (\overline{X} - X) = \overline{X} - X$
67	66	fveq2d	$⊢ φ \to ℑ (\overline{1 - 0} (\overline{X} - X)) = ℑ (\overline{X} - X)$
68	67	adantr	$⊢ (φ \land \neg X \in ℝ) \to ℑ (\overline{1 - 0} (\overline{X} - X)) = ℑ (\overline{X} - X)$
69	15	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to X \in ℂ$
70		imval2	$⊢ X \in ℂ \to ℑ (X) = \frac{X - \overline{X}}{2 i}$
71	15 70	syl	$⊢ φ \to ℑ (X) = \frac{X - \overline{X}}{2 i}$
72	71	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (X) = \frac{X - \overline{X}}{2 i}$
73	15 31	subcld	$⊢ φ \to X - \overline{X} \in ℂ$
74	73	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to X - \overline{X} \in ℂ$
75	64	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to \overline{X} - X \in ℂ$
76	75	imnegd	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (- (\overline{X} - X)) = - ℑ (\overline{X} - X)$
77	31	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to \overline{X} \in ℂ$
78	77 69	negsubdi2d	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to - (\overline{X} - X) = X - \overline{X}$
79	78	fveq2d	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (- (\overline{X} - X)) = ℑ (X - \overline{X})$
80		simpr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (\overline{X} - X) = 0$
81	80	negeqd	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to - ℑ (\overline{X} - X) = - 0$
82	76 79 81	3eqtr3d	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (X - \overline{X}) = - 0$
83		neg0	$⊢ - 0 = 0$
84	82 83	eqtrdi	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (X - \overline{X}) = 0$
85	74 84	reim0bd	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to X - \overline{X} \in ℝ$
86		cjth	$⊢ X \in ℂ \to (X + \overline{X} \in ℝ \land i (X - \overline{X}) \in ℝ)$
87	15 86	syl	$⊢ φ \to (X + \overline{X} \in ℝ \land i (X - \overline{X}) \in ℝ)$
88	87	simprd	$⊢ φ \to i (X - \overline{X}) \in ℝ$
89	88	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to i (X - \overline{X}) \in ℝ$
90		rimul	$⊢ (X - \overline{X} \in ℝ \land i (X - \overline{X}) \in ℝ) \to X - \overline{X} = 0$
91	85 89 90	syl2anc	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to X - \overline{X} = 0$
92	91	oveq1d	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to \frac{X - \overline{X}}{2 i} = \frac{0}{2 i}$
93		ax-icn	$⊢ i \in ℂ$
94	93	a1i	$⊢ φ \to i \in ℂ$
95	33 94	mulcld	$⊢ φ \to 2 i \in ℂ$
96	95	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to 2 i \in ℂ$
97		ine0	$⊢ i \neq 0$
98	97	a1i	$⊢ φ \to i \neq 0$
99	33 94 35 98	mulne0d	$⊢ φ \to 2 i \neq 0$
100	99	adantr	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to 2 i \neq 0$
101	96 100	div0d	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to \frac{0}{2 i} = 0$
102	72 92 101	3eqtrd	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to ℑ (X) = 0$
103	69 102	reim0bd	$⊢ (φ \land ℑ (\overline{X} - X) = 0) \to X \in ℝ$
104	103	ex	$⊢ φ \to (ℑ (\overline{X} - X) = 0 \to X \in ℝ)$
105	104	necon3bd	$⊢ φ \to (\neg X \in ℝ \to ℑ (\overline{X} - X) \neq 0)$
106	105	imp	$⊢ (φ \land \neg X \in ℝ) \to ℑ (\overline{X} - X) \neq 0$
107	68 106	eqnetrd	$⊢ (φ \land \neg X \in ℝ) \to ℑ (\overline{1 - 0} (\overline{X} - X)) \neq 0$
108	8 11 12 14 17 19 21 30 58 107	constrllcl	$⊢ (φ \land \neg X \in ℝ) \to ℜ (X) \in Constr$
109	5 108	pm2.61dan	$⊢ φ \to ℜ (X) \in Constr$

Metamath Proof Explorer

Theorem constrrecl

Proof