Theorem constrinvcl

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

	Ref	Expression
Hypotheses	constrinvcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
	constrinvcl.2	$$⊢\phi \to X\ne 0$$
Assertion	constrinvcl	$$⊢\phi \to \frac{1}{X}\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrinvcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constrinvcl.2	$$⊢\phi \to X\ne 0$$
3	1	adantr	$$⊢\left(\phi \wedge X\in ℝ\right)\to X\in \mathrm{Constr}$$
4	2	adantr	$$⊢\left(\phi \wedge X\in ℝ\right)\to X\ne 0$$
5		simpr	$$⊢\left(\phi \wedge X\in ℝ\right)\to X\in ℝ$$
6	3 4 5	constrreinvcl	$$⊢\left(\phi \wedge X\in ℝ\right)\to \frac{1}{X}\in \mathrm{Constr}$$
7		1cnd	$$⊢\phi \to 1\in ℂ$$
8	1	constrcn	$$⊢\phi \to X\in ℂ$$
9	7 8 2	absdivd	$$⊢\phi \to \left|\frac{1}{X}\right|=\frac{\left|1\right|}{\left|X\right|}$$
10		abs1	$$⊢\left|1\right|=1$$
11	10	oveq1i	$$⊢\frac{\left|1\right|}{\left|X\right|}=\frac{1}{\left|X\right|}$$
12	9 11	eqtr2di	$$⊢\phi \to \frac{1}{\left|X\right|}=\left|\frac{1}{X}\right|$$
13	8 2	reccld	$$⊢\phi \to \frac{1}{X}\in ℂ$$
14	8 2	recne0d	$$⊢\phi \to \frac{1}{X}\ne 0$$
15	13 14	efiargd	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}=\frac{\frac{1}{X}}{\left|\frac{1}{X}\right|}$$
16	12 15	oveq12d	$$⊢\phi \to \left(\frac{1}{\left|X\right|}\right){\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}=\left|\frac{1}{X}\right|\left(\frac{\frac{1}{X}}{\left|\frac{1}{X}\right|}\right)$$
17	13	abscld	$$⊢\phi \to \left|\frac{1}{X}\right|\in ℝ$$
18	17	recnd	$$⊢\phi \to \left|\frac{1}{X}\right|\in ℂ$$
19	13 14	absne0d	$$⊢\phi \to \left|\frac{1}{X}\right|\ne 0$$
20	13 18 19	divcan2d	$$⊢\phi \to \left|\frac{1}{X}\right|\left(\frac{\frac{1}{X}}{\left|\frac{1}{X}\right|}\right)=\frac{1}{X}$$
21	16 20	eqtrd	$$⊢\phi \to \left(\frac{1}{\left|X\right|}\right){\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}=\frac{1}{X}$$
22	21	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \left(\frac{1}{\left|X\right|}\right){\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}=\frac{1}{X}$$
23		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
24	23	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
25		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
26	25	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
27	8	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
28	27	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
29	7	subid1d	$$⊢\phi \to 1-0=1$$
30	29 7	eqeltrd	$$⊢\phi \to 1-0\in ℂ$$
31	28 30	mulcld	$$⊢\phi \to \left|X\right|\left(1-0\right)\in ℂ$$
32	31	addlidd	$$⊢\phi \to 0+\left|X\right|\left(1-0\right)=\left|X\right|\left(1-0\right)$$
33	29	oveq2d	$$⊢\phi \to \left|X\right|\left(1-0\right)=\left|X\right|\cdot 1$$
34	28	mulridd	$$⊢\phi \to \left|X\right|\cdot 1=\left|X\right|$$
35	32 33 34	3eqtrrd	$$⊢\phi \to \left|X\right|=0+\left|X\right|\left(1-0\right)$$
36	8	absge0d	$$⊢\phi \to 0\le \left|X\right|$$
37	27 36	absidd	$$⊢\phi \to \left|\left|X\right|\right|=\left|X\right|$$
38	28	subid1d	$$⊢\phi \to \left|X\right|-0=\left|X\right|$$
39	38	fveq2d	$$⊢\phi \to \left|\left|X\right|-0\right|=\left|\left|X\right|\right|$$
40	8	subid1d	$$⊢\phi \to X-0=X$$
41	40	fveq2d	$$⊢\phi \to \left|X-0\right|=\left|X\right|$$
42	37 39 41	3eqtr4d	$$⊢\phi \to \left|\left|X\right|-0\right|=\left|X-0\right|$$
43	24 26 24 1 24 27 28 35 42	constrlccl	$$⊢\phi \to \left|X\right|\in \mathrm{Constr}$$
44	8 2	absne0d	$$⊢\phi \to \left|X\right|\ne 0$$
45	43 44 27	constrreinvcl	$$⊢\phi \to \frac{1}{\left|X\right|}\in \mathrm{Constr}$$
46	45	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \frac{1}{\left|X\right|}\in \mathrm{Constr}$$
47	8	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to X\in ℂ$$
48	2	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to X\ne 0$$
49	8	adantr	$$⊢\left(\phi \wedge -X\in {ℝ}^{+}\right)\to X\in ℂ$$
50		simpr	$$⊢\left(\phi \wedge -X\in {ℝ}^{+}\right)\to -X\in {ℝ}^{+}$$
51	50	rpred	$$⊢\left(\phi \wedge -X\in {ℝ}^{+}\right)\to -X\in ℝ$$
52	49 51	negrebd	$$⊢\left(\phi \wedge -X\in {ℝ}^{+}\right)\to X\in ℝ$$
53	52	stoic1a	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \neg -X\in {ℝ}^{+}$$
54	47 48 53	arginv	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \Im \left(\log \left(\frac{1}{X}\right)\right)=-\Im \left(\log X\right)$$
55	47 48 53	argcj	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \Im \left(\log \bar{X}\right)=-\Im \left(\log X\right)$$
56	54 55	eqtr4d	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \Im \left(\log \left(\frac{1}{X}\right)\right)=\Im \left(\log \bar{X}\right)$$
57	56	oveq2d	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)=\mathrm{i}\Im \left(\log \bar{X}\right)$$
58	57	fveq2d	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}={\mathrm{e}}^{\mathrm{i}\Im \left(\log \bar{X}\right)}$$
59	8	cjcld	$$⊢\phi \to \bar{X}\in ℂ$$
60	8 2	cjne0d	$$⊢\phi \to \bar{X}\ne 0$$
61	59 60	efiargd	$$⊢\phi \to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \bar{X}\right)}=\frac{\bar{X}}{\left|\bar{X}\right|}$$
62	61	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \bar{X}\right)}=\frac{\bar{X}}{\left|\bar{X}\right|}$$
63	58 62	eqtrd	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}=\frac{\bar{X}}{\left|\bar{X}\right|}$$
64	1	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to X\in \mathrm{Constr}$$
65	64	constrcjcl	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \bar{X}\in \mathrm{Constr}$$
66	60	adantr	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \bar{X}\ne 0$$
67	65 66	constrdircl	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \frac{\bar{X}}{\left|\bar{X}\right|}\in \mathrm{Constr}$$
68	63 67	eqeltrd	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to {\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}\in \mathrm{Constr}$$
69	46 68	constrmulcl	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \left(\frac{1}{\left|X\right|}\right){\mathrm{e}}^{\mathrm{i}\Im \left(\log \left(\frac{1}{X}\right)\right)}\in \mathrm{Constr}$$
70	22 69	eqeltrrd	$$⊢\left(\phi \wedge \neg X\in ℝ\right)\to \frac{1}{X}\in \mathrm{Constr}$$
71	6 70	pm2.61dan	$$⊢\phi \to \frac{1}{X}\in \mathrm{Constr}$$