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	⊢ ( 𝜑 → 𝑋 ∈ Constr )
	constraddcl.2	⊢ ( 𝜑 → 𝑌 ∈ Constr )
Assertion	constraddcl	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constraddcl.1	⊢ ( 𝜑 → 𝑋 ∈ Constr )
2		constraddcl.2	⊢ ( 𝜑 → 𝑌 ∈ Constr )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
4	3	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 + 𝑋 ) = ( 𝑋 + 𝑌 ) )
5		0nn0	⊢ 0 ∈ ℕ0
6	5	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
7	6	nn0constr	⊢ ( 𝜑 → 0 ∈ Constr )
8		2re	⊢ 2 ∈ ℝ
9	8	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
10	1	constrcn	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
11	10 10	addcld	⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) ∈ ℂ )
12		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
13		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
14	10 13	subcld	⊢ ( 𝜑 → ( 𝑋 − 0 ) ∈ ℂ )
15	12 14	mulcld	⊢ ( 𝜑 → ( 2 · ( 𝑋 − 0 ) ) ∈ ℂ )
16	15	addlidd	⊢ ( 𝜑 → ( 0 + ( 2 · ( 𝑋 − 0 ) ) ) = ( 2 · ( 𝑋 − 0 ) ) )
17	10	subid1d	⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 )
18	17	oveq2d	⊢ ( 𝜑 → ( 2 · ( 𝑋 − 0 ) ) = ( 2 · 𝑋 ) )
19	10	2timesd	⊢ ( 𝜑 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )
20	16 18 19	3eqtrrd	⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) = ( 0 + ( 2 · ( 𝑋 − 0 ) ) ) )
21	10 10	pncand	⊢ ( 𝜑 → ( ( 𝑋 + 𝑋 ) − 𝑋 ) = 𝑋 )
22	21 17	eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 + 𝑋 ) − 𝑋 ) = ( 𝑋 − 0 ) )
23	22	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 + 𝑋 ) − 𝑋 ) ) = ( abs ‘ ( 𝑋 − 0 ) ) )
24	7 1 1 1 7 9 11 20 23	constrlccl	⊢ ( 𝜑 → ( 𝑋 + 𝑋 ) ∈ Constr )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 + 𝑋 ) ∈ Constr )
26	4 25	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 + 𝑌 ) ∈ Constr )
27	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ Constr )
28	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ Constr )
29	7	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 0 ∈ Constr )
30	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ ℂ )
31	2	constrcn	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ℂ )
33	30 32	addcld	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 + 𝑌 ) ∈ ℂ )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
35	30 32	pncan2d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 + 𝑌 ) − 𝑋 ) = 𝑌 )
36	32	subid1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 − 0 ) = 𝑌 )
37	35 36	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 + 𝑌 ) − 𝑋 ) = ( 𝑌 − 0 ) )
38	37	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( abs ‘ ( ( 𝑋 + 𝑌 ) − 𝑋 ) ) = ( abs ‘ ( 𝑌 − 0 ) ) )
39	30 32	pncand	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 + 𝑌 ) − 𝑌 ) = 𝑋 )
40	30	subid1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 − 0 ) = 𝑋 )
41	39 40	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 + 𝑌 ) − 𝑌 ) = ( 𝑋 − 0 ) )
42	41	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( abs ‘ ( ( 𝑋 + 𝑌 ) − 𝑌 ) ) = ( abs ‘ ( 𝑋 − 0 ) ) )
43	27 28 29 28 27 29 33 34 38 42	constrcccl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 + 𝑌 ) ∈ Constr )
44	26 43	pm2.61dane	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ Constr )