constrsuc

Description: Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrsuc.1	$⊢ φ \to N \in On$
	constrsuc.2	$⊢ S = C (N)$
Assertion	constrsuc	$⊢ φ \to (X \in C (suc N) \leftrightarrow (X \in ℂ \land (\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\|))))$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrsuc.1	$⊢ φ \to N \in On$
3		constrsuc.2	$⊢ S = C (N)$
4	1	fveq1i	$⊢ C (suc N) = 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\}) (suc N)$
5		rdgsuc	$⊢ N \in On \to 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\}) (suc N) = (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\|))\}) (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\}) (N))$
6	2 5	syl	$⊢ φ \to 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\}) (suc N) = (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\|))\}) (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\}) (N))$
7	4 6	eqtrid	$⊢ φ \to C (suc N) = (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\|))\}) (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\}) (N))$
8	1	fveq1i	$⊢ C (N) = 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\}) (N)$
9	3 8	eqtri	$⊢ S = 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\}) (N)$
10	9	fveq2i	$⊢ (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\|))\}) (S) = (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\|))\}) (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\}) (N))$
11	7 10	eqtr4di	$⊢ φ \to C (suc N) = (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\|))\}) (S)$
12	11	eleq2d	$⊢ φ \to (X \in C (suc N) \leftrightarrow X \in (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\|))\}) (S))$
13		eqid	$⊢ (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\|))\}) = (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\|))\})$
14		id	$⊢ s = S \to s = S$
15		rexeq	$⊢ s = S \to (\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) \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))$
16	14 15	rexeqbidv	$⊢ s = S \to (\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) \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))$
17	14 16	rexeqbidv	$⊢ s = S \to (\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) \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))$
18	14 17	rexeqbidv	$⊢ s = S \to (\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) \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))$
19		rexeq	$⊢ s = S \to (\exists f \in s \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\|))$
20	14 19	rexeqbidv	$⊢ s = S \to (\exists e \in s \exists f \in s \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\|))$
21	14 20	rexeqbidv	$⊢ s = S \to (\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\|) \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\|))$
22	14 21	rexeqbidv	$⊢ s = S \to (\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\|) \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\|))$
23	14 22	rexeqbidvv	$⊢ s = S \to (\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\|) \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\|))$
24		rexeq	$⊢ s = S \to (\exists f \in s (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\|))$
25	14 24	rexeqbidv	$⊢ s = S \to (\exists e \in s \exists f \in s (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\|))$
26	14 25	rexeqbidv	$⊢ s = S \to (\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\|) \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\|))$
27	14 26	rexeqbidv	$⊢ s = S \to (\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\|) \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\|))$
28	14 27	rexeqbidv	$⊢ s = S \to (\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\|) \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\|))$
29	14 28	rexeqbidvv	$⊢ s = S \to (\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\|) \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\|))$
30	18 23 29	3orbi123d	$⊢ s = S \to ((\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\|)) \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\|)))$
31	30	rabbidv	$⊢ s = S \to \{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\|))\} = \{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\|))\}$
32	31	adantl	$⊢ (φ \land s = S) \to \{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\|))\} = \{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\|))\}$
33	3	fvexi	$⊢ S \in V$
34	33	a1i	$⊢ φ \to S \in V$
35		cnex	$⊢ ℂ \in V$
36		ssrab2	$⊢ \{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\|))\} \subseteq ℂ$
37	35 36	ssexi	$⊢ \{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\|))\} \in V$
38	37	a1i	$⊢ φ \to \{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\|))\} \in V$
39	13 32 34 38	fvmptd2	$⊢ φ \to (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\|))\}) (S) = \{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\|))\}$
40	39	eleq2d	$⊢ φ \to (X \in (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\|))\}) (S) \leftrightarrow X \in \{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\|))\})$
41		eqeq1	$⊢ x = y \to (x = a + t (b - a) \leftrightarrow y = a + t (b - a))$
42		eqeq1	$⊢ x = y \to (x = c + r (d - c) \leftrightarrow y = c + r (d - c))$
43	41 42	3anbi12d	$⊢ x = y \to ((x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - 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))$
44	43	2rexbidv	$⊢ x = y \to (\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 t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
45	44	2rexbidv	$⊢ x = y \to (\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) \leftrightarrow \exists c \in S \exists d \in S \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))$
46	45	2rexbidv	$⊢ x = y \to (\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) \leftrightarrow \exists a \in S \exists b \in S \exists c \in S \exists d \in S \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))$
47		fvoveq1	$⊢ x = y \to \|x - c\| = \|y - c\|$
48	47	eqeq1d	$⊢ x = y \to (\|x - c\| = \|e - f\| \leftrightarrow \|y - c\| = \|e - f\|)$
49	41 48	anbi12d	$⊢ x = y \to ((x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
50	49	2rexbidv	$⊢ x = y \to (\exists f \in S \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \leftrightarrow \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
51	50	2rexbidv	$⊢ x = y \to (\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\|) \leftrightarrow \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
52	51	2rexbidv	$⊢ x = y \to (\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\|) \leftrightarrow \exists a \in S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|))$
53		fvoveq1	$⊢ x = y \to \|x - a\| = \|y - a\|$
54	53	eqeq1d	$⊢ x = y \to (\|x - a\| = \|b - c\| \leftrightarrow \|y - a\| = \|b - c\|)$
55		fvoveq1	$⊢ x = y \to \|x - d\| = \|y - d\|$
56	55	eqeq1d	$⊢ x = y \to (\|x - d\| = \|e - f\| \leftrightarrow \|y - d\| = \|e - f\|)$
57	54 56	3anbi23d	$⊢ x = y \to ((a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \leftrightarrow (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
58	57	2rexbidv	$⊢ x = y \to (\exists e \in S \exists f \in S (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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
59	58	2rexbidv	$⊢ x = y \to (\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\|) \leftrightarrow \exists c \in S \exists d \in S \exists e \in S \exists f \in S (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
60	59	2rexbidv	$⊢ x = y \to (\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\|) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
61	46 52 60	3orbi123d	$⊢ x = y \to ((\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\|)) \leftrightarrow (\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)))$
62	61	cbvrabv	$⊢ \{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\|))\} = \{y \in ℂ \| (\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))\}$
63	62	eleq2i	$⊢ X \in \{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\|))\} \leftrightarrow X \in \{y \in ℂ \| (\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))\}$
64		eqeq1	$⊢ y = X \to (y = a + t (b - a) \leftrightarrow X = a + t (b - a))$
65		eqeq1	$⊢ y = X \to (y = c + r (d - c) \leftrightarrow X = c + r (d - c))$
66	64 65	3anbi12d	$⊢ 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))$
67	66	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))$
68	67	2rexbidv	$⊢ y = X \to (\exists c \in S \exists d \in S \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 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))$
69	68	2rexbidv	$⊢ y = X \to (\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 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))$
70		fvoveq1	$⊢ y = X \to \|y - c\| = \|X - c\|$
71	70	eqeq1d	$⊢ y = X \to (\|y - c\| = \|e - f\| \leftrightarrow \|X - c\| = \|e - f\|)$
72	64 71	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\|))$
73	72	2rexbidv	$⊢ y = X \to (\exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \leftrightarrow \exists f \in S \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|))$
74	73	2rexbidv	$⊢ y = X \to (\exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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\|))$
75	74	2rexbidv	$⊢ y = X \to (\exists a \in S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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\|))$
76		fvoveq1	$⊢ y = X \to \|y - a\| = \|X - a\|$
77	76	eqeq1d	$⊢ y = X \to (\|y - a\| = \|b - c\| \leftrightarrow \|X - a\| = \|b - c\|)$
78		fvoveq1	$⊢ y = X \to \|y - d\| = \|X - d\|$
79	78	eqeq1d	$⊢ y = X \to (\|y - d\| = \|e - f\| \leftrightarrow \|X - d\| = \|e - f\|)$
80	77 79	3anbi23d	$⊢ 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\|))$
81	80	2rexbidv	$⊢ y = X \to (\exists e \in S \exists f \in S (a \neq d \land \|y - a\| = \|b - c\| \land \|y - 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\|))$
82	81	2rexbidv	$⊢ y = X \to (\exists c \in S \exists d \in S \exists e \in S \exists f \in S (a \neq d \land \|y - a\| = \|b - c\| \land \|y - 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\|))$
83	82	2rexbidv	$⊢ y = X \to (\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 \|y - a\| = \|b - c\| \land \|y - 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\|))$
84	69 75 83	3orbi123d	$⊢ y = X \to ((\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - 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\|)))$
85	84	elrab	$⊢ X \in \{y \in ℂ \| (\exists a \in S \exists b \in S \exists c \in S \exists d \in S \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 S \exists b \in S \exists c \in S \exists e \in S \exists f \in S \exists t \in ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))\} \leftrightarrow (X \in ℂ \land (\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\|)))$
86	63 85	bitri	$⊢ X \in \{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\|))\} \leftrightarrow (X \in ℂ \land (\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\|)))$
87	86	a1i	$⊢ φ \to (X \in \{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\|))\} \leftrightarrow (X \in ℂ \land (\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\|))))$
88	12 40 87	3bitrd	$⊢ φ \to (X \in C (suc N) \leftrightarrow (X \in ℂ \land (\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\|))))$

Metamath Proof Explorer

Theorem constrsuc

Proof