constrext2chn

Description: If a constructible number generates some subfield L of CC , then the degree of the extension of L over QQ is a power of two. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	constrext2chn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	constrext2chn.l	$⊢ L = ℂ_{fld} ↾_{𝑠} S$
	constrext2chn.s	$⊢ S = ℂ_{fld} fldGen (ℚ \cup \{A\})$
	constrext2chn.a	$⊢ φ \to A \in Constr$
Assertion	constrext2chn	$⊢ φ \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		constrext2chn.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		constrext2chn.l	$⊢ L = ℂ_{fld} ↾_{𝑠} S$
3		constrext2chn.s	$⊢ S = ℂ_{fld} fldGen (ℚ \cup \{A\})$
4		constrext2chn.a	$⊢ φ \to A \in Constr$
5		oveq1	$⊢ o = t \to o (j - i) = t (j - i)$
6	5	oveq2d	$⊢ o = t \to i + o (j - i) = i + t (j - i)$
7	6	eqeq2d	$⊢ o = t \to (y = i + o (j - i) \leftrightarrow y = i + t (j - i))$
8	7	3anbi1d	$⊢ o = t \to ((y = i + o (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \leftrightarrow (y = i + t (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0))$
9		oveq1	$⊢ p = r \to p (l - k) = r (l - k)$
10	9	oveq2d	$⊢ p = r \to k + p (l - k) = k + r (l - k)$
11	10	eqeq2d	$⊢ p = r \to (y = k + p (l - k) \leftrightarrow y = k + r (l - k))$
12	11	3anbi2d	$⊢ p = r \to ((y = i + t (j - i) \land y = k + p (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \leftrightarrow (y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0))$
13	8 12	cbvrex2vw	$⊢ \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) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0)$
14	13	2rexbii	$⊢ \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) \leftrightarrow \exists k \in z \exists l \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0)$
15		id	$⊢ k = c \to k = c$
16		oveq2	$⊢ k = c \to l - k = l - c$
17	16	oveq2d	$⊢ k = c \to r (l - k) = r (l - c)$
18	15 17	oveq12d	$⊢ k = c \to k + r (l - k) = c + r (l - c)$
19	18	eqeq2d	$⊢ k = c \to (y = k + r (l - k) \leftrightarrow y = c + r (l - c))$
20	16	oveq2d	$⊢ k = c \to \overline{j - i} (l - k) = \overline{j - i} (l - c)$
21	20	fveq2d	$⊢ k = c \to ℑ (\overline{j - i} (l - k)) = ℑ (\overline{j - i} (l - c))$
22	21	neeq1d	$⊢ k = c \to (ℑ (\overline{j - i} (l - k)) \neq 0 \leftrightarrow ℑ (\overline{j - i} (l - c)) \neq 0)$
23	19 22	3anbi23d	$⊢ k = c \to ((y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \leftrightarrow (y = i + t (j - i) \land y = c + r (l - c) \land ℑ (\overline{j - i} (l - c)) \neq 0))$
24	23	2rexbidv	$⊢ k = c \to (\exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (l - c) \land ℑ (\overline{j - i} (l - c)) \neq 0))$
25		oveq1	$⊢ l = d \to l - c = d - c$
26	25	oveq2d	$⊢ l = d \to r (l - c) = r (d - c)$
27	26	oveq2d	$⊢ l = d \to c + r (l - c) = c + r (d - c)$
28	27	eqeq2d	$⊢ l = d \to (y = c + r (l - c) \leftrightarrow y = c + r (d - c))$
29	25	oveq2d	$⊢ l = d \to \overline{j - i} (l - c) = \overline{j - i} (d - c)$
30	29	fveq2d	$⊢ l = d \to ℑ (\overline{j - i} (l - c)) = ℑ (\overline{j - i} (d - c))$
31	30	neeq1d	$⊢ l = d \to (ℑ (\overline{j - i} (l - c)) \neq 0 \leftrightarrow ℑ (\overline{j - i} (d - c)) \neq 0)$
32	28 31	3anbi23d	$⊢ l = d \to ((y = i + t (j - i) \land y = c + r (l - c) \land ℑ (\overline{j - i} (l - c)) \neq 0) \leftrightarrow (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0))$
33	32	2rexbidv	$⊢ l = d \to (\exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (l - c) \land ℑ (\overline{j - i} (l - c)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0))$
34	24 33	cbvrex2vw	$⊢ \exists k \in z \exists l \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = k + r (l - k) \land ℑ (\overline{j - i} (l - k)) \neq 0) \leftrightarrow \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0)$
35	14 34	bitri	$⊢ \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) \leftrightarrow \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0)$
36	35	2rexbii	$⊢ \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) \leftrightarrow \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0)$
37		oveq2	$⊢ q = f \to m - q = m - f$
38	37	fveq2d	$⊢ q = f \to \|m - q\| = \|m - f\|$
39	38	eqeq2d	$⊢ q = f \to (\|y - k\| = \|m - q\| \leftrightarrow \|y - k\| = \|m - f\|)$
40	39	anbi2d	$⊢ q = f \to ((y = i + o (j - i) \land \|y - k\| = \|m - q\|) \leftrightarrow (y = i + o (j - i) \land \|y - k\| = \|m - f\|))$
41	7	anbi1d	$⊢ o = t \to ((y = i + o (j - i) \land \|y - k\| = \|m - f\|) \leftrightarrow (y = i + t (j - i) \land \|y - k\| = \|m - f\|))$
42	40 41	cbvrex2vw	$⊢ \exists q \in z \exists o \in ℝ (y = i + o (j - i) \land \|y - k\| = \|m - q\|) \leftrightarrow \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - k\| = \|m - f\|)$
43	42	2rexbii	$⊢ \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\|) \leftrightarrow \exists k \in z \exists m \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - k\| = \|m - f\|)$
44		oveq2	$⊢ k = c \to y - k = y - c$
45	44	fveq2d	$⊢ k = c \to \|y - k\| = \|y - c\|$
46	45	eqeq1d	$⊢ k = c \to (\|y - k\| = \|m - f\| \leftrightarrow \|y - c\| = \|m - f\|)$
47	46	anbi2d	$⊢ k = c \to ((y = i + t (j - i) \land \|y - k\| = \|m - f\|) \leftrightarrow (y = i + t (j - i) \land \|y - c\| = \|m - f\|))$
48	47	2rexbidv	$⊢ k = c \to (\exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - k\| = \|m - f\|) \leftrightarrow \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|m - f\|))$
49		oveq1	$⊢ m = e \to m - f = e - f$
50	49	fveq2d	$⊢ m = e \to \|m - f\| = \|e - f\|$
51	50	eqeq2d	$⊢ m = e \to (\|y - c\| = \|m - f\| \leftrightarrow \|y - c\| = \|e - f\|)$
52	51	anbi2d	$⊢ m = e \to ((y = i + t (j - i) \land \|y - c\| = \|m - f\|) \leftrightarrow (y = i + t (j - i) \land \|y - c\| = \|e - f\|))$
53	52	2rexbidv	$⊢ m = e \to (\exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|m - f\|) \leftrightarrow \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|))$
54	48 53	cbvrex2vw	$⊢ \exists k \in z \exists m \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - k\| = \|m - f\|) \leftrightarrow \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|)$
55	43 54	bitri	$⊢ \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\|) \leftrightarrow \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|)$
56	55	2rexbii	$⊢ \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\|) \leftrightarrow \exists i \in z \exists j \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|)$
57		oveq1	$⊢ m = e \to m - q = e - q$
58	57	fveq2d	$⊢ m = e \to \|m - q\| = \|e - q\|$
59	58	eqeq2d	$⊢ m = e \to (\|y - l\| = \|m - q\| \leftrightarrow \|y - l\| = \|e - q\|)$
60	59	3anbi3d	$⊢ m = e \to ((i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|) \leftrightarrow (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - q\|))$
61		oveq2	$⊢ q = f \to e - q = e - f$
62	61	fveq2d	$⊢ q = f \to \|e - q\| = \|e - f\|$
63	62	eqeq2d	$⊢ q = f \to (\|y - l\| = \|e - q\| \leftrightarrow \|y - l\| = \|e - f\|)$
64	63	3anbi3d	$⊢ q = f \to ((i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - q\|) \leftrightarrow (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|))$
65	60 64	cbvrex2vw	$⊢ \exists m \in z \exists q \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|m - q\|) \leftrightarrow \exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|)$
66	65	2rexbii	$⊢ \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\|) \leftrightarrow \exists k \in z \exists l \in z \exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|)$
67		oveq2	$⊢ k = c \to j - k = j - c$
68	67	fveq2d	$⊢ k = c \to \|j - k\| = \|j - c\|$
69	68	eqeq2d	$⊢ k = c \to (\|y - i\| = \|j - k\| \leftrightarrow \|y - i\| = \|j - c\|)$
70	69	3anbi2d	$⊢ k = c \to ((i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|) \leftrightarrow (i \neq l \land \|y - i\| = \|j - c\| \land \|y - l\| = \|e - f\|))$
71	70	2rexbidv	$⊢ k = c \to (\exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|) \leftrightarrow \exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - c\| \land \|y - l\| = \|e - f\|))$
72		neeq2	$⊢ l = d \to (i \neq l \leftrightarrow i \neq d)$
73		oveq2	$⊢ l = d \to y - l = y - d$
74	73	fveq2d	$⊢ l = d \to \|y - l\| = \|y - d\|$
75	74	eqeq1d	$⊢ l = d \to (\|y - l\| = \|e - f\| \leftrightarrow \|y - d\| = \|e - f\|)$
76	72 75	3anbi13d	$⊢ l = d \to ((i \neq l \land \|y - i\| = \|j - c\| \land \|y - l\| = \|e - f\|) \leftrightarrow (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
77	76	2rexbidv	$⊢ l = d \to (\exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - c\| \land \|y - l\| = \|e - f\|) \leftrightarrow \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
78	71 77	cbvrex2vw	$⊢ \exists k \in z \exists l \in z \exists e \in z \exists f \in z (i \neq l \land \|y - i\| = \|j - k\| \land \|y - l\| = \|e - f\|) \leftrightarrow \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|)$
79	66 78	bitri	$⊢ \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\|) \leftrightarrow \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|)$
80	79	2rexbii	$⊢ \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\|) \leftrightarrow \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|)$
81	36 56 80	3orbi123i	$⊢ (\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\|)) \leftrightarrow (\exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \lor \exists i \in z \exists j \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|) \lor \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
82		id	$⊢ i = a \to i = a$
83		oveq2	$⊢ i = a \to j - i = j - a$
84	83	oveq2d	$⊢ i = a \to t (j - i) = t (j - a)$
85	82 84	oveq12d	$⊢ i = a \to i + t (j - i) = a + t (j - a)$
86	85	eqeq2d	$⊢ i = a \to (y = i + t (j - i) \leftrightarrow y = a + t (j - a))$
87	83	fveq2d	$⊢ i = a \to \overline{j - i} = \overline{j - a}$
88	87	oveq1d	$⊢ i = a \to \overline{j - i} (d - c) = \overline{j - a} (d - c)$
89	88	fveq2d	$⊢ i = a \to ℑ (\overline{j - i} (d - c)) = ℑ (\overline{j - a} (d - c))$
90	89	neeq1d	$⊢ i = a \to (ℑ (\overline{j - i} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{j - a} (d - c)) \neq 0)$
91	86 90	3anbi13d	$⊢ i = a \to ((y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \leftrightarrow (y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0))$
92	91	2rexbidv	$⊢ i = a \to (\exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0))$
93	92	2rexbidv	$⊢ i = a \to (\exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \leftrightarrow \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0))$
94		oveq1	$⊢ j = b \to j - a = b - a$
95	94	oveq2d	$⊢ j = b \to t (j - a) = t (b - a)$
96	95	oveq2d	$⊢ j = b \to a + t (j - a) = a + t (b - a)$
97	96	eqeq2d	$⊢ j = b \to (y = a + t (j - a) \leftrightarrow y = a + t (b - a))$
98	94	fveq2d	$⊢ j = b \to \overline{j - a} = \overline{b - a}$
99	98	oveq1d	$⊢ j = b \to \overline{j - a} (d - c) = \overline{b - a} (d - c)$
100	99	fveq2d	$⊢ j = b \to ℑ (\overline{j - a} (d - c)) = ℑ (\overline{b - a} (d - c))$
101	100	neeq1d	$⊢ j = b \to (ℑ (\overline{j - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - a} (d - c)) \neq 0)$
102	97 101	3anbi13d	$⊢ j = b \to ((y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0) \leftrightarrow (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
103	102	2rexbidv	$⊢ j = b \to (\exists t \in ℝ \exists r \in ℝ (y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
104	103	2rexbidv	$⊢ j = b \to (\exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (j - a) \land y = c + r (d - c) \land ℑ (\overline{j - a} (d - c)) \neq 0) \leftrightarrow \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
105	93 104	cbvrex2vw	$⊢ \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)$
106	86	anbi1d	$⊢ i = a \to ((y = i + t (j - i) \land \|y - c\| = \|e - f\|) \leftrightarrow (y = a + t (j - a) \land \|y - c\| = \|e - f\|))$
107	106	2rexbidv	$⊢ i = a \to (\exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists f \in z \exists t \in ℝ (y = a + t (j - a) \land \|y - c\| = \|e - f\|))$
108	107	2rexbidv	$⊢ i = a \to (\exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (j - a) \land \|y - c\| = \|e - f\|))$
109	97	anbi1d	$⊢ j = b \to ((y = a + t (j - a) \land \|y - c\| = \|e - f\|) \leftrightarrow (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
110	109	2rexbidv	$⊢ j = b \to (\exists f \in z \exists t \in ℝ (y = a + t (j - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
111	110	2rexbidv	$⊢ j = b \to (\exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (j - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
112	108 111	cbvrex2vw	$⊢ \exists i \in z \exists j \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)$
113		neeq1	$⊢ i = a \to (i \neq d \leftrightarrow a \neq d)$
114		oveq2	$⊢ i = a \to y - i = y - a$
115	114	fveq2d	$⊢ i = a \to \|y - i\| = \|y - a\|$
116	115	eqeq1d	$⊢ i = a \to (\|y - i\| = \|j - c\| \leftrightarrow \|y - a\| = \|j - c\|)$
117	113 116	3anbi12d	$⊢ i = a \to ((i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow (a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
118	117	2rexbidv	$⊢ i = a \to (\exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
119	118	2rexbidv	$⊢ i = a \to (\exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|))$
120		oveq1	$⊢ j = b \to j - c = b - c$
121	120	fveq2d	$⊢ j = b \to \|j - c\| = \|b - c\|$
122	121	eqeq2d	$⊢ j = b \to (\|y - a\| = \|j - c\| \leftrightarrow \|y - a\| = \|b - c\|)$
123	122	3anbi2d	$⊢ j = b \to ((a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
124	123	2rexbidv	$⊢ j = b \to (\exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
125	124	2rexbidv	$⊢ j = b \to (\exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
126	119 125	cbvrex2vw	$⊢ \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)$
127	105 112 126	3orbi123i	$⊢ (\exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = i + t (j - i) \land y = c + r (d - c) \land ℑ (\overline{j - i} (d - c)) \neq 0) \lor \exists i \in z \exists j \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = i + t (j - i) \land \|y - c\| = \|e - f\|) \lor \exists i \in z \exists j \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (i \neq d \land \|y - i\| = \|j - c\| \land \|y - d\| = \|e - f\|)) \leftrightarrow (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
128	81 127	bitri	$⊢ (\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\|)) \leftrightarrow (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
129	128	rabbii	$⊢ \{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\|))\} = \{y \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))\}$
130		eqeq1	$⊢ y = x \to (y = a + t (b - a) \leftrightarrow x = a + t (b - a))$
131		eqeq1	$⊢ y = x \to (y = c + r (d - c) \leftrightarrow x = c + r (d - c))$
132		biidd	$⊢ y = x \to (ℑ (\overline{b - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - a} (d - c)) \neq 0)$
133	130 131 132	3anbi123d	$⊢ y = x \to ((y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
134	133	2rexbidv	$⊢ y = x \to (\exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \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))$
135	134	2rexbidv	$⊢ y = x \to (\exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists c \in z \exists d \in z \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))$
136	135	2rexbidv	$⊢ y = x \to (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists d \in z \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))$
137		oveq1	$⊢ y = x \to y - c = x - c$
138	137	fveq2d	$⊢ y = x \to \|y - c\| = \|x - c\|$
139	138	eqeq1d	$⊢ y = x \to (\|y - c\| = \|e - f\| \leftrightarrow \|x - c\| = \|e - f\|)$
140	130 139	anbi12d	$⊢ y = x \to ((y = a + t (b - a) \land \|y - c\| = \|e - f\|) \leftrightarrow (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
141	140	2rexbidv	$⊢ y = x \to (\exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
142	141	2rexbidv	$⊢ y = x \to (\exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
143	142	2rexbidv	$⊢ y = x \to (\exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
144		biidd	$⊢ y = x \to (a \neq d \leftrightarrow a \neq d)$
145		oveq1	$⊢ y = x \to y - a = x - a$
146	145	fveq2d	$⊢ y = x \to \|y - a\| = \|x - a\|$
147	146	eqeq1d	$⊢ y = x \to (\|y - a\| = \|b - c\| \leftrightarrow \|x - a\| = \|b - c\|)$
148		oveq1	$⊢ y = x \to y - d = x - d$
149	148	fveq2d	$⊢ y = x \to \|y - d\| = \|x - d\|$
150	149	eqeq1d	$⊢ y = x \to (\|y - d\| = \|e - f\| \leftrightarrow \|x - d\| = \|e - f\|)$
151	144 147 150	3anbi123d	$⊢ y = x \to ((a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
152	151	2rexbidv	$⊢ y = x \to (\exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
153	152	2rexbidv	$⊢ y = x \to (\exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
154	153	2rexbidv	$⊢ y = x \to (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \leftrightarrow \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
155	136 143 154	3orbi123d	$⊢ y = x \to ((\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \leftrightarrow (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)))$
156	155	cbvrabv	$⊢ \{y \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))\} = \{x \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}$
157	129 156	eqtri	$⊢ \{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\|))\} = \{x \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}$
158	157	mpteq2i	$⊢ (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\|))\}) = (z \in V ⟼ \{x \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\})$
159		elequ2	$⊢ z = s \to (a \in z \leftrightarrow a \in s)$
160		elequ2	$⊢ z = s \to (b \in z \leftrightarrow b \in s)$
161		elequ2	$⊢ z = s \to (c \in z \leftrightarrow c \in s)$
162		rexeq	$⊢ z = s \to (\exists d \in z \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) \leftrightarrow \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))$
163	161 162	anbi12d	$⊢ z = s \to ((c \in z \land \exists d \in z \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)) \leftrightarrow (c \in s \land \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)))$
164	163	rexbidv2	$⊢ z = s \to (\exists c \in z \exists d \in z \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) \leftrightarrow \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))$
165	160 164	anbi12d	$⊢ z = s \to ((b \in z \land \exists c \in z \exists d \in z \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)) \leftrightarrow (b \in s \land \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)))$
166	165	rexbidv2	$⊢ z = s \to (\exists b \in z \exists c \in z \exists d \in z \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) \leftrightarrow \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))$
167	159 166	anbi12d	$⊢ z = s \to ((a \in z \land \exists b \in z \exists c \in z \exists d \in z \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)) \leftrightarrow (a \in s \land \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)))$
168	167	rexbidv2	$⊢ z = s \to (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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) \leftrightarrow \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))$
169		elequ2	$⊢ z = s \to (e \in z \leftrightarrow e \in s)$
170		rexeq	$⊢ z = s \to (\exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
171	169 170	anbi12d	$⊢ z = s \to ((e \in z \land \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \leftrightarrow (e \in s \land \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)))$
172	171	rexbidv2	$⊢ z = s \to (\exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|))$
173	161 172	anbi12d	$⊢ z = s \to ((c \in z \land \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \leftrightarrow (c \in s \land \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)))$
174	173	rexbidv2	$⊢ z = s \to (\exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \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\|))$
175	160 174	anbi12d	$⊢ z = s \to ((b \in z \land \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \leftrightarrow (b \in s \land \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\|)))$
176	175	rexbidv2	$⊢ z = s \to (\exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \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\|))$
177	159 176	anbi12d	$⊢ z = s \to ((a \in z \land \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \leftrightarrow (a \in s \land \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\|)))$
178	177	rexbidv2	$⊢ z = s \to (\exists a \in z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \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\|))$
179		elequ2	$⊢ z = s \to (d \in z \leftrightarrow d \in s)$
180		rexeq	$⊢ z = s \to (\exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
181	169 180	anbi12d	$⊢ z = s \to ((e \in z \land \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (e \in s \land \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)))$
182	181	rexbidv2	$⊢ z = s \to (\exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))$
183	179 182	anbi12d	$⊢ z = s \to ((d \in z \land \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (d \in s \land \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)))$
184	183	rexbidv2	$⊢ z = s \to (\exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \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\|))$
185	161 184	anbi12d	$⊢ z = s \to ((c \in z \land \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (c \in s \land \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\|)))$
186	185	rexbidv2	$⊢ z = s \to (\exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \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\|))$
187	160 186	anbi12d	$⊢ z = s \to ((b \in z \land \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (b \in s \land \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\|)))$
188	187	rexbidv2	$⊢ z = s \to (\exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \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\|))$
189	159 188	anbi12d	$⊢ z = s \to ((a \in z \land \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (a \in s \land \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\|)))$
190	189	rexbidv2	$⊢ z = s \to (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow \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\|))$
191	168 178 190	3orbi123d	$⊢ z = s \to ((\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \leftrightarrow (\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\|)))$
192	191	rabbidv	$⊢ z = s \to \{x \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\} = \{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\|))\}$
193	192	cbvmptv	$⊢ (z \in V ⟼ \{x \in ℂ \| (\exists a \in z \exists b \in z \exists c \in z \exists d \in z \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 z \exists b \in z \exists c \in z \exists e \in z \exists f \in z \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in z \exists b \in z \exists c \in z \exists d \in z \exists e \in z \exists f \in z (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}) = (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\|))\})$
194	158 193	eqtri	$⊢ (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\|))\}) = (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\|))\})$
195		rdgeq1	$⊢ (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\|))\}) = (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\|))\}) \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\}) = 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\})$
196	194 195	ax-mp	$⊢ 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\})$
197		eqid	$⊢ ℂ_{fld} ↾_{𝑠} e = ℂ_{fld} ↾_{𝑠} e$
198		eqid	$⊢ ℂ_{fld} ↾_{𝑠} f = ℂ_{fld} ↾_{𝑠} f$
199		oveq2	$⊢ h = e \to ℂ_{fld} ↾_{𝑠} h = ℂ_{fld} ↾_{𝑠} e$
200	199	adantl	$⊢ (g = f \land h = e) \to ℂ_{fld} ↾_{𝑠} h = ℂ_{fld} ↾_{𝑠} e$
201		oveq2	$⊢ g = f \to ℂ_{fld} ↾_{𝑠} g = ℂ_{fld} ↾_{𝑠} f$
202	201	adantr	$⊢ (g = f \land h = e) \to ℂ_{fld} ↾_{𝑠} g = ℂ_{fld} ↾_{𝑠} f$
203	200 202	breq12d	$⊢ (g = f \land h = e) \to ((ℂ_{fld} ↾_{𝑠} h) /_{FldExt} (ℂ_{fld} ↾_{𝑠} g) \leftrightarrow (ℂ_{fld} ↾_{𝑠} e) /_{FldExt} (ℂ_{fld} ↾_{𝑠} f))$
204	200 202	oveq12d	$⊢ (g = f \land h = e) \to (ℂ_{fld} ↾_{𝑠} h) [. : .] (ℂ_{fld} ↾_{𝑠} g) = (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f)$
205	204	eqeq1d	$⊢ (g = f \land h = e) \to ((ℂ_{fld} ↾_{𝑠} h) [. : .] (ℂ_{fld} ↾_{𝑠} g) = 2 \leftrightarrow (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f) = 2)$
206	203 205	anbi12d	$⊢ (g = f \land h = e) \to (((ℂ_{fld} ↾_{𝑠} h) /_{FldExt} (ℂ_{fld} ↾_{𝑠} g) \land (ℂ_{fld} ↾_{𝑠} h) [. : .] (ℂ_{fld} ↾_{𝑠} g) = 2) \leftrightarrow ((ℂ_{fld} ↾_{𝑠} e) /_{FldExt} (ℂ_{fld} ↾_{𝑠} f) \land (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f) = 2))$
207	206	cbvopabv	$⊢ \{⟨g, h⟩ \| ((ℂ_{fld} ↾_{𝑠} h) /_{FldExt} (ℂ_{fld} ↾_{𝑠} g) \land (ℂ_{fld} ↾_{𝑠} h) [. : .] (ℂ_{fld} ↾_{𝑠} g) = 2)\} = \{⟨f, e⟩ \| ((ℂ_{fld} ↾_{𝑠} e) /_{FldExt} (ℂ_{fld} ↾_{𝑠} f) \land (ℂ_{fld} ↾_{𝑠} e) [. : .] (ℂ_{fld} ↾_{𝑠} f) = 2)\}$
208		peano1	$⊢ \emptyset \in ω$
209	208	a1i	$⊢ φ \to \emptyset \in ω$
210	3	oveq2i	$⊢ ℂ_{fld} ↾_{𝑠} S = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
211	2 210	eqtri	$⊢ L = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
212	196 197 198 207 209 1 211 4	constrext2chnlem	$⊢ φ \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$

Metamath Proof Explorer

Theorem constrext2chn

Proof