constrcbvlem

Description: Technical lemma for eliminating the hypothesis of constr0 and co. (Contributed by Thierry Arnoux, 2-Nov-2025)

		Ref	Expression
	Assertion	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\})$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ o = t \to o (j - i) = t (j - i)$
2	1	oveq2d	$⊢ o = t \to i + o (j - i) = i + t (j - i)$
3	2	eqeq2d	$⊢ o = t \to (y = i + o (j - i) \leftrightarrow y = i + t (j - i))$
4	3	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))$
5		oveq1	$⊢ p = r \to p (l - k) = r (l - k)$
6	5	oveq2d	$⊢ p = r \to k + p (l - k) = k + r (l - k)$
7	6	eqeq2d	$⊢ p = r \to (y = k + p (l - k) \leftrightarrow y = k + r (l - k))$
8	7	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))$
9	4 8	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)$
10	9	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)$
11		id	$⊢ k = c \to k = c$
12		oveq2	$⊢ k = c \to l - k = l - c$
13	12	oveq2d	$⊢ k = c \to r (l - k) = r (l - c)$
14	11 13	oveq12d	$⊢ k = c \to k + r (l - k) = c + r (l - c)$
15	14	eqeq2d	$⊢ k = c \to (y = k + r (l - k) \leftrightarrow y = c + r (l - c))$
16	12	oveq2d	$⊢ k = c \to \overline{j - i} (l - k) = \overline{j - i} (l - c)$
17	16	fveq2d	$⊢ k = c \to ℑ (\overline{j - i} (l - k)) = ℑ (\overline{j - i} (l - c))$
18	17	neeq1d	$⊢ k = c \to (ℑ (\overline{j - i} (l - k)) \neq 0 \leftrightarrow ℑ (\overline{j - i} (l - c)) \neq 0)$
19	15 18	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))$
20	19	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))$
21		oveq1	$⊢ l = d \to l - c = d - c$
22	21	oveq2d	$⊢ l = d \to r (l - c) = r (d - c)$
23	22	oveq2d	$⊢ l = d \to c + r (l - c) = c + r (d - c)$
24	23	eqeq2d	$⊢ l = d \to (y = c + r (l - c) \leftrightarrow y = c + r (d - c))$
25	21	oveq2d	$⊢ l = d \to \overline{j - i} (l - c) = \overline{j - i} (d - c)$
26	25	fveq2d	$⊢ l = d \to ℑ (\overline{j - i} (l - c)) = ℑ (\overline{j - i} (d - c))$
27	26	neeq1d	$⊢ l = d \to (ℑ (\overline{j - i} (l - c)) \neq 0 \leftrightarrow ℑ (\overline{j - i} (d - c)) \neq 0)$
28	24 27	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))$
29	28	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))$
30	20 29	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)$
31	10 30	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)$
32	31	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)$
33		oveq2	$⊢ q = f \to m - q = m - f$
34	33	fveq2d	$⊢ q = f \to \|m - q\| = \|m - f\|$
35	34	eqeq2d	$⊢ q = f \to (\|y - k\| = \|m - q\| \leftrightarrow \|y - k\| = \|m - f\|)$
36	35	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\|))$
37	3	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\|))$
38	36 37	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\|)$
39	38	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\|)$
40		oveq2	$⊢ k = c \to y - k = y - c$
41	40	fveq2d	$⊢ k = c \to \|y - k\| = \|y - c\|$
42	41	eqeq1d	$⊢ k = c \to (\|y - k\| = \|m - f\| \leftrightarrow \|y - c\| = \|m - f\|)$
43	42	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\|))$
44	43	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\|))$
45		oveq1	$⊢ m = e \to m - f = e - f$
46	45	fveq2d	$⊢ m = e \to \|m - f\| = \|e - f\|$
47	46	eqeq2d	$⊢ m = e \to (\|y - c\| = \|m - f\| \leftrightarrow \|y - c\| = \|e - f\|)$
48	47	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\|))$
49	48	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\|))$
50	44 49	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\|)$
51	39 50	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\|)$
52	51	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\|)$
53		oveq1	$⊢ m = e \to m - q = e - q$
54	53	fveq2d	$⊢ m = e \to \|m - q\| = \|e - q\|$
55	54	eqeq2d	$⊢ m = e \to (\|y - l\| = \|m - q\| \leftrightarrow \|y - l\| = \|e - q\|)$
56	55	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\|))$
57		oveq2	$⊢ q = f \to e - q = e - f$
58	57	fveq2d	$⊢ q = f \to \|e - q\| = \|e - f\|$
59	58	eqeq2d	$⊢ q = f \to (\|y - l\| = \|e - q\| \leftrightarrow \|y - l\| = \|e - f\|)$
60	59	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\|))$
61	56 60	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\|)$
62	61	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\|)$
63		oveq2	$⊢ k = c \to j - k = j - c$
64	63	fveq2d	$⊢ k = c \to \|j - k\| = \|j - c\|$
65	64	eqeq2d	$⊢ k = c \to (\|y - i\| = \|j - k\| \leftrightarrow \|y - i\| = \|j - c\|)$
66	65	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\|))$
67	66	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\|))$
68		neeq2	$⊢ l = d \to (i \neq l \leftrightarrow i \neq d)$
69		oveq2	$⊢ l = d \to y - l = y - d$
70	69	fveq2d	$⊢ l = d \to \|y - l\| = \|y - d\|$
71	70	eqeq1d	$⊢ l = d \to (\|y - l\| = \|e - f\| \leftrightarrow \|y - d\| = \|e - f\|)$
72	68 71	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\|))$
73	72	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\|))$
74	67 73	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\|)$
75	62 74	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\|)$
76	75	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\|)$
77	32 52 76	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\|))$
78		id	$⊢ i = a \to i = a$
79		oveq2	$⊢ i = a \to j - i = j - a$
80	79	oveq2d	$⊢ i = a \to t (j - i) = t (j - a)$
81	78 80	oveq12d	$⊢ i = a \to i + t (j - i) = a + t (j - a)$
82	81	eqeq2d	$⊢ i = a \to (y = i + t (j - i) \leftrightarrow y = a + t (j - a))$
83	79	fveq2d	$⊢ i = a \to \overline{j - i} = \overline{j - a}$
84	83	oveq1d	$⊢ i = a \to \overline{j - i} (d - c) = \overline{j - a} (d - c)$
85	84	fveq2d	$⊢ i = a \to ℑ (\overline{j - i} (d - c)) = ℑ (\overline{j - a} (d - c))$
86	85	neeq1d	$⊢ i = a \to (ℑ (\overline{j - i} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{j - a} (d - c)) \neq 0)$
87	82 86	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))$
88	87	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))$
89	88	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))$
90		oveq1	$⊢ j = b \to j - a = b - a$
91	90	oveq2d	$⊢ j = b \to t (j - a) = t (b - a)$
92	91	oveq2d	$⊢ j = b \to a + t (j - a) = a + t (b - a)$
93	92	eqeq2d	$⊢ j = b \to (y = a + t (j - a) \leftrightarrow y = a + t (b - a))$
94	90	fveq2d	$⊢ j = b \to \overline{j - a} = \overline{b - a}$
95	94	oveq1d	$⊢ j = b \to \overline{j - a} (d - c) = \overline{b - a} (d - c)$
96	95	fveq2d	$⊢ j = b \to ℑ (\overline{j - a} (d - c)) = ℑ (\overline{b - a} (d - c))$
97	96	neeq1d	$⊢ j = b \to (ℑ (\overline{j - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - a} (d - c)) \neq 0)$
98	93 97	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))$
99	98	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))$
100	99	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))$
101	89 100	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)$
102	82	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\|))$
103	102	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\|))$
104	103	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\|))$
105	93	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\|))$
106	105	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\|))$
107	106	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\|))$
108	104 107	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\|)$
109		neeq1	$⊢ i = a \to (i \neq d \leftrightarrow a \neq d)$
110		oveq2	$⊢ i = a \to y - i = y - a$
111	110	fveq2d	$⊢ i = a \to \|y - i\| = \|y - a\|$
112	111	eqeq1d	$⊢ i = a \to (\|y - i\| = \|j - c\| \leftrightarrow \|y - a\| = \|j - c\|)$
113	109 112	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\|))$
114	113	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\|))$
115	114	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\|))$
116		oveq1	$⊢ j = b \to j - c = b - c$
117	116	fveq2d	$⊢ j = b \to \|j - c\| = \|b - c\|$
118	117	eqeq2d	$⊢ j = b \to (\|y - a\| = \|j - c\| \leftrightarrow \|y - a\| = \|b - c\|)$
119	118	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\|))$
120	119	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\|))$
121	120	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\|))$
122	115 121	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\|)$
123	101 108 122	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\|))$
124	77 123	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\|))$
125	124	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\|))\}$
126		eqeq1	$⊢ y = x \to (y = a + t (b - a) \leftrightarrow x = a + t (b - a))$
127		eqeq1	$⊢ y = x \to (y = c + r (d - c) \leftrightarrow x = c + r (d - c))$
128		biidd	$⊢ y = x \to (ℑ (\overline{b - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - a} (d - c)) \neq 0)$
129	126 127 128	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))$
130	129	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))$
131	130	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))$
132	131	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))$
133		oveq1	$⊢ y = x \to y - c = x - c$
134	133	fveq2d	$⊢ y = x \to \|y - c\| = \|x - c\|$
135	134	eqeq1d	$⊢ y = x \to (\|y - c\| = \|e - f\| \leftrightarrow \|x - c\| = \|e - f\|)$
136	126 135	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\|))$
137	136	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\|))$
138	137	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\|))$
139	138	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\|))$
140		biidd	$⊢ y = x \to (a \neq d \leftrightarrow a \neq d)$
141		oveq1	$⊢ y = x \to y - a = x - a$
142	141	fveq2d	$⊢ y = x \to \|y - a\| = \|x - a\|$
143	142	eqeq1d	$⊢ y = x \to (\|y - a\| = \|b - c\| \leftrightarrow \|x - a\| = \|b - c\|)$
144		oveq1	$⊢ y = x \to y - d = x - d$
145	144	fveq2d	$⊢ y = x \to \|y - d\| = \|x - d\|$
146	145	eqeq1d	$⊢ y = x \to (\|y - d\| = \|e - f\| \leftrightarrow \|x - d\| = \|e - f\|)$
147	140 143 146	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\|))$
148	147	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\|))$
149	148	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\|))$
150	149	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\|))$
151	132 139 150	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\|)))$
152	151	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\|))\}$
153	125 152	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\|))\}$
154	153	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\|))\})$
155		elequ2	$⊢ z = s \to (a \in z \leftrightarrow a \in s)$
156		elequ2	$⊢ z = s \to (b \in z \leftrightarrow b \in s)$
157		elequ2	$⊢ z = s \to (c \in z \leftrightarrow c \in s)$
158		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))$
159	157 158	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)))$
160	159	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))$
161	156 160	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)))$
162	161	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))$
163	155 162	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)))$
164	163	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))$
165		elequ2	$⊢ z = s \to (e \in z \leftrightarrow e \in s)$
166		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\|))$
167	165 166	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\|)))$
168	167	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\|))$
169	157 168	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\|)))$
170	169	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\|))$
171	156 170	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\|)))$
172	171	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\|))$
173	155 172	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\|)))$
174	173	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\|))$
175		elequ2	$⊢ z = s \to (d \in z \leftrightarrow d \in s)$
176		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\|))$
177	165 176	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\|)))$
178	177	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\|))$
179	175 178	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\|)))$
180	179	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\|))$
181	157 180	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\|)))$
182	181	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\|))$
183	156 182	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\|)))$
184	183	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\|))$
185	155 184	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\|)))$
186	185	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\|))$
187	164 174 186	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\|)))$
188	187	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\|))\}$
189	188	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\|))\})$
190	154 189	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\|))\})$
191		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\})$
192	190 191	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\})$

Metamath Proof Explorer

Theorem constrcbvlem

Proof