Metamath Proof Explorer

Theorem constrcn

Description: Constructible numbers are complex numbers. (Contributed by Thierry Arnoux, 2-Nov-2025)

		Ref	Expression
	Hypothesis	constrcn.1	$⊢ φ \to X \in Constr$
	Assertion	constrcn	$⊢ φ \to X \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		constrcn.1	$⊢ φ \to X \in Constr$
2		constrcbvlem	$⊢ rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) = 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\})$
3		nnon	$⊢ u \in ω \to u \in On$
4	3	adantl	$⊢ (φ \land u \in ω) \to u \in On$
5	2 4	constrsscn	$⊢ (φ \land u \in ω) \to rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u) \subseteq ℂ$
6	5	sselda	$⊢ ((φ \land u \in ω) \land X \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)) \to X \in ℂ$
7	2	isconstr	$⊢ X \in Constr \leftrightarrow \exists u \in ω X \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
8	1 7	sylib	$⊢ φ \to \exists u \in ω X \in rec ((z \in V ⟼ \{y \in ℂ \| (\exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists o \in ℝ \exists p \in ℝ (y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \lor \exists i \in z \exists j \in z \exists k \in z \exists m \in z \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \lor \exists i \in z \exists j \in z \exists k \in z \exists l \in z \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|))\}), \{0, 1\}) (u)$
9	6 8	r19.29a	$⊢ φ \to X \in ℂ$