constrfin

Description: Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-Jul-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\})$
	constrfin.1	$⊢ φ \to N \in ω$
Assertion	constrfin	$⊢ φ \to C (N) \in Fin$

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		constrfin.1	$⊢ φ \to N \in ω$
3		fveq2	$⊢ m = \emptyset \to C (m) = C (\emptyset)$
4	3	eleq1d	$⊢ m = \emptyset \to (C (m) \in Fin \leftrightarrow C (\emptyset) \in Fin)$
5		fveq2	$⊢ m = n \to C (m) = C (n)$
6	5	eleq1d	$⊢ m = n \to (C (m) \in Fin \leftrightarrow C (n) \in Fin)$
7		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
8	7	eleq1d	$⊢ m = suc n \to (C (m) \in Fin \leftrightarrow C (suc n) \in Fin)$
9		fveq2	$⊢ m = N \to C (m) = C (N)$
10	9	eleq1d	$⊢ m = N \to (C (m) \in Fin \leftrightarrow C (N) \in Fin)$
11	1	constr0	$⊢ C (\emptyset) = \{0, 1\}$
12		prfi	$⊢ \{0, 1\} \in Fin$
13	11 12	eqeltri	$⊢ C (\emptyset) \in Fin$
14		nfv	$⊢ Ⅎ x (n \in ω \land C (n) \in Fin)$
15		nfcv	$⊢ \underline{Ⅎ} x C (suc n)$
16		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ℂ \| (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}$
17		nnon	$⊢ n \in ω \to n \in On$
18	17	adantr	$⊢ (n \in ω \land C (n) \in Fin) \to n \in On$
19		eqid	$⊢ C (n) = C (n)$
20	1 18 19	constrsuc	$⊢ (n \in ω \land C (n) \in Fin) \to (x \in C (suc n) \leftrightarrow (x \in ℂ \land (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))))$
21		rabid	$⊢ x \in \{x \in ℂ \| (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\} \leftrightarrow (x \in ℂ \land (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)))$
22	20 21	bitr4di	$⊢ (n \in ω \land C (n) \in Fin) \to (x \in C (suc n) \leftrightarrow x \in \{x \in ℂ \| (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\})$
23	14 15 16 22	eqrd	$⊢ (n \in ω \land C (n) \in Fin) \to C (suc n) = \{x \in ℂ \| (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}$
24		3unrab	$⊢ (\{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\}) \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} = \{x \in ℂ \| (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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 C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}$
25	23 24	eqtr4di	$⊢ (n \in ω \land C (n) \in Fin) \to C (suc n) = (\{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\}) \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\}$
26		simpr	$⊢ (n \in ω \land C (n) \in Fin) \to C (n) \in Fin$
27	26	adantr	$⊢ ((n \in ω \land C (n) \in Fin) \land a \in C (n)) \to C (n) \in Fin$
28	27	adantr	$⊢ (((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \to C (n) \in Fin$
29	28	adantr	$⊢ ((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \to C (n) \in Fin$
30		snfi	$⊢ \{a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)\} \in Fin$
31	30	a1i	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to \{a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)\} \in Fin$
32	1 17	constrsscn	$⊢ n \in ω \to C (n) \subseteq ℂ$
33	32	ad9antr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to C (n) \subseteq ℂ$
34		simp-8r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to a \in C (n)$
35		simp-7r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to b \in C (n)$
36		simp-6r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to c \in C (n)$
37		simp-5r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to d \in C (n)$
38		simpllr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to t \in ℝ$
39		simplr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to r \in ℝ$
40		simpr1	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to x = a + t (b - a)$
41		simpr2	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to x = c + r (d - c)$
42		simpr3	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{b - a} (d - c)) \neq 0$
43		eqid	$⊢ a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a) = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)$
44	33 34 35 36 37 38 39 40 41 42 43	constrrtll	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land r \in ℝ) \land (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)$
45	44	r19.29an	$⊢ ((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land t \in ℝ) \land \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)$
46	45	r19.29an	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \land \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)) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)$
47	46	ex	$⊢ ((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land x \in ℂ) \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) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a))$
48	47	ralrimiva	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to \forall x \in ℂ (\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) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a))$
49		rabsssn	$⊢ \{x \in ℂ \| \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)\} \subseteq \{a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)\} \leftrightarrow \forall x \in ℂ (\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) \to x = a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a))$
50	48 49	sylibr	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to \{x \in ℂ \| \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)\} \subseteq \{a + (\frac{(a - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c)}{(\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})}) (b - a)\}$
51	31 50	ssfid	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to \{x \in ℂ \| \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)\} \in Fin$
52	29 51	rabrexfi	$⊢ ((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \to \{x \in ℂ \| \exists d \in C (n) \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)\} \in Fin$
53	28 52	rabrexfi	$⊢ (((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \to \{x \in ℂ \| \exists c \in C (n) \exists d \in C (n) \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)\} \in Fin$
54	27 53	rabrexfi	$⊢ ((n \in ω \land C (n) \in Fin) \land a \in C (n)) \to \{x \in ℂ \| \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \in Fin$
55	26 54	rabrexfi	$⊢ (n \in ω \land C (n) \in Fin) \to \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \in Fin$
56	29	adantr	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \to C (n) \in Fin$
57		snfi	$⊢ \{a\} \in Fin$
58	57	a1i	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \to \{a\} \in Fin$
59	32	ad10antr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to C (n) \subseteq ℂ$
60		simp-9r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a \in C (n)$
61		simp-8r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b \in C (n)$
62		simp-7r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c \in C (n)$
63		simp-6r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to e \in C (n)$
64		simp-5r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to f \in C (n)$
65		simplr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to t \in ℝ$
66		simprl	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x = a + t (b - a)$
67		simprr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \|x - c\| = \|e - f\|$
68		simp-4r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a = b$
69	59 60 61 62 63 64 65 66 67 68	constrrtlc2	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x = a$
70	69	r19.29an	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \land \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x = a$
71	70	ex	$⊢ ((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \land x \in ℂ) \to (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to x = a)$
72	71	ralrimiva	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \to \forall x \in ℂ (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to x = a)$
73		rabsssn	$⊢ \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \subseteq \{a\} \leftrightarrow \forall x \in ℂ (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to x = a)$
74	72 73	sylibr	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \to \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \subseteq \{a\}$
75	58 74	ssfid	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a = b) \to \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
76		prfi	$⊢ \{\frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}, \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}\} \in Fin$
77	76	a1i	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \to \{\frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}, \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}\} \in Fin$
78		simpllr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x \in ℂ$
79		1cnd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to 1 \in ℂ$
80		ax-1ne0	$⊢ 1 \neq 0$
81	80	a1i	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to 1 \neq 0$
82	32	ad10antr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to C (n) \subseteq ℂ$
83		simp-9r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a \in C (n)$
84	82 83	sseldd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a \in ℂ$
85	84	cjcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{a} \in ℂ$
86		simp-8r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b \in C (n)$
87	82 86	sseldd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b \in ℂ$
88	87	cjcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{b} \in ℂ$
89	88 85	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{b} - \overline{a} \in ℂ$
90	87 84	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b - a \in ℂ$
91		simp-4r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a \neq b$
92	91	necomd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b \neq a$
93	87 84 92	subne0d	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to b - a \neq 0$
94	89 90 93	divcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \frac{\overline{b} - \overline{a}}{b - a} \in ℂ$
95	84 94	mulcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to a (\frac{\overline{b} - \overline{a}}{b - a}) \in ℂ$
96	85 95	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) \in ℂ$
97		simp-7r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c \in C (n)$
98	82 97	sseldd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c \in ℂ$
99	98	cjcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{c} \in ℂ$
100	96 99	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c} \in ℂ$
101	98 94	mulcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c (\frac{\overline{b} - \overline{a}}{b - a}) \in ℂ$
102	100 101	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a}) \in ℂ$
103		simp-6r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to e \in C (n)$
104		simp-5r	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to f \in C (n)$
105		simplr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to t \in ℝ$
106		simprl	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x = a + t (b - a)$
107		simprr	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \|x - c\| = \|e - f\|$
108		eqid	$⊢ \frac{\overline{b} - \overline{a}}{b - a} = \frac{\overline{b} - \overline{a}}{b - a}$
109		eqid	$⊢ \frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}} = \frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}$
110		eqid	$⊢ \frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}} = \frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}}$
111	82 83 86 97 103 104 105 106 107 108 109 110 91	constrrtlc1	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to (x^{2} + (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) x + (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}}) = 0 \land \frac{\overline{b} - \overline{a}}{b - a} \neq 0)$
112	111	simprd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \frac{\overline{b} - \overline{a}}{b - a} \neq 0$
113	102 94 112	divcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}} \in ℂ$
114	98 100	mulcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) \in ℂ$
115	82 103	sseldd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to e \in ℂ$
116	82 104	sseldd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to f \in ℂ$
117	115 116	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to e - f \in ℂ$
118	115	cjcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{e} \in ℂ$
119	116	cjcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{f} \in ℂ$
120	118 119	subcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \overline{e} - \overline{f} \in ℂ$
121	117 120	mulcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to (e - f) (\overline{e} - \overline{f}) \in ℂ$
122	114 121	addcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}) \in ℂ$
123	122	negcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to - (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f})) \in ℂ$
124	123 94 112	divcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to \frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}} \in ℂ$
125	78	sqcld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x^{2} \in ℂ$
126	125	mullidd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to 1 x^{2} = x^{2}$
127	126	oveq1d	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to 1 x^{2} + (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) x + (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}}) = x^{2} + (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) x + (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})$
128	111	simpld	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to x^{2} + (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) x + (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}}) = 0$
129	127 128	eqtrd	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to 1 x^{2} + (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) x + (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}}) = 0$
130	78 79 81 113 124 129	quad3d	$⊢ ((((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land t \in ℝ) \land (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to (x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1})$
131	130	r19.29an	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \land \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)) \to (x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1})$
132	131	ex	$⊢ ((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \land x \in ℂ) \to (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to (x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}))$
133	132	ralrimiva	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \to \forall x \in ℂ (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to (x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}))$
134		rabsspr	$⊢ \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \subseteq \{\frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}, \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}\} \leftrightarrow \forall x \in ℂ (\exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \to (x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}))$
135	133 134	sylibr	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \to \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \subseteq \{\frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) + \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}, \frac{- (\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}}) - \sqrt{{(\frac{(\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a})}{\frac{\overline{b} - \overline{a}}{b - a}})}^{2} - 4 1 (\frac{- (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))}{\frac{\overline{b} - \overline{a}}{b - a}})}}{2 \cdot 1}\}$
136	77 135	ssfid	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \land a \neq b) \to \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
137		exmidne	$⊢ (a = b \lor a \neq b)$
138	137	a1i	$⊢ ((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \to (a = b \lor a \neq b)$
139	75 136 138	mpjaodan	$⊢ ((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \to \{x \in ℂ \| \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
140	56 139	rabrexfi	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \to \{x \in ℂ \| \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
141	29 140	rabrexfi	$⊢ ((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \to \{x \in ℂ \| \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
142	28 141	rabrexfi	$⊢ (((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \to \{x \in ℂ \| \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
143	27 142	rabrexfi	$⊢ ((n \in ω \land C (n) \in Fin) \land a \in C (n)) \to \{x \in ℂ \| \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
144	26 143	rabrexfi	$⊢ (n \in ω \land C (n) \in Fin) \to \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
145	55 144	unfid	$⊢ (n \in ω \land C (n) \in Fin) \to \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\} \in Fin$
146	29	adantr	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to C (n) \in Fin$
147	146	adantr	$⊢ ((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \to C (n) \in Fin$
148		prfi	$⊢ \{\frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}, \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}\} \in Fin$
149	148	a1i	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to \{\frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}, \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}\} \in Fin$
150		simplr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to x \in ℂ$
151		1cnd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to 1 \in ℂ$
152	80	a1i	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to 1 \neq 0$
153	32	ad9antr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to C (n) \subseteq ℂ$
154		simp-4r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to e \in C (n)$
155	153 154	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to e \in ℂ$
156		simpllr	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to f \in C (n)$
157	153 156	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to f \in ℂ$
158	155 157	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to e - f \in ℂ$
159	158	cjcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{e - f} \in ℂ$
160	158 159	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (e - f) \overline{e - f} \in ℂ$
161		simp-5r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d \in C (n)$
162	153 161	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d \in ℂ$
163	162	cjcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} \in ℂ$
164		simp-8r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to a \in C (n)$
165	153 164	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to a \in ℂ$
166	162 165	addcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d + a \in ℂ$
167	163 166	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} (d + a) \in ℂ$
168	160 167	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (e - f) \overline{e - f} - \overline{d} (d + a) \in ℂ$
169		simp-7r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to b \in C (n)$
170	153 169	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to b \in ℂ$
171		simp-6r	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to c \in C (n)$
172	153 171	sseldd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to c \in ℂ$
173	170 172	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to b - c \in ℂ$
174	173	cjcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{b - c} \in ℂ$
175	173 174	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (b - c) \overline{b - c} \in ℂ$
176	165	cjcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{a} \in ℂ$
177	176 166	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{a} (d + a) \in ℂ$
178	175 177	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (b - c) \overline{b - c} - \overline{a} (d + a) \in ℂ$
179	168 178	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a)) \in ℂ$
180	163 176	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} - \overline{a} \in ℂ$
181	162 165	cjsubd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d - a} = \overline{d} - \overline{a}$
182	162 165	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d - a \in ℂ$
183		simpr1	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to a \neq d$
184	183	necomd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d \neq a$
185	162 165 184	subne0d	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d - a \neq 0$
186	182 185	cjne0d	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d - a} \neq 0$
187	181 186	eqnetrrd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} - \overline{a} \neq 0$
188	179 180 187	divcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}} \in ℂ$
189	162 165	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to d a \in ℂ$
190	176 189	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{a} d a \in ℂ$
191	175 162	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (b - c) \overline{b - c} d \in ℂ$
192	190 191	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{a} d a - (b - c) \overline{b - c} d \in ℂ$
193	163 189	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} d a \in ℂ$
194	160 165	mulcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (e - f) \overline{e - f} a \in ℂ$
195	193 194	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{d} d a - (e - f) \overline{e - f} a \in ℂ$
196	192 195	subcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a) \in ℂ$
197	196 180 187	divcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}} \in ℂ$
198	197	negcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to - \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}} \in ℂ$
199	150	sqcld	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to x^{2} \in ℂ$
200	199	mullidd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to 1 x^{2} = x^{2}$
201	200	oveq1d	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to 1 x^{2} + (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) x + (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}}) = x^{2} + (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) x + (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})$
202		simpr2	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \|x - a\| = \|b - c\|$
203		simpr3	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to \|x - d\| = \|e - f\|$
204		eqid	$⊢ (b - c) \overline{b - c} = (b - c) \overline{b - c}$
205		eqid	$⊢ (e - f) \overline{e - f} = (e - f) \overline{e - f}$
206		eqid	$⊢ \frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}} = \frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}$
207		eqid	$⊢ - \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}} = - \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}}$
208	153 164 169 171 161 154 156 150 183 202 203 204 205 206 207	constrrtcc	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to x^{2} + (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) x + (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}}) = 0$
209	201 208	eqtrd	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to 1 x^{2} + (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) x + (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}}) = 0$
210	150 151 152 188 198 209	quad3d	$⊢ (((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \land (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)) \to (x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1})$
211	210	ex	$⊢ ((((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \land x \in ℂ) \to ((a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \to (x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}))$
212	211	ralrimiva	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to \forall x \in ℂ ((a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \to (x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}))$
213		rabsspr	$⊢ \{x \in ℂ \| (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \subseteq \{\frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}, \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}\} \leftrightarrow \forall x \in ℂ ((a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|) \to (x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1} \lor x = \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}))$
214	212 213	sylibr	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to \{x \in ℂ \| (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \subseteq \{\frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) + \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}, \frac{- (\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}}) - \sqrt{{(\frac{(e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a))}{\overline{d} - \overline{a}})}^{2} - 4 1 (- \frac{\overline{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a)}{\overline{d} - \overline{a}})}}{2 \cdot 1}\}$
215	149 214	ssfid	$⊢ (((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to \{x \in ℂ \| (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
216	147 215	rabrexfi	$⊢ ((((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \to \{x \in ℂ \| \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
217	146 216	rabrexfi	$⊢ (((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to \{x \in ℂ \| \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
218	29 217	rabrexfi	$⊢ ((((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \to \{x \in ℂ \| \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
219	28 218	rabrexfi	$⊢ (((n \in ω \land C (n) \in Fin) \land a \in C (n)) \land b \in C (n)) \to \{x \in ℂ \| \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
220	27 219	rabrexfi	$⊢ ((n \in ω \land C (n) \in Fin) \land a \in C (n)) \to \{x \in ℂ \| \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
221	26 220	rabrexfi	$⊢ (n \in ω \land C (n) \in Fin) \to \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
222	145 221	unfid	$⊢ (n \in ω \land C (n) \in Fin) \to (\{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \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)\} \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|)\}) \cup \{x \in ℂ \| \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|)\} \in Fin$
223	25 222	eqeltrd	$⊢ (n \in ω \land C (n) \in Fin) \to C (suc n) \in Fin$
224	223	ex	$⊢ n \in ω \to (C (n) \in Fin \to C (suc n) \in Fin)$
225	4 6 8 10 13 224	finds	$⊢ N \in ω \to C (N) \in Fin$
226	2 225	syl	$⊢ φ \to C (N) \in Fin$

Metamath Proof Explorer

Theorem constrfin

Proof