Theorem constraddcl

Description: Constructive numbers are closed under complex addition. Item (1) of Theorem 7.10 of Stewart p. 96. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	constraddcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
	constraddcl.2	$$⊢\phi \to Y\in \mathrm{Constr}$$
Assertion	constraddcl	$$⊢\phi \to X+Y\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constraddcl.1	$$⊢\phi \to X\in \mathrm{Constr}$$
2		constraddcl.2	$$⊢\phi \to Y\in \mathrm{Constr}$$
3		simpr	$$⊢\left(\phi \wedge X=Y\right)\to X=Y$$
4	3	oveq2d	$$⊢\left(\phi \wedge X=Y\right)\to X+X=X+Y$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
7	6	nn0constr	$$⊢\phi \to 0\in \mathrm{Constr}$$
8		2re	$$⊢2\in ℝ$$
9	8	a1i	$$⊢\phi \to 2\in ℝ$$
10	1	constrcn	$$⊢\phi \to X\in ℂ$$
11	10 10	addcld	$$⊢\phi \to X+X\in ℂ$$
12		2cnd	$$⊢\phi \to 2\in ℂ$$
13		0cnd	$$⊢\phi \to 0\in ℂ$$
14	10 13	subcld	$$⊢\phi \to X-0\in ℂ$$
15	12 14	mulcld	$$⊢\phi \to 2\left(X-0\right)\in ℂ$$
16	15	addlidd	$$⊢\phi \to 0+2\left(X-0\right)=2\left(X-0\right)$$
17	10	subid1d	$$⊢\phi \to X-0=X$$
18	17	oveq2d	$$⊢\phi \to 2\left(X-0\right)=2X$$
19	10	2timesd	$$⊢\phi \to 2X=X+X$$
20	16 18 19	3eqtrrd	$$⊢\phi \to X+X=0+2\left(X-0\right)$$
21	10 10	pncand	$$⊢\phi \to X+X-X=X$$
22	21 17	eqtr4d	$$⊢\phi \to X+X-X=X-0$$
23	22	fveq2d	$$⊢\phi \to \left|X+X-X\right|=\left|X-0\right|$$
24	7 1 1 1 7 9 11 20 23	constrlccl	$$⊢\phi \to X+X\in \mathrm{Constr}$$
25	24	adantr	$$⊢\left(\phi \wedge X=Y\right)\to X+X\in \mathrm{Constr}$$
26	4 25	eqeltrrd	$$⊢\left(\phi \wedge X=Y\right)\to X+Y\in \mathrm{Constr}$$
27	1	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in \mathrm{Constr}$$
28	2	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in \mathrm{Constr}$$
29	7	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to 0\in \mathrm{Constr}$$
30	10	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\in ℂ$$
31	2	constrcn	$$⊢\phi \to Y\in ℂ$$
32	31	adantr	$$⊢\left(\phi \wedge X\ne Y\right)\to Y\in ℂ$$
33	30 32	addcld	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y\in ℂ$$
34		simpr	$$⊢\left(\phi \wedge X\ne Y\right)\to X\ne Y$$
35	30 32	pncan2d	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y-X=Y$$
36	32	subid1d	$$⊢\left(\phi \wedge X\ne Y\right)\to Y-0=Y$$
37	35 36	eqtr4d	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y-X=Y-0$$
38	37	fveq2d	$$⊢\left(\phi \wedge X\ne Y\right)\to \left|X+Y-X\right|=\left|Y-0\right|$$
39	30 32	pncand	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y-Y=X$$
40	30	subid1d	$$⊢\left(\phi \wedge X\ne Y\right)\to X-0=X$$
41	39 40	eqtr4d	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y-Y=X-0$$
42	41	fveq2d	$$⊢\left(\phi \wedge X\ne Y\right)\to \left|X+Y-Y\right|=\left|X-0\right|$$
43	27 28 29 28 27 29 33 34 38 42	constrcccl	$$⊢\left(\phi \wedge X\ne Y\right)\to X+Y\in \mathrm{Constr}$$
44	26 43	pm2.61dane	$$⊢\phi \to X+Y\in \mathrm{Constr}$$