Metamath Proof Explorer

Theorem constrcjcl

Description: Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025)

		Ref	Expression
	Hypothesis	constrcjcl.1	$⊢ φ \to X \in Constr$
	Assertion	constrcjcl	$⊢ φ \to \overline{X} \in Constr$

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.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	2	isconstr	$⊢ X \in Constr \leftrightarrow \exists n \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\}) (n)$
4	1 3	sylib	$⊢ φ \to \exists n \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\}) (n)$
5		nnon	$⊢ n \in ω \to n \in On$
6	5	ad2antlr	$⊢ ((φ \land n \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\}) (n)) \to n \in On$
7		simpr	$⊢ ((φ \land n \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\}) (n)) \to 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\}) (n)$
8	2 6 7	constrconj	$⊢ ((φ \land n \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\}) (n)) \to \overline{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\}) (n)$
9	8	ex	$⊢ (φ \land n \in ω) \to (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\}) (n) \to \overline{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\}) (n))$
10	9	reximdva	$⊢ φ \to (\exists n \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\}) (n) \to \exists n \in ω \overline{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\}) (n))$
11	4 10	mpd	$⊢ φ \to \exists n \in ω \overline{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\}) (n)$
12	2	isconstr	$⊢ \overline{X} \in Constr \leftrightarrow \exists n \in ω \overline{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\}) (n)$
13	11 12	sylibr	$⊢ φ \to \overline{X} \in Constr$