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		0elpr01	$⊢ 0 \in \{0, 1\}$
176	175	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\}$
177	174 176	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)$
178	133 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 F$
179	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$
180	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$
181	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$
182	39 132 180 181	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$
183	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)$
184	133 183	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$
185	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)$
186	133 185	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$
187	39 132 184 186	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$
188	33 138 182 187	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$
189	28 132 179 188	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$
190	39 132 178 189	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$
191	173 190	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$
192	36 37 126 191 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$
193		2nn0	$⊢ 2 \in ℕ_{0}$
194	193	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}$
195		cnfldexp	$⊢ (X \in ℂ \land 2 \in ℕ_{0}) \to 2 \cdot_{{mulGrp}_{ℂ_{fld}}} X = X^{2}$
196	131 194 195	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}$
197	196	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}})$
198	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$
199	197 198	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$
200	2 3 37 122 8 33 28 123 125 126 131 172 192 199	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)$
201		exmidne	$⊢ (a = b \lor a \neq b)$
202	201	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)$
203	121 200 202	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)$
204	203	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)$
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 \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)$
206	205	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)$
207	206	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)$
208	207	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)$
209	208	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)$
210	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$
211	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})$
212	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 ℂ$
213	211 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})$
214	211 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})$
215	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$
216		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)$
217	215 216	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$
218		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)$
219	215 218	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$
220	39 213 217 219	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$
221	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 ℂ$
222	221 216	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 ℂ$
223	221 218	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 ℂ$
224	222 223	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}$
225	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$
226	1 225 216	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)$
227	215 226	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$
228	1 225 218	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)$
229	215 228	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$
230	39 213 227 229	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$
231	224 230	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$
232	33 214 220 231	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$
233		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)$
234	1 225 233	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)$
235	215 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 \overline{d} \in F$
236	215 233	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$
237		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)$
238	215 237	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$
239	28 213 236 238	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$
240	33 214 235 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 \overline{d} (d + a) \in F$
241	39 213 232 240	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$
242		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)$
243	215 242	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$
244		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)$
245	215 244	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$
246	39 213 243 245	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$
247	221 242	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 ℂ$
248	221 244	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 ℂ$
249	247 248	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}$
250	1 225 242	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)$
251	215 250	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$
252	1 225 244	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)$
253	215 252	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$
254	39 213 251 253	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$
255	249 254	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$
256	33 214 246 255	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$
257	1 225 237	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)$
258	215 257	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$
259	33 214 258 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 \overline{a} (d + a) \in F$
260	39 213 256 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 (b - c) \overline{b - c} - \overline{a} (d + a) \in F$
261	39 213 241 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 (e - f) \overline{e - f} - \overline{d} (d + a) - ((b - c) \overline{b - c} - \overline{a} (d + a)) \in F$
262	39 213 235 258	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$
263	221 233	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 ℂ$
264	221 237	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 ℂ$
265	263 264	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}$
266	263 264	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 ℂ$
267		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$
268	267	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$
269	263 264 268	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$
270	266 269	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$
271	265 270	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$
272	36 37 211 261 262 271	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$
273		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}})$
274	1 225	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)$
275	175	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\}$
276	274 275	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)$
277	215 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 F$
278	33 214 236 238	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$
279	33 214 258 278	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$
280	33 214 256 236	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$
281	39 213 279 280	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$
282	33 214 235 278	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$
283	33 214 232 238	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$
284	39 213 282 283	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$
285	39 213 281 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{a} d a - (b - c) \overline{b - c} d - (\overline{d} d a - (e - f) \overline{e - f} a) \in F$
286	36 37 211 285 262 271	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$
287	39 213 277 286	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$
288	273 287	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$
289	212 193 195	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}$
290	289	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}})$
291		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\|$
292		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\|$
293		eqid	$⊢ (b - c) \overline{b - c} = (b - c) \overline{b - c}$
294		eqid	$⊢ (e - f) \overline{e - f} = (e - f) \overline{e - f}$
295		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}}$
296		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}}$
297	221 237 242 244 233 216 218 212 267 291 292 293 294 295 296	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$
298	290 297	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$
299	2 3 37 122 8 33 28 123 210 211 212 272 288 298	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)$
300	299	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)$
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 \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)$
302	301	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)$
303	302	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)$
304	303	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)$
305	304	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)$
306	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\|))$
307	105 209 305 306	mpjao3dan	$⊢ φ \to (X \in F \lor L [. : .] K = 2)$

Metamath Proof Explorer

Theorem constrelextdg2

Proof