constrelextdg2

Description: If the N -th step ( CN ) of the construction of constuctible numbers is included in a subfield F of the complex numbers, then any element X of the next step ( Csuc N ) is either in F or in a quadratic extension of F . (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\})$
	constrelextdg2.k	$⊢ K = ℂ_{fld} ↾_{𝑠} F$
	constrelextdg2.l	$⊢ L = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (F \cup \{X\}))$
	constrelextdg2.f	$⊢ φ \to F \in SubDRing (ℂ_{fld})$
	constrelextdg2.n	$⊢ φ \to N \in On$
	constrelextdg2.1	$⊢ φ \to C (N) \subseteq F$
	constrelextdg2.x	$⊢ φ \to X \in C (suc N)$
Assertion	constrelextdg2	$⊢ φ \to (X \in F \lor L [. : .] K = 2)$

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		constrelextdg2.k	$⊢ K = ℂ_{fld} ↾_{𝑠} F$
3		constrelextdg2.l	$⊢ L = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (F \cup \{X\}))$
4		constrelextdg2.f	$⊢ φ \to F \in SubDRing (ℂ_{fld})$
5		constrelextdg2.n	$⊢ φ \to N \in On$
6		constrelextdg2.1	$⊢ φ \to C (N) \subseteq F$
7		constrelextdg2.x	$⊢ φ \to X \in C (suc N)$
8		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
9	8	sdrgss	$⊢ F \in SubDRing (ℂ_{fld}) \to F \subseteq ℂ$
10	4 9	syl	$⊢ φ \to F \subseteq ℂ$
11	10	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F \subseteq ℂ$
12	6	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F$
13		simp-7r	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
14	12 13	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F$
15		simp-6r	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
16	12 15	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F$
17		simp-5r	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
18	12 17	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F$
19		simp-4r	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
20	12 19	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F$
21		simpllr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℝ$
22		simplr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℝ$
23		simpr1	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
24		simpr2	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
25		simpr3	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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$
26		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)$
27	11 14 16 18 20 21 22 23 24 25 26	constrrtll	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)$
28		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
29		sdrgsubrg	$⊢ F \in SubDRing (ℂ_{fld}) \to F \in SubRing (ℂ_{fld})$
30		subrgsubg	$⊢ F \in SubRing (ℂ_{fld}) \to F \in SubGrp (ℂ_{fld})$
31	4 29 30	3syl	$⊢ φ \to F \in SubGrp (ℂ_{fld})$
32	31	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F \in SubGrp (ℂ_{fld})$
33		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
34	4 29	syl	$⊢ φ \to F \in SubRing (ℂ_{fld})$
35	34	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F \in SubRing (ℂ_{fld})$
36		cnflddiv	$⊢ \div = /_{r} (ℂ_{fld})$
37		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
38	4	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 F \in SubDRing (ℂ_{fld})$
39		cnfldsub	$⊢ - = -_{ℂ_{fld}}$
40	39 32 14 18	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - c \in F$
41	5	ad7antr	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 N \in On$
42	1 41 19	constrconj	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{d} \in C (N)$
43	12 42	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{d} \in F$
44	1 41 17	constrconj	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{c} \in C (N)$
45	12 44	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{c} \in F$
46	39 32 43 45	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{d} - \overline{c} \in F$
47	33 35 40 46	subrgmcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - c) (\overline{d} - \overline{c}) \in F$
48	1 41 13	constrconj	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{a} \in C (N)$
49	12 48	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{a} \in F$
50	39 32 49 45	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{a} - \overline{c} \in F$
51	39 32 20 18	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - c \in F$
52	33 35 50 51	subrgmcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{a} - \overline{c}) (d - c) \in F$
53	39 32 47 52	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - c) (\overline{d} - \overline{c}) - (\overline{a} - \overline{c}) (d - c) \in F$
54	1 41 15	constrconj	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} \in C (N)$
55	12 54	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} \in F$
56	39 32 55 49	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} - \overline{a} \in F$
57	33 35 56 51	subrgmcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} - \overline{a}) (d - c) \in F$
58	39 32 16 14	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - a \in F$
59	33 35 58 46	subrgmcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - a) (\overline{d} - \overline{c}) \in F$
60	39 32 57 59	subgsubcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c}) \in F$
61	11 16	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℂ$
62	11 14	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℂ$
63	61 62	cjsubd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} = \overline{b} - \overline{a}$
64	63	oveq1d	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) = (\overline{b} - \overline{a}) (d - c)$
65	11 58	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - a \in ℂ$
66	65	cjcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} \in ℂ$
67	11 51	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 - c \in ℂ$
68	66 67	cjmuld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{\overline{b - a} (d - c)} = \overline{\overline{b - a}} \overline{d - c}$
69	65	cjcjd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{\overline{b - a}} = b - a$
70	11 20	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℂ$
71	11 18	sseldd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 ℂ$
72	70 71	cjsubd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{d - c} = \overline{d} - \overline{c}$
73	69 72	oveq12d	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{\overline{b - a}} \overline{d - c} = (b - a) (\overline{d} - \overline{c})$
74	68 73	eqtrd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{\overline{b - a} (d - c)} = (b - a) (\overline{d} - \overline{c})$
75	64 74	oveq12d	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) - \overline{\overline{b - a} (d - c)} = (\overline{b} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c})$
76	66 67	mulcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) \in ℂ$
77		imval2	$⊢ \overline{b - a} (d - c) \in ℂ \to ℑ (\overline{b - a} (d - c)) = \frac{\overline{b - a} (d - c) - \overline{\overline{b - a} (d - c)}}{2 i}$
78	76 77	syl	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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)) = \frac{\overline{b - a} (d - c) - \overline{\overline{b - a} (d - c)}}{2 i}$
79	78	neeq1d	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \leftrightarrow \frac{\overline{b - a} (d - c) - \overline{\overline{b - a} (d - c)}}{2 i} \neq 0)$
80	25 79	mpbid	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \frac{\overline{b - a} (d - c) - \overline{\overline{b - a} (d - c)}}{2 i} \neq 0$
81	76	cjcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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{\overline{b - a} (d - c)} \in ℂ$
82	76 81	subcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) - \overline{\overline{b - a} (d - c)} \in ℂ$
83		2cnd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 2 \in ℂ$
84		ax-icn	$⊢ i \in ℂ$
85	84	a1i	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 i \in ℂ$
86	83 85	mulcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 2 i \in ℂ$
87		2cn	$⊢ 2 \in ℂ$
88		2ne0	$⊢ 2 \neq 0$
89		ine0	$⊢ i \neq 0$
90	87 84 88 89	mulne0i	$⊢ 2 i \neq 0$
91	90	a1i	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 2 i \neq 0$
92	82 86 91	divne0bd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) - \overline{\overline{b - a} (d - c)} \neq 0 \leftrightarrow \frac{\overline{b - a} (d - c) - \overline{\overline{b - a} (d - c)}}{2 i} \neq 0)$
93	80 92	mpbird	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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) - \overline{\overline{b - a} (d - c)} \neq 0$
94	75 93	eqnetrrd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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} - \overline{a}) (d - c) - (b - a) (\overline{d} - \overline{c}) \neq 0$
95	36 37 38 53 60 94	sdrgdvcl	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \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})} \in F$
96	33 35 95 58	subrgmcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 (\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 F$
97	28 32 14 96	subgcld	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 + (\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 F$
98	27 97	eqeltrd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \in F$
99	98	orcd	$⊢ (((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \in F \lor L [. : .] K = 2)$
100	99	r19.29an	$⊢ ((((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \in F \lor L [. : .] K = 2)$
101	100	r19.29an	$⊢ (((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \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 \in F \lor L [. : .] K = 2)$
102	101	r19.29an	$⊢ ((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land \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)) \to (X \in F \lor L [. : .] K = 2)$
103	102	r19.29an	$⊢ (((φ \land a \in C (N)) \land b \in C (N)) \land \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)) \to (X \in F \lor L [. : .] K = 2)$
104	103	r19.29an	$⊢ ((φ \land a \in C (N)) \land \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)) \to (X \in F \lor L [. : .] K = 2)$
105	104	r19.29an	$⊢ (φ \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)) \to (X \in F \lor L [. : .] K = 2)$
106	1 5	constrsscn	$⊢ φ \to C (N) \subseteq ℂ$
107	106	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to C (N) \subseteq ℂ$
108		simp-8r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to a \in C (N)$
109		simp-7r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to b \in C (N)$
110		simp-6r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to c \in C (N)$
111		simp-5r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to e \in C (N)$
112		simp-4r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to f \in C (N)$
113		simpllr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to t \in ℝ$
114		simplrl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to X = a + t (b - a)$
115		simplrr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to \|X - c\| = \|e - f\|$
116		simpr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to a = b$
117	107 108 109 110 111 112 113 114 115 116	constrrtlc2	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to X = a$
118	6	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to C (N) \subseteq F$
119	118 108	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to a \in F$
120	117 119	eqeltrd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to X \in F$
121	120	orcd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a = b) \to (X \in F \lor L [. : .] K = 2)$
122		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
123		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
124		cnfldfld	$⊢ ℂ_{fld} \in Field$
125	124	a1i	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to ℂ_{fld} \in Field$
126	4	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to F \in SubDRing (ℂ_{fld})$
127		eqid	$⊢ C (N) = C (N)$
128	1 5 127	constrsuc	$⊢ φ \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\|))))$
129	7 128	mpbid	$⊢ φ \to (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\|)))$
130	129	simpld	$⊢ φ \to X \in ℂ$
131	130	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to X \in ℂ$
132	31	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to F \in SubGrp (ℂ_{fld})$
133	6	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to C (N) \subseteq F$
134	5	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to N \in On$
135		simp-8r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to a \in C (N)$
136	1 134 135	constrconj	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{a} \in C (N)$
137	133 136	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{a} \in F$
138	126 29	syl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to F \in SubRing (ℂ_{fld})$
139	133 135	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to a \in F$
140		simp-7r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b \in C (N)$
141	1 134 140	constrconj	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{b} \in C (N)$
142	133 141	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{b} \in F$
143	39 132 142 137	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{b} - \overline{a} \in F$
144	133 140	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b \in F$
145	39 132 144 139	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b - a \in F$
146	106	ad8antr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to C (N) \subseteq ℂ$
147	146 140	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b \in ℂ$
148	146 135	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to a \in ℂ$
149		simpr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to a \neq b$
150	149	necomd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b \neq a$
151	147 148 150	subne0d	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to b - a \neq 0$
152	36 37 126 143 145 151	sdrgdvcl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \frac{\overline{b} - \overline{a}}{b - a} \in F$
153	33 138 139 152	subrgmcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to a (\frac{\overline{b} - \overline{a}}{b - a}) \in F$
154	39 132 137 153	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) \in F$
155		simp-6r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to c \in C (N)$
156	1 134 155	constrconj	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{c} \in C (N)$
157	133 156	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{c} \in F$
158	39 132 154 157	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c} \in F$
159	133 155	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to c \in F$
160	33 138 159 152	subrgmcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to c (\frac{\overline{b} - \overline{a}}{b - a}) \in F$
161	39 132 158 160	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a})) - \overline{c} - c (\frac{\overline{b} - \overline{a}}{b - a}) \in F$
162		simp-5r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to e \in C (N)$
163		simp-4r	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to f \in C (N)$
164		simpllr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to t \in ℝ$
165		simplrl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to X = a + t (b - a)$
166		simplrr	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \|X - c\| = \|e - f\|$
167		eqid	$⊢ \frac{\overline{b} - \overline{a}}{b - a} = \frac{\overline{b} - \overline{a}}{b - a}$
168		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}}$
169		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}}$
170	146 135 140 155 162 163 164 165 166 167 168 169 149	constrrtlc1	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \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)$
171	170	simprd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \frac{\overline{b} - \overline{a}}{b - a} \neq 0$
172	36 37 126 161 152 171	sdrgdvcl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \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 F$
173		df-neg	$⊢ - (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f})) = 0 - (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}))$
174	1 134	constr01	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \{0, 1\} \subseteq C (N)$
175	37	fvexi	$⊢ 0 \in V$
176	175	prid1	$⊢ 0 \in \{0, 1\}$
177	176	a1i	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 0 \in \{0, 1\}$
178	174 177	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 0 \in C (N)$
179	133 178	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 0 \in F$
180	33 138 159 158	subrgmcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) \in F$
181	133 162	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to e \in F$
182	133 163	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to f \in F$
183	39 132 181 182	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to e - f \in F$
184	1 134 162	constrconj	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{e} \in C (N)$
185	133 184	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{e} \in F$
186	1 134 163	constrconj	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{f} \in C (N)$
187	133 186	sseldd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{f} \in F$
188	39 132 185 187	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to \overline{e} - \overline{f} \in F$
189	33 138 183 188	subrgmcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to (e - f) (\overline{e} - \overline{f}) \in F$
190	28 132 180 189	subgcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f}) \in F$
191	39 132 179 190	subgsubcld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 0 - (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f})) \in F$
192	173 191	eqeltrid	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to - (c (\overline{a} - a (\frac{\overline{b} - \overline{a}}{b - a}) - \overline{c}) + (e - f) (\overline{e} - \overline{f})) \in F$
193	36 37 126 192 152 171	sdrgdvcl	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \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 F$
194		2nn0	$⊢ 2 \in ℕ_{0}$
195	194	a1i	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 2 \in ℕ_{0}$
196		cnfldexp	$⊢ (X \in ℂ \land 2 \in ℕ_{0}) \to 2 \cdot_{{mulGrp}_{ℂ_{fld}}} X = X^{2}$
197	131 195 196	syl2anc	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to 2 \cdot_{{mulGrp}_{ℂ_{fld}}} X = X^{2}$
198	197	oveq1d	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to (2 \cdot_{{mulGrp}_{ℂ_{fld}}} X) + (\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}})$
199	170	simpld	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \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$
200	198 199	eqtrd	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to (2 \cdot_{{mulGrp}_{ℂ_{fld}}} X) + (\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$
201	2 3 37 122 8 33 28 123 125 126 131 172 193 200	rtelextdg2	$⊢ ((((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \land a \neq b) \to (X \in F \lor L [. : .] K = 2)$
202		exmidne	$⊢ (a = b \lor a \neq b)$
203	202	a1i	$⊢ (((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \to (a = b \lor a \neq b)$
204	121 201 203	mpjaodan	$⊢ (((((((φ \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 t \in ℝ) \land (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
205	204	r19.29an	$⊢ ((((((φ \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 \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
206	205	r19.29an	$⊢ (((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land e \in C (N)) \land \exists f \in C (N) \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
207	206	r19.29an	$⊢ ((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land \exists e \in C (N) \exists f \in C (N) \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
208	207	r19.29an	$⊢ (((φ \land a \in C (N)) \land b \in C (N)) \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
209	208	r19.29an	$⊢ ((φ \land a \in C (N)) \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
210	209	r19.29an	$⊢ (φ \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
211	124	a1i	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to ℂ_{fld} \in Field$
212	4	ad7antr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to F \in SubDRing (ℂ_{fld})$
213	130	ad7antr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to X \in ℂ$
214	212 29 30	3syl	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to F \in SubGrp (ℂ_{fld})$
215	212 29	syl	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to F \in SubRing (ℂ_{fld})$
216	6	ad7antr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to C (N) \subseteq F$
217		simpllr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to e \in C (N)$
218	216 217	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to e \in F$
219		simplr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to f \in C (N)$
220	216 219	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to f \in F$
221	39 214 218 220	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to e - f \in F$
222	106	ad7antr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to C (N) \subseteq ℂ$
223	222 217	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to e \in ℂ$
224	222 219	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to f \in ℂ$
225	223 224	cjsubd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{e - f} = \overline{e} - \overline{f}$
226	5	ad7antr	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to N \in On$
227	1 226 217	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{e} \in C (N)$
228	216 227	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{e} \in F$
229	1 226 219	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{f} \in C (N)$
230	216 229	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{f} \in F$
231	39 214 228 230	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{e} - \overline{f} \in F$
232	225 231	eqeltrd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{e - f} \in F$
233	33 215 221 232	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (e - f) \overline{e - f} \in F$
234		simp-4r	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d \in C (N)$
235	1 226 234	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} \in C (N)$
236	216 235	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} \in F$
237	216 234	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d \in F$
238		simp-7r	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to a \in C (N)$
239	216 238	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to a \in F$
240	28 214 237 239	subgcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d + a \in F$
241	33 215 236 240	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} (d + a) \in F$
242	39 214 233 241	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (e - f) \overline{e - f} - \overline{d} (d + a) \in F$
243		simp-6r	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to b \in C (N)$
244	216 243	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to b \in F$
245		simp-5r	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to c \in C (N)$
246	216 245	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to c \in F$
247	39 214 244 246	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to b - c \in F$
248	222 243	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to b \in ℂ$
249	222 245	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to c \in ℂ$
250	248 249	cjsubd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{b - c} = \overline{b} - \overline{c}$
251	1 226 243	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{b} \in C (N)$
252	216 251	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{b} \in F$
253	1 226 245	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{c} \in C (N)$
254	216 253	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{c} \in F$
255	39 214 252 254	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{b} - \overline{c} \in F$
256	250 255	eqeltrd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{b - c} \in F$
257	33 215 247 256	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (b - c) \overline{b - c} \in F$
258	1 226 238	constrconj	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{a} \in C (N)$
259	216 258	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{a} \in F$
260	33 215 259 240	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{a} (d + a) \in F$
261	39 214 257 260	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (b - c) \overline{b - c} - \overline{a} (d + a) \in F$
262	39 214 242 261	subgsubcld	$⊢ (((((((φ \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 (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 F$
263	39 214 236 259	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} - \overline{a} \in F$
264	222 234	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d \in ℂ$
265	222 238	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to a \in ℂ$
266	264 265	cjsubd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d - a} = \overline{d} - \overline{a}$
267	264 265	subcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d - a \in ℂ$
268		simpr1	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to a \neq d$
269	268	necomd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d \neq a$
270	264 265 269	subne0d	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d - a \neq 0$
271	267 270	cjne0d	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d - a} \neq 0$
272	266 271	eqnetrrd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} - \overline{a} \neq 0$
273	36 37 212 262 263 272	sdrgdvcl	$⊢ (((((((φ \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 (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 F$
274		df-neg	$⊢ - \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 - (\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}})$
275	1 226	constr01	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \{0, 1\} \subseteq C (N)$
276	176	a1i	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to 0 \in \{0, 1\}$
277	275 276	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to 0 \in C (N)$
278	216 277	sseldd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to 0 \in F$
279	33 215 237 239	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to d a \in F$
280	33 215 259 279	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{a} d a \in F$
281	33 215 257 237	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (b - c) \overline{b - c} d \in F$
282	39 214 280 281	subgsubcld	$⊢ (((((((φ \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 (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 F$
283	33 215 236 279	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \overline{d} d a \in F$
284	33 215 233 239	subrgmcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (e - f) \overline{e - f} a \in F$
285	39 214 283 284	subgsubcld	$⊢ (((((((φ \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 (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 F$
286	39 214 282 285	subgsubcld	$⊢ (((((((φ \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 (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 F$
287	36 37 212 286 263 272	sdrgdvcl	$⊢ (((((((φ \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 (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 F$
288	39 214 278 287	subgsubcld	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to 0 - (\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 F$
289	274 288	eqeltrid	$⊢ (((((((φ \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 (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 F$
290	213 194 196	sylancl	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to 2 \cdot_{{mulGrp}_{ℂ_{fld}}} X = X^{2}$
291	290	oveq1d	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (2 \cdot_{{mulGrp}_{ℂ_{fld}}} X) + (\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}})$
292		simpr2	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \|X - a\| = \|b - c\|$
293		simpr3	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to \|X - d\| = \|e - f\|$
294		eqid	$⊢ (b - c) \overline{b - c} = (b - c) \overline{b - c}$
295		eqid	$⊢ (e - f) \overline{e - f} = (e - f) \overline{e - f}$
296		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}}$
297		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}}$
298	222 238 243 245 234 217 219 213 268 292 293 294 295 296 297	constrrtcc	$⊢ (((((((φ \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 (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$
299	291 298	eqtrd	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (2 \cdot_{{mulGrp}_{ℂ_{fld}}} X) + (\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$
300	2 3 37 122 8 33 28 123 211 212 213 273 289 299	rtelextdg2	$⊢ (((((((φ \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 (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
301	300	r19.29an	$⊢ ((((((φ \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 \exists f \in C (N) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
302	301	r19.29an	$⊢ (((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land d \in C (N)) \land \exists e \in C (N) \exists f \in C (N) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)) \to (X \in F \lor L [. : .] K = 2)$
303	302	r19.29an	$⊢ ((((φ \land a \in C (N)) \land b \in C (N)) \land c \in C (N)) \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
304	303	r19.29an	$⊢ (((φ \land a \in C (N)) \land b \in C (N)) \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
305	304	r19.29an	$⊢ ((φ \land a \in C (N)) \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
306	305	r19.29an	$⊢ (φ \land \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\|)) \to (X \in F \lor L [. : .] K = 2)$
307	129	simprd	$⊢ φ \to (\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\|))$
308	105 210 306 307	mpjao3dan	$⊢ φ \to (X \in F \lor L [. : .] K = 2)$

Metamath Proof Explorer

Theorem constrelextdg2

Proof