constrsscn

Description: Closure of the constructible points in the complex numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrsscn.1	$⊢ φ \to N \in On$
Assertion	constrsscn	$⊢ φ \to C (N) \subseteq ℂ$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrsscn.1	$⊢ φ \to N \in On$
3		fveq2	$⊢ m = \emptyset \to C (m) = C (\emptyset)$
4	3	sseq1d	$⊢ m = \emptyset \to (C (m) \subseteq ℂ \leftrightarrow C (\emptyset) \subseteq ℂ)$
5		fveq2	$⊢ m = n \to C (m) = C (n)$
6	5	sseq1d	$⊢ m = n \to (C (m) \subseteq ℂ \leftrightarrow C (n) \subseteq ℂ)$
7		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
8	7	sseq1d	$⊢ m = suc n \to (C (m) \subseteq ℂ \leftrightarrow C (suc n) \subseteq ℂ)$
9		fveq2	$⊢ m = N \to C (m) = C (N)$
10	9	sseq1d	$⊢ m = N \to (C (m) \subseteq ℂ \leftrightarrow C (N) \subseteq ℂ)$
11	1	constr0	$⊢ C (\emptyset) = \{0, 1\}$
12		0cn	$⊢ 0 \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		prssi	$⊢ (0 \in ℂ \land 1 \in ℂ) \to \{0, 1\} \subseteq ℂ$
15	12 13 14	mp2an	$⊢ \{0, 1\} \subseteq ℂ$
16	11 15	eqsstri	$⊢ C (\emptyset) \subseteq ℂ$
17		simpl	$⊢ (n \in On \land C (n) \subseteq ℂ) \to n \in On$
18		eqid	$⊢ C (n) = C (n)$
19	1 17 18	constrsuc	$⊢ (n \in On \land C (n) \subseteq ℂ) \to (x \in C (suc n) \leftrightarrow (x \in ℂ \land (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))))$
20	19	biimpa	$⊢ ((n \in On \land C (n) \subseteq ℂ) \land x \in C (suc n)) \to (x \in ℂ \land (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)))$
21	20	simpld	$⊢ ((n \in On \land C (n) \subseteq ℂ) \land x \in C (suc n)) \to x \in ℂ$
22	21	ex	$⊢ (n \in On \land C (n) \subseteq ℂ) \to (x \in C (suc n) \to x \in ℂ)$
23	22	ssrdv	$⊢ (n \in On \land C (n) \subseteq ℂ) \to C (suc n) \subseteq ℂ$
24	23	ex	$⊢ n \in On \to (C (n) \subseteq ℂ \to C (suc n) \subseteq ℂ)$
25		vex	$⊢ m \in V$
26	25	a1i	$⊢ (Lim m \land \forall n \in m C (n) \subseteq ℂ) \to m \in V$
27		simpl	$⊢ (Lim m \land \forall n \in m C (n) \subseteq ℂ) \to Lim m$
28	1 26 27	constrlim	$⊢ (Lim m \land \forall n \in m C (n) \subseteq ℂ) \to C (m) = ⋃_{o \in m} C (o)$
29		fveq2	$⊢ n = o \to C (n) = C (o)$
30	29	sseq1d	$⊢ n = o \to (C (n) \subseteq ℂ \leftrightarrow C (o) \subseteq ℂ)$
31		simplr	$⊢ ((Lim m \land \forall n \in m C (n) \subseteq ℂ) \land o \in m) \to \forall n \in m C (n) \subseteq ℂ$
32		simpr	$⊢ ((Lim m \land \forall n \in m C (n) \subseteq ℂ) \land o \in m) \to o \in m$
33	30 31 32	rspcdva	$⊢ ((Lim m \land \forall n \in m C (n) \subseteq ℂ) \land o \in m) \to C (o) \subseteq ℂ$
34	33	iunssd	$⊢ (Lim m \land \forall n \in m C (n) \subseteq ℂ) \to ⋃_{o \in m} C (o) \subseteq ℂ$
35	28 34	eqsstrd	$⊢ (Lim m \land \forall n \in m C (n) \subseteq ℂ) \to C (m) \subseteq ℂ$
36	35	ex	$⊢ Lim m \to (\forall n \in m C (n) \subseteq ℂ \to C (m) \subseteq ℂ)$
37	4 6 8 10 16 24 36	tfinds	$⊢ N \in On \to C (N) \subseteq ℂ$
38	2 37	syl	$⊢ φ \to C (N) \subseteq ℂ$

Metamath Proof Explorer

Theorem constrsscn

Proof