Theorem constrreinvcl

Description: If a real number X is constructible, then, so is its 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$$
	constrreinvcl.3	$$⊢\phi \to X\in ℝ$$
Assertion	constrreinvcl	$$⊢\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		constrreinvcl.3	$$⊢\phi \to X\in ℝ$$
4		iconstr	$$⊢\mathrm{i}\in \mathrm{Constr}$$
5	4	a1i	$$⊢\phi \to \mathrm{i}\in \mathrm{Constr}$$
6		1cnd	$$⊢\phi \to 1\in ℂ$$
7	5 1	constrmulcl	$$⊢\phi \to \mathrm{i}X\in \mathrm{Constr}$$
8	7	constrcn	$$⊢\phi \to \mathrm{i}X\in ℂ$$
9	6 8	negsubd	$$⊢\phi \to 1+\left(-\mathrm{i}X\right)=1-\mathrm{i}X$$
10		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
11	10	zconstr	$$⊢\phi \to 1\in \mathrm{Constr}$$
12	7	constrnegcl	$$⊢\phi \to -\mathrm{i}X\in \mathrm{Constr}$$
13	11 12	constraddcl	$$⊢\phi \to 1+\left(-\mathrm{i}X\right)\in \mathrm{Constr}$$
14	9 13	eqeltrrd	$$⊢\phi \to 1-\mathrm{i}X\in \mathrm{Constr}$$
15	5 14	constraddcl	$$⊢\phi \to \mathrm{i}+1-\mathrm{i}X\in \mathrm{Constr}$$
16		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
17	16	zconstr	$$⊢\phi \to 0\in \mathrm{Constr}$$
18	3 2	rereccld	$$⊢\phi \to \frac{1}{X}\in ℝ$$
19	18	recnd	$$⊢\phi \to \frac{1}{X}\in ℂ$$
20	5	constrcn	$$⊢\phi \to \mathrm{i}\in ℂ$$
21	6 8	subcld	$$⊢\phi \to 1-\mathrm{i}X\in ℂ$$
22	20 21	pncan2d	$$⊢\phi \to \mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}=1-\mathrm{i}X$$
23	22	oveq2d	$$⊢\phi \to \left(\frac{1}{X}\right)\left(\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}\right)=\left(\frac{1}{X}\right)\left(1-\mathrm{i}X\right)$$
24	23	oveq2d	$$⊢\phi \to \mathrm{i}+\left(\frac{1}{X}\right)\left(\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}\right)=\mathrm{i}+\left(\frac{1}{X}\right)\left(1-\mathrm{i}X\right)$$
25	19 6 8	subdid	$$⊢\phi \to \left(\frac{1}{X}\right)\left(1-\mathrm{i}X\right)=\left(\frac{1}{X}\right)\cdot 1-\left(\frac{1}{X}\right)\mathrm{i}X$$
26	19	mulridd	$$⊢\phi \to \left(\frac{1}{X}\right)\cdot 1=\frac{1}{X}$$
27	3	recnd	$$⊢\phi \to X\in ℂ$$
28	6 27 8 2	div32d	$$⊢\phi \to \left(\frac{1}{X}\right)\mathrm{i}X=1\left(\frac{\mathrm{i}X}{X}\right)$$
29	8 27 2	divcld	$$⊢\phi \to \frac{\mathrm{i}X}{X}\in ℂ$$
30	29	mullidd	$$⊢\phi \to 1\left(\frac{\mathrm{i}X}{X}\right)=\frac{\mathrm{i}X}{X}$$
31	20 27 2	divcan4d	$$⊢\phi \to \frac{\mathrm{i}X}{X}=\mathrm{i}$$
32	28 30 31	3eqtrd	$$⊢\phi \to \left(\frac{1}{X}\right)\mathrm{i}X=\mathrm{i}$$
33	26 32	oveq12d	$$⊢\phi \to \left(\frac{1}{X}\right)\cdot 1-\left(\frac{1}{X}\right)\mathrm{i}X=\left(\frac{1}{X}\right)-\mathrm{i}$$
34	25 33	eqtrd	$$⊢\phi \to \left(\frac{1}{X}\right)\left(1-\mathrm{i}X\right)=\left(\frac{1}{X}\right)-\mathrm{i}$$
35	34	oveq2d	$$⊢\phi \to \mathrm{i}+\left(\frac{1}{X}\right)\left(1-\mathrm{i}X\right)=\mathrm{i}+\left(\frac{1}{X}\right)-\mathrm{i}$$
36	20 19	pncan3d	$$⊢\phi \to \mathrm{i}+\left(\frac{1}{X}\right)-\mathrm{i}=\frac{1}{X}$$
37	24 35 36	3eqtrrd	$$⊢\phi \to \frac{1}{X}=\mathrm{i}+\left(\frac{1}{X}\right)\left(\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}\right)$$
38	6	subid1d	$$⊢\phi \to 1-0=1$$
39	38 6	eqeltrd	$$⊢\phi \to 1-0\in ℂ$$
40	19 39	mulcld	$$⊢\phi \to \left(\frac{1}{X}\right)\left(1-0\right)\in ℂ$$
41	40	addlidd	$$⊢\phi \to 0+\left(\frac{1}{X}\right)\left(1-0\right)=\left(\frac{1}{X}\right)\left(1-0\right)$$
42	38	oveq2d	$$⊢\phi \to \left(\frac{1}{X}\right)\left(1-0\right)=\left(\frac{1}{X}\right)\cdot 1$$
43	41 42 26	3eqtrrd	$$⊢\phi \to \frac{1}{X}=0+\left(\frac{1}{X}\right)\left(1-0\right)$$
44	38	oveq2d	$$⊢\phi \to \overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\left(1-0\right)=\overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\cdot 1$$
45	15	constrcn	$$⊢\phi \to \mathrm{i}+1-\mathrm{i}X\in ℂ$$
46	45 20	subcld	$$⊢\phi \to \mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}\in ℂ$$
47	46	cjcld	$$⊢\phi \to \overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\in ℂ$$
48	47	mulridd	$$⊢\phi \to \overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\cdot 1=\overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}$$
49	22	fveq2d	$$⊢\phi \to \overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}=\overline{1-\mathrm{i}X}$$
50	44 48 49	3eqtrd	$$⊢\phi \to \overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\left(1-0\right)=\overline{1-\mathrm{i}X}$$
51	50	fveq2d	$$⊢\phi \to \Im \left(\overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\left(1-0\right)\right)=\Im \left(\overline{1-\mathrm{i}X}\right)$$
52	6 8	cjsubd	$$⊢\phi \to \overline{1-\mathrm{i}X}=\bar{1}-\overline{\mathrm{i}X}$$
53		1red	$$⊢\phi \to 1\in ℝ$$
54	53	cjred	$$⊢\phi \to \bar{1}=1$$
55	20 27	cjmuld	$$⊢\phi \to \overline{\mathrm{i}X}=\bar{\mathrm{i}}\bar{X}$$
56		cji	$$⊢\bar{\mathrm{i}}=-\mathrm{i}$$
57	56	a1i	$$⊢\phi \to \bar{\mathrm{i}}=-\mathrm{i}$$
58	3	cjred	$$⊢\phi \to \bar{X}=X$$
59	57 58	oveq12d	$$⊢\phi \to \bar{\mathrm{i}}\bar{X}=\left(-\mathrm{i}\right)X$$
60	20 27	mulneg1d	$$⊢\phi \to \left(-\mathrm{i}\right)X=-\mathrm{i}X$$
61	55 59 60	3eqtrd	$$⊢\phi \to \overline{\mathrm{i}X}=-\mathrm{i}X$$
62	54 61	oveq12d	$$⊢\phi \to \bar{1}-\overline{\mathrm{i}X}=1-\left(-\mathrm{i}X\right)$$
63	6 8	subnegd	$$⊢\phi \to 1-\left(-\mathrm{i}X\right)=1+\mathrm{i}X$$
64	52 62 63	3eqtrd	$$⊢\phi \to \overline{1-\mathrm{i}X}=1+\mathrm{i}X$$
65	64	fveq2d	$$⊢\phi \to \Im \left(\overline{1-\mathrm{i}X}\right)=\Im \left(1+\mathrm{i}X\right)$$
66	53 3	crimd	$$⊢\phi \to \Im \left(1+\mathrm{i}X\right)=X$$
67	51 65 66	3eqtrd	$$⊢\phi \to \Im \left(\overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\left(1-0\right)\right)=X$$
68	67 2	eqnetrd	$$⊢\phi \to \Im \left(\overline{\mathrm{i}+\left(1-\mathrm{i}X\right)-\mathrm{i}}\left(1-0\right)\right)\ne 0$$
69	5 15 17 11 18 18 19 37 43 68	constrllcl	$$⊢\phi \to \frac{1}{X}\in \mathrm{Constr}$$