constrconj

Description: If a point X of the complex plane is constructible, so is its conjugate ( *X ) . (Proposed by Saveliy Skresanov, 25-Jun-2025.) (Contributed by Thierry Arnoux, 1-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\})$
	constrconj.1	$⊢ φ \to N \in On$
	constrconj.2	$⊢ φ \to X \in C (N)$
Assertion	constrconj	$⊢ φ \to \overline{X} \in C (N)$

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		constrconj.1	$⊢ φ \to N \in On$
3		constrconj.2	$⊢ φ \to X \in C (N)$
4		fveq2	$⊢ m = \emptyset \to C (m) = C (\emptyset)$
5	4	eleq2d	$⊢ m = \emptyset \to (\overline{x} \in C (m) \leftrightarrow \overline{x} \in C (\emptyset))$
6	4 5	raleqbidv	$⊢ m = \emptyset \to (\forall x \in C (m) \overline{x} \in C (m) \leftrightarrow \forall x \in C (\emptyset) \overline{x} \in C (\emptyset))$
7		fveq2	$⊢ m = n \to C (m) = C (n)$
8	7	eleq2d	$⊢ m = n \to (\overline{x} \in C (m) \leftrightarrow \overline{x} \in C (n))$
9	7 8	raleqbidv	$⊢ m = n \to (\forall x \in C (m) \overline{x} \in C (m) \leftrightarrow \forall x \in C (n) \overline{x} \in C (n))$
10		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
11	10	eleq2d	$⊢ m = suc n \to (\overline{x} \in C (m) \leftrightarrow \overline{x} \in C (suc n))$
12	10 11	raleqbidv	$⊢ m = suc n \to (\forall x \in C (m) \overline{x} \in C (m) \leftrightarrow \forall x \in C (suc n) \overline{x} \in C (suc n))$
13		fveq2	$⊢ m = N \to C (m) = C (N)$
14	13	eleq2d	$⊢ m = N \to (\overline{x} \in C (m) \leftrightarrow \overline{x} \in C (N))$
15	13 14	raleqbidv	$⊢ m = N \to (\forall x \in C (m) \overline{x} \in C (m) \leftrightarrow \forall x \in C (N) \overline{x} \in C (N))$
16		simpr	$⊢ (x \in C (\emptyset) \land x = 0) \to x = 0$
17	16	fveq2d	$⊢ (x \in C (\emptyset) \land x = 0) \to \overline{x} = \overline{0}$
18		cj0	$⊢ \overline{0} = 0$
19	17 18	eqtrdi	$⊢ (x \in C (\emptyset) \land x = 0) \to \overline{x} = 0$
20		c0ex	$⊢ 0 \in V$
21	20	prid1	$⊢ 0 \in \{0, 1\}$
22	21	a1i	$⊢ (x \in C (\emptyset) \land x = 0) \to 0 \in \{0, 1\}$
23	19 22	eqeltrd	$⊢ (x \in C (\emptyset) \land x = 0) \to \overline{x} \in \{0, 1\}$
24	1	constr0	$⊢ C (\emptyset) = \{0, 1\}$
25	24	a1i	$⊢ (x \in C (\emptyset) \land x = 0) \to C (\emptyset) = \{0, 1\}$
26	23 25	eleqtrrd	$⊢ (x \in C (\emptyset) \land x = 0) \to \overline{x} \in C (\emptyset)$
27		simpr	$⊢ (x \in C (\emptyset) \land x = 1) \to x = 1$
28	27	fveq2d	$⊢ (x \in C (\emptyset) \land x = 1) \to \overline{x} = \overline{1}$
29		1re	$⊢ 1 \in ℝ$
30		cjre	$⊢ 1 \in ℝ \to \overline{1} = 1$
31	29 30	ax-mp	$⊢ \overline{1} = 1$
32	28 31	eqtrdi	$⊢ (x \in C (\emptyset) \land x = 1) \to \overline{x} = 1$
33		1ex	$⊢ 1 \in V$
34	33	prid2	$⊢ 1 \in \{0, 1\}$
35	34	a1i	$⊢ (x \in C (\emptyset) \land x = 1) \to 1 \in \{0, 1\}$
36	32 35	eqeltrd	$⊢ (x \in C (\emptyset) \land x = 1) \to \overline{x} \in \{0, 1\}$
37	24	a1i	$⊢ (x \in C (\emptyset) \land x = 1) \to C (\emptyset) = \{0, 1\}$
38	36 37	eleqtrrd	$⊢ (x \in C (\emptyset) \land x = 1) \to \overline{x} \in C (\emptyset)$
39	24	eleq2i	$⊢ x \in C (\emptyset) \leftrightarrow x \in \{0, 1\}$
40	39	biimpi	$⊢ x \in C (\emptyset) \to x \in \{0, 1\}$
41		elpri	$⊢ x \in \{0, 1\} \to (x = 0 \lor x = 1)$
42	40 41	syl	$⊢ x \in C (\emptyset) \to (x = 0 \lor x = 1)$
43	26 38 42	mpjaodan	$⊢ x \in C (\emptyset) \to \overline{x} \in C (\emptyset)$
44	43	rgen	$⊢ \forall x \in C (\emptyset) \overline{x} \in C (\emptyset)$
45		simpl	$⊢ (n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \to n \in On$
46		eqid	$⊢ C (n) = C (n)$
47	1 45 46	constrsuc	$⊢ (n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \to (y \in C (suc n) \leftrightarrow (y \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 ℝ (y = a + t (b - a) \land y = 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 ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))))$
48	47	biimpa	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to (y \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 ℝ (y = a + t (b - a) \land y = 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 ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)))$
49	48	simpld	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to y \in ℂ$
50	49	cjcld	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to \overline{y} \in ℂ$
51	48	simprd	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = 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 ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|))$
52		fveq2	$⊢ x = a \to \overline{x} = \overline{a}$
53	52	eleq1d	$⊢ x = a \to (\overline{x} \in C (n) \leftrightarrow \overline{a} \in C (n))$
54		simp-4r	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \forall x \in C (n) \overline{x} \in C (n)$
55		simplr	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to a \in C (n)$
56	53 54 55	rspcdva	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{a} \in C (n)$
57		id	$⊢ g = \overline{a} \to g = \overline{a}$
58		oveq2	$⊢ g = \overline{a} \to h - g = h - \overline{a}$
59	58	oveq2d	$⊢ g = \overline{a} \to t (h - g) = t (h - \overline{a})$
60	57 59	oveq12d	$⊢ g = \overline{a} \to g + t (h - g) = \overline{a} + t (h - \overline{a})$
61	60	eqeq2d	$⊢ g = \overline{a} \to (\overline{y} = g + t (h - g) \leftrightarrow \overline{y} = \overline{a} + t (h - \overline{a}))$
62	58	fveq2d	$⊢ g = \overline{a} \to \overline{h - g} = \overline{h - \overline{a}}$
63	62	oveq1d	$⊢ g = \overline{a} \to \overline{h - g} (j - i) = \overline{h - \overline{a}} (j - i)$
64	63	fveq2d	$⊢ g = \overline{a} \to ℑ (\overline{h - g} (j - i)) = ℑ (\overline{h - \overline{a}} (j - i))$
65	64	neeq1d	$⊢ g = \overline{a} \to (ℑ (\overline{h - g} (j - i)) \neq 0 \leftrightarrow ℑ (\overline{h - \overline{a}} (j - i)) \neq 0)$
66	61 65	3anbi13d	$⊢ g = \overline{a} \to ((\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0) \leftrightarrow (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0))$
67	66	rexbidv	$⊢ g = \overline{a} \to (\exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0) \leftrightarrow \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0))$
68	67	2rexbidv	$⊢ g = \overline{a} \to (\exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0) \leftrightarrow \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0))$
69	68	2rexbidv	$⊢ g = \overline{a} \to (\exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0))$
70	69	adantl	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \land g = \overline{a}) \to (\exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0))$
71		fveq2	$⊢ x = b \to \overline{x} = \overline{b}$
72	71	eleq1d	$⊢ x = b \to (\overline{x} \in C (n) \leftrightarrow \overline{b} \in C (n))$
73		simp-5r	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \forall x \in C (n) \overline{x} \in C (n)$
74		simplr	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to b \in C (n)$
75	72 73 74	rspcdva	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{b} \in C (n)$
76		oveq1	$⊢ h = \overline{b} \to h - \overline{a} = \overline{b} - \overline{a}$
77	76	oveq2d	$⊢ h = \overline{b} \to t (h - \overline{a}) = t (\overline{b} - \overline{a})$
78	77	oveq2d	$⊢ h = \overline{b} \to \overline{a} + t (h - \overline{a}) = \overline{a} + t (\overline{b} - \overline{a})$
79	78	eqeq2d	$⊢ h = \overline{b} \to (\overline{y} = \overline{a} + t (h - \overline{a}) \leftrightarrow \overline{y} = \overline{a} + t (\overline{b} - \overline{a}))$
80	76	fveq2d	$⊢ h = \overline{b} \to \overline{h - \overline{a}} = \overline{\overline{b} - \overline{a}}$
81	80	oveq1d	$⊢ h = \overline{b} \to \overline{h - \overline{a}} (j - i) = \overline{\overline{b} - \overline{a}} (j - i)$
82	81	fveq2d	$⊢ h = \overline{b} \to ℑ (\overline{h - \overline{a}} (j - i)) = ℑ (\overline{\overline{b} - \overline{a}} (j - i))$
83	82	neeq1d	$⊢ h = \overline{b} \to (ℑ (\overline{h - \overline{a}} (j - i)) \neq 0 \leftrightarrow ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0)$
84	79 83	3anbi13d	$⊢ h = \overline{b} \to ((\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0))$
85	84	2rexbidv	$⊢ h = \overline{b} \to (\exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0))$
86	85	2rexbidv	$⊢ h = \overline{b} \to (\exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0))$
87	86	adantl	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \land h = \overline{b}) \to (\exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0))$
88		fveq2	$⊢ x = c \to \overline{x} = \overline{c}$
89	88	eleq1d	$⊢ x = c \to (\overline{x} \in C (n) \leftrightarrow \overline{c} \in C (n))$
90		simp-6r	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \forall x \in C (n) \overline{x} \in C (n)$
91		simplr	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to c \in C (n)$
92	89 90 91	rspcdva	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{c} \in C (n)$
93		id	$⊢ i = \overline{c} \to i = \overline{c}$
94		oveq2	$⊢ i = \overline{c} \to j - i = j - \overline{c}$
95	94	oveq2d	$⊢ i = \overline{c} \to r (j - i) = r (j - \overline{c})$
96	93 95	oveq12d	$⊢ i = \overline{c} \to i + r (j - i) = \overline{c} + r (j - \overline{c})$
97	96	eqeq2d	$⊢ i = \overline{c} \to (\overline{y} = i + r (j - i) \leftrightarrow \overline{y} = \overline{c} + r (j - \overline{c}))$
98	94	oveq2d	$⊢ i = \overline{c} \to \overline{\overline{b} - \overline{a}} (j - i) = \overline{\overline{b} - \overline{a}} (j - \overline{c})$
99	98	fveq2d	$⊢ i = \overline{c} \to ℑ (\overline{\overline{b} - \overline{a}} (j - i)) = ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c}))$
100	99	neeq1d	$⊢ i = \overline{c} \to (ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0 \leftrightarrow ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0)$
101	97 100	3anbi23d	$⊢ i = \overline{c} \to ((\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0))$
102	101	rexbidv	$⊢ i = \overline{c} \to (\exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0))$
103	102	2rexbidv	$⊢ i = \overline{c} \to (\exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0))$
104	103	adantl	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \land i = \overline{c}) \to (\exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0) \leftrightarrow \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0))$
105		fveq2	$⊢ x = d \to \overline{x} = \overline{d}$
106	105	eleq1d	$⊢ x = d \to (\overline{x} \in C (n) \leftrightarrow \overline{d} \in C (n))$
107		simp-7r	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \forall x \in C (n) \overline{x} \in C (n)$
108		simplr	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to d \in C (n)$
109	106 107 108	rspcdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{d} \in C (n)$
110		oveq1	$⊢ j = \overline{d} \to j - \overline{c} = \overline{d} - \overline{c}$
111	110	oveq2d	$⊢ j = \overline{d} \to r (j - \overline{c}) = r (\overline{d} - \overline{c})$
112	111	oveq2d	$⊢ j = \overline{d} \to \overline{c} + r (j - \overline{c}) = \overline{c} + r (\overline{d} - \overline{c})$
113	112	eqeq2d	$⊢ j = \overline{d} \to (\overline{y} = \overline{c} + r (j - \overline{c}) \leftrightarrow \overline{y} = \overline{c} + r (\overline{d} - \overline{c}))$
114	110	oveq2d	$⊢ j = \overline{d} \to \overline{\overline{b} - \overline{a}} (j - \overline{c}) = \overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})$
115	114	fveq2d	$⊢ j = \overline{d} \to ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) = ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c}))$
116	115	neeq1d	$⊢ j = \overline{d} \to (ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0 \leftrightarrow ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0)$
117	113 116	3anbi23d	$⊢ j = \overline{d} \to ((\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
118	117	2rexbidv	$⊢ j = \overline{d} \to (\exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
119	118	adantl	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \land j = \overline{d}) \to (\exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
120		simpr1	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to y = a + t (b - a)$
121	120	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{y} = \overline{a + t (b - a)}$
122		id	$⊢ n \in On \to n \in On$
123	1 122	constrsscn	$⊢ n \in On \to C (n) \subseteq ℂ$
124	123	ad9antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to C (n) \subseteq ℂ$
125		simp-7r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to a \in C (n)$
126	124 125	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to a \in ℂ$
127		simpllr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to t \in ℝ$
128	127	recnd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to t \in ℂ$
129		simp-6r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to b \in C (n)$
130	124 129	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to b \in ℂ$
131	130 126	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to b - a \in ℂ$
132	128 131	mulcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to t (b - a) \in ℂ$
133	126 132	cjaddd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{a + t (b - a)} = \overline{a} + \overline{t (b - a)}$
134	128 131	cjmuld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{t (b - a)} = \overline{t} \overline{b - a}$
135	127	cjred	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{t} = t$
136	130 126	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{b - a} = \overline{b} - \overline{a}$
137	135 136	oveq12d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{t} \overline{b - a} = t (\overline{b} - \overline{a})$
138	134 137	eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{t (b - a)} = t (\overline{b} - \overline{a})$
139	138	oveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{a} + \overline{t (b - a)} = \overline{a} + t (\overline{b} - \overline{a})$
140	121 133 139	3eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{y} = \overline{a} + t (\overline{b} - \overline{a})$
141		simpr2	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to y = c + r (d - c)$
142	141	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{y} = \overline{c + r (d - c)}$
143		simp-5r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to c \in C (n)$
144	124 143	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to c \in ℂ$
145		simplr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to r \in ℝ$
146	145	recnd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to r \in ℂ$
147		simp-4r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to d \in C (n)$
148	124 147	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to d \in ℂ$
149	148 144	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to d - c \in ℂ$
150	146 149	mulcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to r (d - c) \in ℂ$
151	144 150	cjaddd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{c + r (d - c)} = \overline{c} + \overline{r (d - c)}$
152	146 149	cjmuld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{r (d - c)} = \overline{r} \overline{d - c}$
153	145	cjred	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{r} = r$
154	148 144	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{d - c} = \overline{d} - \overline{c}$
155	153 154	oveq12d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{r} \overline{d - c} = r (\overline{d} - \overline{c})$
156	152 155	eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{r (d - c)} = r (\overline{d} - \overline{c})$
157	156	oveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{c} + \overline{r (d - c)} = \overline{c} + r (\overline{d} - \overline{c})$
158	142 151 157	3eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{y} = \overline{c} + r (\overline{d} - \overline{c})$
159	131	cjcjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b - a}} = b - a$
160	159	oveq1d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b - a}} \overline{d - c} = (b - a) \overline{d - c}$
161	131	cjcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{b - a} \in ℂ$
162	161 149	cjmuld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = 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}$
163	130	cjcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{b} \in ℂ$
164	126	cjcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{a} \in ℂ$
165	163 164	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b} - \overline{a}} = \overline{\overline{b}} - \overline{\overline{a}}$
166	130	cjcjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b}} = b$
167	126	cjcjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{a}} = a$
168	166 167	oveq12d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b}} - \overline{\overline{a}} = b - a$
169	165 168	eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b} - \overline{a}} = b - a$
170	154	eqcomd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{d} - \overline{c} = \overline{d - c}$
171	169 170	oveq12d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c}) = (b - a) \overline{d - c}$
172	160 162 171	3eqtr4rd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c}) = \overline{\overline{b - a} (d - c)}$
173	172	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) = ℑ (\overline{\overline{b - a} (d - c)})$
174	161 149	mulcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \overline{b - a} (d - c) \in ℂ$
175	174	imcjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{\overline{b - a} (d - c)}) = - ℑ (\overline{b - a} (d - c))$
176	173 175	eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) = - ℑ (\overline{b - a} (d - c))$
177		simpr3	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{b - a} (d - c)) \neq 0$
178	174	imcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{b - a} (d - c)) \in ℝ$
179	178	recnd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{b - a} (d - c)) \in ℂ$
180	179	negne0bd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to (ℑ (\overline{b - a} (d - c)) \neq 0 \leftrightarrow - ℑ (\overline{b - a} (d - c)) \neq 0)$
181	177 180	mpbid	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to - ℑ (\overline{b - a} (d - c)) \neq 0$
182	176 181	eqnetrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0$
183	140 158 182	3jca	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0)$
184	183	ex	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ) \to ((y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \to (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
185	184	reximdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land t \in ℝ) \to (\exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \to \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
186	185	reximdva	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to (\exists t \in ℝ \exists r \in ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \to \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0))$
187	186	imp	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (\overline{d} - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (\overline{d} - \overline{c})) \neq 0)$
188	109 119 187	rspcedvd	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0)$
189	188	r19.29an	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = \overline{c} + r (j - \overline{c}) \land ℑ (\overline{\overline{b} - \overline{a}} (j - \overline{c})) \neq 0)$
190	92 104 189	rspcedvd	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0)$
191	190	r19.29an	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{\overline{b} - \overline{a}} (j - i)) \neq 0)$
192	75 87 191	rspcedvd	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0)$
193	192	r19.29an	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - \overline{a}} (j - i)) \neq 0)$
194	56 70 193	rspcedvd	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
195	194	r19.29an	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
196		id	$⊢ a = g \to a = g$
197		oveq2	$⊢ a = g \to b - a = b - g$
198	197	oveq2d	$⊢ a = g \to t (b - a) = t (b - g)$
199	196 198	oveq12d	$⊢ a = g \to a + t (b - a) = g + t (b - g)$
200	199	eqeq2d	$⊢ a = g \to (\overline{y} = a + t (b - a) \leftrightarrow \overline{y} = g + t (b - g))$
201	197	fveq2d	$⊢ a = g \to \overline{b - a} = \overline{b - g}$
202	201	oveq1d	$⊢ a = g \to \overline{b - a} (d - c) = \overline{b - g} (d - c)$
203	202	fveq2d	$⊢ a = g \to ℑ (\overline{b - a} (d - c)) = ℑ (\overline{b - g} (d - c))$
204	203	neeq1d	$⊢ a = g \to (ℑ (\overline{b - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - g} (d - c)) \neq 0)$
205	200 204	3anbi13d	$⊢ a = g \to ((\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0))$
206	205	rexbidv	$⊢ a = g \to (\exists r \in ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0))$
207	206	2rexbidv	$⊢ a = g \to (\exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0))$
208	207	2rexbidv	$⊢ a = g \to (\exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0))$
209	208	cbvrexvw	$⊢ \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists g \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0)$
210		oveq1	$⊢ b = h \to b - g = h - g$
211	210	oveq2d	$⊢ b = h \to t (b - g) = t (h - g)$
212	211	oveq2d	$⊢ b = h \to g + t (b - g) = g + t (h - g)$
213	212	eqeq2d	$⊢ b = h \to (\overline{y} = g + t (b - g) \leftrightarrow \overline{y} = g + t (h - g))$
214	210	fveq2d	$⊢ b = h \to \overline{b - g} = \overline{h - g}$
215	214	oveq1d	$⊢ b = h \to \overline{b - g} (d - c) = \overline{h - g} (d - c)$
216	215	fveq2d	$⊢ b = h \to ℑ (\overline{b - g} (d - c)) = ℑ (\overline{h - g} (d - c))$
217	216	neeq1d	$⊢ b = h \to (ℑ (\overline{b - g} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{h - g} (d - c)) \neq 0)$
218	213 217	3anbi13d	$⊢ b = h \to ((\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0))$
219	218	2rexbidv	$⊢ b = h \to (\exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0))$
220	219	2rexbidv	$⊢ b = h \to (\exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0))$
221	220	cbvrexvw	$⊢ \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow \exists h \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0)$
222		id	$⊢ c = i \to c = i$
223		oveq2	$⊢ c = i \to d - c = d - i$
224	223	oveq2d	$⊢ c = i \to r (d - c) = r (d - i)$
225	222 224	oveq12d	$⊢ c = i \to c + r (d - c) = i + r (d - i)$
226	225	eqeq2d	$⊢ c = i \to (\overline{y} = c + r (d - c) \leftrightarrow \overline{y} = i + r (d - i))$
227	223	oveq2d	$⊢ c = i \to \overline{h - g} (d - c) = \overline{h - g} (d - i)$
228	227	fveq2d	$⊢ c = i \to ℑ (\overline{h - g} (d - c)) = ℑ (\overline{h - g} (d - i))$
229	228	neeq1d	$⊢ c = i \to (ℑ (\overline{h - g} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{h - g} (d - i)) \neq 0)$
230	226 229	3anbi23d	$⊢ c = i \to ((\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0))$
231	230	rexbidv	$⊢ c = i \to (\exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0))$
232	231	2rexbidv	$⊢ c = i \to (\exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0))$
233	232	cbvrexvw	$⊢ \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow \exists i \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0)$
234		oveq1	$⊢ d = j \to d - i = j - i$
235	234	oveq2d	$⊢ d = j \to r (d - i) = r (j - i)$
236	235	oveq2d	$⊢ d = j \to i + r (d - i) = i + r (j - i)$
237	236	eqeq2d	$⊢ d = j \to (\overline{y} = i + r (d - i) \leftrightarrow \overline{y} = i + r (j - i))$
238	234	oveq2d	$⊢ d = j \to \overline{h - g} (d - i) = \overline{h - g} (j - i)$
239	238	fveq2d	$⊢ d = j \to ℑ (\overline{h - g} (d - i)) = ℑ (\overline{h - g} (j - i))$
240	239	neeq1d	$⊢ d = j \to (ℑ (\overline{h - g} (d - i)) \neq 0 \leftrightarrow ℑ (\overline{h - g} (j - i)) \neq 0)$
241	237 240	3anbi23d	$⊢ d = j \to ((\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0) \leftrightarrow (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0))$
242	241	2rexbidv	$⊢ d = j \to (\exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0) \leftrightarrow \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0))$
243	242	cbvrexvw	$⊢ \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0) \leftrightarrow \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
244	243	rexbii	$⊢ \exists i \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (d - i) \land ℑ (\overline{h - g} (d - i)) \neq 0) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
245	233 244	bitri	$⊢ \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
246	245	rexbii	$⊢ \exists h \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{h - g} (d - c)) \neq 0) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
247	221 246	bitri	$⊢ \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
248	247	rexbii	$⊢ \exists g \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (b - g) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - g} (d - c)) \neq 0) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
249	209 248	bitri	$⊢ \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists t \in ℝ \exists r \in ℝ (\overline{y} = g + t (h - g) \land \overline{y} = i + r (j - i) \land ℑ (\overline{h - g} (j - i)) \neq 0)$
250	195 249	sylibr	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)) \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0)$
251	250	ex	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0))$
252		simp-4r	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
253		simplr	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to a \in C (n)$
254	53 252 253	rspcdva	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{a} \in C (n)$
255	61	anbi1d	$⊢ g = \overline{a} \to ((\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
256	255	rexbidv	$⊢ g = \overline{a} \to (\exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
257	256	2rexbidv	$⊢ g = \overline{a} \to (\exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
258	257	2rexbidv	$⊢ g = \overline{a} \to (\exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
259	258	adantl	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \land g = \overline{a}) \to (\exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
260		simp-5r	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
261		simplr	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to b \in C (n)$
262	72 260 261	rspcdva	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{b} \in C (n)$
263	79	anbi1d	$⊢ h = \overline{b} \to ((\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
264	263	2rexbidv	$⊢ h = \overline{b} \to (\exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
265	264	2rexbidv	$⊢ h = \overline{b} \to (\exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
266	265	adantl	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \land h = \overline{b}) \to (\exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|))$
267		simp-6r	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
268		simplr	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to c \in C (n)$
269	89 267 268	rspcdva	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{c} \in C (n)$
270		oveq2	$⊢ i = \overline{c} \to \overline{y} - i = \overline{y} - \overline{c}$
271	270	fveq2d	$⊢ i = \overline{c} \to \|\overline{y} - i\| = \|\overline{y} - \overline{c}\|$
272	271	eqeq1d	$⊢ i = \overline{c} \to (\|\overline{y} - i\| = \|k - l\| \leftrightarrow \|\overline{y} - \overline{c}\| = \|k - l\|)$
273	272	anbi2d	$⊢ i = \overline{c} \to ((\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|))$
274	273	rexbidv	$⊢ i = \overline{c} \to (\exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|))$
275	274	2rexbidv	$⊢ i = \overline{c} \to (\exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|))$
276	275	adantl	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \land i = \overline{c}) \to (\exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|) \leftrightarrow \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|))$
277		fveq2	$⊢ x = e \to \overline{x} = \overline{e}$
278	277	eleq1d	$⊢ x = e \to (\overline{x} \in C (n) \leftrightarrow \overline{e} \in C (n))$
279		simp-7r	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
280		simplr	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to e \in C (n)$
281	278 279 280	rspcdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{e} \in C (n)$
282		oveq1	$⊢ k = \overline{e} \to k - l = \overline{e} - l$
283	282	fveq2d	$⊢ k = \overline{e} \to \|k - l\| = \|\overline{e} - l\|$
284	283	eqeq2d	$⊢ k = \overline{e} \to (\|\overline{y} - \overline{c}\| = \|k - l\| \leftrightarrow \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|)$
285	284	anbi2d	$⊢ k = \overline{e} \to ((\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|))$
286	285	2rexbidv	$⊢ k = \overline{e} \to (\exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|) \leftrightarrow \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|))$
287	286	adantl	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \land k = \overline{e}) \to (\exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|) \leftrightarrow \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|))$
288		fveq2	$⊢ x = f \to \overline{x} = \overline{f}$
289	288	eleq1d	$⊢ x = f \to (\overline{x} \in C (n) \leftrightarrow \overline{f} \in C (n))$
290		simp-8r	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
291		simplr	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to f \in C (n)$
292	289 290 291	rspcdva	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{f} \in C (n)$
293		oveq2	$⊢ l = \overline{f} \to \overline{e} - l = \overline{e} - \overline{f}$
294	293	fveq2d	$⊢ l = \overline{f} \to \|\overline{e} - l\| = \|\overline{e} - \overline{f}\|$
295	294	eqeq2d	$⊢ l = \overline{f} \to (\|\overline{y} - \overline{c}\| = \|\overline{e} - l\| \leftrightarrow \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|)$
296	295	anbi2d	$⊢ l = \overline{f} \to ((\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|) \leftrightarrow (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|))$
297	296	rexbidv	$⊢ l = \overline{f} \to (\exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|) \leftrightarrow \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|))$
298	297	adantl	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \land l = \overline{f}) \to (\exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|) \leftrightarrow \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|))$
299		simprl	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to y = a + t (b - a)$
300	299	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{y} = \overline{a + t (b - a)}$
301	123	ad9antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to C (n) \subseteq ℂ$
302		simp-7r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to a \in C (n)$
303	301 302	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to a \in ℂ$
304		simplr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to t \in ℝ$
305	304	recnd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to t \in ℂ$
306		simp-6r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to b \in C (n)$
307	301 306	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to b \in ℂ$
308	307 303	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to b - a \in ℂ$
309	305 308	mulcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to t (b - a) \in ℂ$
310	303 309	cjaddd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{a + t (b - a)} = \overline{a} + \overline{t (b - a)}$
311	305 308	cjmuld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{t (b - a)} = \overline{t} \overline{b - a}$
312	304	cjred	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{t} = t$
313	307 303	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{b - a} = \overline{b} - \overline{a}$
314	312 313	oveq12d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{t} \overline{b - a} = t (\overline{b} - \overline{a})$
315	311 314	eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{t (b - a)} = t (\overline{b} - \overline{a})$
316	315	oveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{a} + \overline{t (b - a)} = \overline{a} + t (\overline{b} - \overline{a})$
317	300 310 316	3eqtrd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{y} = \overline{a} + t (\overline{b} - \overline{a})$
318		simprr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|y - c\| = \|e - f\|$
319	49	ad7antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to y \in ℂ$
320		simp-5r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to c \in C (n)$
321	301 320	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to c \in ℂ$
322	319 321	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to y - c \in ℂ$
323	322	abscjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{y - c}\| = \|y - c\|$
324		simp-4r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to e \in C (n)$
325	301 324	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to e \in ℂ$
326		simpllr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to f \in C (n)$
327	301 326	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to f \in ℂ$
328	325 327	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to e - f \in ℂ$
329	328	abscjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{e - f}\| = \|e - f\|$
330	318 323 329	3eqtr4d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{y - c}\| = \|\overline{e - f}\|$
331	319 321	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{y - c} = \overline{y} - \overline{c}$
332	331	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{y - c}\| = \|\overline{y} - \overline{c}\|$
333	325 327	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \overline{e - f} = \overline{e} - \overline{f}$
334	333	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{e - f}\| = \|\overline{e} - \overline{f}\|$
335	330 332 334	3eqtr3d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|$
336	317 335	jca	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|)$
337	336	ex	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ) \to ((y = a + t (b - a) \land \|y - c\| = \|e - f\|) \to (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|))$
338	337	reximdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land e \in C (n)) \land f \in C (n)) \to (\exists t \in ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \to \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|))$
339	338	imp	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - \overline{f}\|)$
340	292 298 339	rspcedvd	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|)$
341	340	r19.29an	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|\overline{e} - l\|)$
342	281 287 341	rspcedvd	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|)$
343	342	r19.29an	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - \overline{c}\| = \|k - l\|)$
344	269 276 343	rspcedvd	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|)$
345	344	r19.29an	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (\overline{b} - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|)$
346	262 266 345	rspcedvd	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|)$
347	346	r19.29an	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = \overline{a} + t (h - \overline{a}) \land \|\overline{y} - i\| = \|k - l\|)$
348	254 259 347	rspcedvd	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
349	348	r19.29an	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
350	200	anbi1d	$⊢ a = g \to ((\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|))$
351	350	rexbidv	$⊢ a = g \to (\exists t \in ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|))$
352	351	2rexbidv	$⊢ a = g \to (\exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|))$
353	352	2rexbidv	$⊢ a = g \to (\exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|))$
354	353	cbvrexvw	$⊢ \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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists g \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 ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|)$
355	213	anbi1d	$⊢ b = h \to ((\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|))$
356	355	2rexbidv	$⊢ b = h \to (\exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|))$
357	356	2rexbidv	$⊢ b = h \to (\exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|))$
358	357	cbvrexvw	$⊢ \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|)$
359		oveq2	$⊢ c = i \to \overline{y} - c = \overline{y} - i$
360	359	fveq2d	$⊢ c = i \to \|\overline{y} - c\| = \|\overline{y} - i\|$
361	360	eqeq1d	$⊢ c = i \to (\|\overline{y} - c\| = \|e - f\| \leftrightarrow \|\overline{y} - i\| = \|e - f\|)$
362	361	anbi2d	$⊢ c = i \to ((\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|))$
363	362	rexbidv	$⊢ c = i \to (\exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|))$
364	363	2rexbidv	$⊢ c = i \to (\exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|))$
365	364	cbvrexvw	$⊢ \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|)$
366		oveq1	$⊢ e = k \to e - f = k - f$
367	366	fveq2d	$⊢ e = k \to \|e - f\| = \|k - f\|$
368	367	eqeq2d	$⊢ e = k \to (\|\overline{y} - i\| = \|e - f\| \leftrightarrow \|\overline{y} - i\| = \|k - f\|)$
369	368	anbi2d	$⊢ e = k \to ((\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|) \leftrightarrow (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|))$
370	369	2rexbidv	$⊢ e = k \to (\exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|) \leftrightarrow \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|))$
371	370	cbvrexvw	$⊢ \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|) \leftrightarrow \exists k \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|)$
372		oveq2	$⊢ f = l \to k - f = k - l$
373	372	fveq2d	$⊢ f = l \to \|k - f\| = \|k - l\|$
374	373	eqeq2d	$⊢ f = l \to (\|\overline{y} - i\| = \|k - f\| \leftrightarrow \|\overline{y} - i\| = \|k - l\|)$
375	374	anbi2d	$⊢ f = l \to ((\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|) \leftrightarrow (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|))$
376	375	rexbidv	$⊢ f = l \to (\exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|) \leftrightarrow \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|))$
377	376	cbvrexvw	$⊢ \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|) \leftrightarrow \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
378	377	rexbii	$⊢ \exists k \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - f\|) \leftrightarrow \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
379	371 378	bitri	$⊢ \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|) \leftrightarrow \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
380	379	rexbii	$⊢ \exists i \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
381	365 380	bitri	$⊢ \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
382	381	rexbii	$⊢ \exists h \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
383	358 382	bitri	$⊢ \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
384	383	rexbii	$⊢ \exists g \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 ℝ (\overline{y} = g + t (b - g) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
385	354 384	bitri	$⊢ \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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists k \in C (n) \exists l \in C (n) \exists t \in ℝ (\overline{y} = g + t (h - g) \land \|\overline{y} - i\| = \|k - l\|)$
386	349 385	sylibr	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|)) \to \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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|)$
387	386	ex	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to (\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 ℝ (y = a + t (b - a) \land \|y - c\| = \|e - f\|) \to \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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - c\| = \|e - f\|))$
388		simp-4r	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
389		simplr	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to a \in C (n)$
390	53 388 389	rspcdva	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \overline{a} \in C (n)$
391		neeq1	$⊢ g = \overline{a} \to (g \neq j \leftrightarrow \overline{a} \neq j)$
392		oveq2	$⊢ g = \overline{a} \to \overline{y} - g = \overline{y} - \overline{a}$
393	392	fveq2d	$⊢ g = \overline{a} \to \|\overline{y} - g\| = \|\overline{y} - \overline{a}\|$
394	393	eqeq1d	$⊢ g = \overline{a} \to (\|\overline{y} - g\| = \|h - i\| \leftrightarrow \|\overline{y} - \overline{a}\| = \|h - i\|)$
395	391 394	3anbi12d	$⊢ g = \overline{a} \to ((g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
396	395	rexbidv	$⊢ g = \overline{a} \to (\exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
397	396	2rexbidv	$⊢ g = \overline{a} \to (\exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
398	397	2rexbidv	$⊢ g = \overline{a} \to (\exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
399	398	adantl	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \land g = \overline{a}) \to (\exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
400		simp-5r	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
401		simplr	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to b \in C (n)$
402	72 400 401	rspcdva	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \overline{b} \in C (n)$
403		oveq1	$⊢ h = \overline{b} \to h - i = \overline{b} - i$
404	403	fveq2d	$⊢ h = \overline{b} \to \|h - i\| = \|\overline{b} - i\|$
405	404	eqeq2d	$⊢ h = \overline{b} \to (\|\overline{y} - \overline{a}\| = \|h - i\| \leftrightarrow \|\overline{y} - \overline{a}\| = \|\overline{b} - i\|)$
406	405	3anbi2d	$⊢ h = \overline{b} \to ((\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|))$
407	406	2rexbidv	$⊢ h = \overline{b} \to (\exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|))$
408	407	2rexbidv	$⊢ h = \overline{b} \to (\exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|))$
409	408	adantl	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \land h = \overline{b}) \to (\exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|))$
410		simp-6r	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
411		simplr	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to c \in C (n)$
412	89 410 411	rspcdva	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \overline{c} \in C (n)$
413		oveq2	$⊢ i = \overline{c} \to \overline{b} - i = \overline{b} - \overline{c}$
414	413	fveq2d	$⊢ i = \overline{c} \to \|\overline{b} - i\| = \|\overline{b} - \overline{c}\|$
415	414	eqeq2d	$⊢ i = \overline{c} \to (\|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \leftrightarrow \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\|)$
416	415	3anbi2d	$⊢ i = \overline{c} \to ((\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|))$
417	416	rexbidv	$⊢ i = \overline{c} \to (\exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|))$
418	417	2rexbidv	$⊢ i = \overline{c} \to (\exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|))$
419	418	adantl	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \land i = \overline{c}) \to (\exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|))$
420		simp-7r	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \forall x \in C (n) \overline{x} \in C (n)$
421		simplr	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to d \in C (n)$
422	106 420 421	rspcdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \overline{d} \in C (n)$
423		neeq2	$⊢ j = \overline{d} \to (\overline{a} \neq j \leftrightarrow \overline{a} \neq \overline{d})$
424		oveq2	$⊢ j = \overline{d} \to \overline{y} - j = \overline{y} - \overline{d}$
425	424	fveq2d	$⊢ j = \overline{d} \to \|\overline{y} - j\| = \|\overline{y} - \overline{d}\|$
426	425	eqeq1d	$⊢ j = \overline{d} \to (\|\overline{y} - j\| = \|e - f\| \leftrightarrow \|\overline{y} - \overline{d}\| = \|e - f\|)$
427	423 426	3anbi13d	$⊢ j = \overline{d} \to ((\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
428	427	2rexbidv	$⊢ j = \overline{d} \to (\exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
429	428	adantl	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \land j = \overline{d}) \to (\exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
430	123	ad9antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to C (n) \subseteq ℂ$
431		simp-7r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to a \in C (n)$
432	430 431	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to a \in ℂ$
433		simp-4r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to d \in C (n)$
434	430 433	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to d \in ℂ$
435		simpr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to a \neq d$
436		cj11	$⊢ (a \in ℂ \land d \in ℂ) \to (\overline{a} = \overline{d} \leftrightarrow a = d)$
437	436	necon3bid	$⊢ (a \in ℂ \land d \in ℂ) \to (\overline{a} \neq \overline{d} \leftrightarrow a \neq d)$
438	437	biimpar	$⊢ ((a \in ℂ \land d \in ℂ) \land a \neq d) \to \overline{a} \neq \overline{d}$
439	432 434 435 438	syl21anc	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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) \to \overline{a} \neq \overline{d}$
440	439	ex	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to (a \neq d \to \overline{a} \neq \overline{d})$
441		simpr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|y - a\| = \|b - c\|$
442	49	ad7antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to y \in ℂ$
443	123	ad9antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to C (n) \subseteq ℂ$
444		simp-7r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to a \in C (n)$
445	443 444	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to a \in ℂ$
446	442 445	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to y - a \in ℂ$
447	446	abscjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{y - a}\| = \|y - a\|$
448		simp-6r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to b \in C (n)$
449	443 448	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to b \in ℂ$
450		simp-5r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to c \in C (n)$
451	443 450	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to c \in ℂ$
452	449 451	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to b - c \in ℂ$
453	452	abscjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{b - c}\| = \|b - c\|$
454	441 447 453	3eqtr4d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{y - a}\| = \|\overline{b - c}\|$
455	442 445	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \overline{y - a} = \overline{y} - \overline{a}$
456	455	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{y - a}\| = \|\overline{y} - \overline{a}\|$
457	449 451	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \overline{b - c} = \overline{b} - \overline{c}$
458	457	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{b - c}\| = \|\overline{b} - \overline{c}\|$
459	454 456 458	3eqtr3d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\|) \to \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\|$
460	459	ex	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to (\|y - a\| = \|b - c\| \to \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\|)$
461	49	ad7antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to y \in ℂ$
462	123	ad9antr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to C (n) \subseteq ℂ$
463		simp-4r	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to d \in C (n)$
464	462 463	sseldd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to d \in ℂ$
465	461 464	subcld	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to y - d \in ℂ$
466	465	abscjd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to \|\overline{y - d}\| = \|y - d\|$
467	461 464	cjsubd	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to \overline{y - d} = \overline{y} - \overline{d}$
468	467	fveq2d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to \|\overline{y - d}\| = \|\overline{y} - \overline{d}\|$
469		simpr	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to \|y - d\| = \|e - f\|$
470	466 468 469	3eqtr3d	$⊢ (((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - d\| = \|e - f\|) \to \|\overline{y} - \overline{d}\| = \|e - f\|$
471	470	ex	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to (\|y - d\| = \|e - f\| \to \|\overline{y} - \overline{d}\| = \|e - f\|)$
472	440 460 471	3anim123d	$⊢ ((((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \land f \in C (n)) \to ((a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \to (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
473	472	reximdva	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \land e \in C (n)) \to (\exists f \in C (n) (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \to \exists f \in C (n) (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
474	473	reximdva	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \land a \in C (n)) \land b \in C (n)) \land c \in C (n)) \land d \in C (n)) \to (\exists e \in C (n) \exists f \in C (n) (a \neq d \land \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \to \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|))$
475	474	imp	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq \overline{d} \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - \overline{d}\| = \|e - f\|)$
476	422 429 475	rspcedvd	$⊢ (((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|)$
477	476	r19.29an	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - \overline{c}\| \land \|\overline{y} - j\| = \|e - f\|)$
478	412 419 477	rspcedvd	$⊢ ((((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|)$
479	478	r19.29an	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|\overline{b} - i\| \land \|\overline{y} - j\| = \|e - f\|)$
480	402 409 479	rspcedvd	$⊢ (((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
481	480	r19.29an	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (\overline{a} \neq j \land \|\overline{y} - \overline{a}\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
482	390 399 481	rspcedvd	$⊢ ((((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
483	482	r19.29an	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
484		neeq1	$⊢ a = g \to (a \neq d \leftrightarrow g \neq d)$
485		oveq2	$⊢ a = g \to \overline{y} - a = \overline{y} - g$
486	485	fveq2d	$⊢ a = g \to \|\overline{y} - a\| = \|\overline{y} - g\|$
487	486	eqeq1d	$⊢ a = g \to (\|\overline{y} - a\| = \|b - c\| \leftrightarrow \|\overline{y} - g\| = \|b - c\|)$
488	484 487	3anbi12d	$⊢ a = g \to ((a \neq d \land \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
489	488	rexbidv	$⊢ a = g \to (\exists f \in C (n) (a \neq d \land \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
490	489	2rexbidv	$⊢ a = g \to (\exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
491	490	2rexbidv	$⊢ a = g \to (\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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \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) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
492	491	cbvrexvw	$⊢ \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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists g \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) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|)$
493		oveq1	$⊢ b = h \to b - c = h - c$
494	493	fveq2d	$⊢ b = h \to \|b - c\| = \|h - c\|$
495	494	eqeq2d	$⊢ b = h \to (\|\overline{y} - g\| = \|b - c\| \leftrightarrow \|\overline{y} - g\| = \|h - c\|)$
496	495	3anbi2d	$⊢ b = h \to ((g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|))$
497	496	2rexbidv	$⊢ b = h \to (\exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|))$
498	497	2rexbidv	$⊢ b = h \to (\exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|))$
499	498	cbvrexvw	$⊢ \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) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|)$
500		oveq2	$⊢ c = i \to h - c = h - i$
501	500	fveq2d	$⊢ c = i \to \|h - c\| = \|h - i\|$
502	501	eqeq2d	$⊢ c = i \to (\|\overline{y} - g\| = \|h - c\| \leftrightarrow \|\overline{y} - g\| = \|h - i\|)$
503	502	3anbi2d	$⊢ c = i \to ((g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|))$
504	503	rexbidv	$⊢ c = i \to (\exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|))$
505	504	2rexbidv	$⊢ c = i \to (\exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|))$
506	505	cbvrexvw	$⊢ \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|)$
507		neeq2	$⊢ d = j \to (g \neq d \leftrightarrow g \neq j)$
508		oveq2	$⊢ d = j \to \overline{y} - d = \overline{y} - j$
509	508	fveq2d	$⊢ d = j \to \|\overline{y} - d\| = \|\overline{y} - j\|$
510	509	eqeq1d	$⊢ d = j \to (\|\overline{y} - d\| = \|e - f\| \leftrightarrow \|\overline{y} - j\| = \|e - f\|)$
511	507 510	3anbi13d	$⊢ d = j \to ((g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
512	511	2rexbidv	$⊢ d = j \to (\exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|))$
513	512	cbvrexvw	$⊢ \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
514	513	rexbii	$⊢ \exists i \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
515	506 514	bitri	$⊢ \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
516	515	rexbii	$⊢ \exists h \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq d \land \|\overline{y} - g\| = \|h - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
517	499 516	bitri	$⊢ \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) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
518	517	rexbii	$⊢ \exists g \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) (g \neq d \land \|\overline{y} - g\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
519	492 518	bitri	$⊢ \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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|) \leftrightarrow \exists g \in C (n) \exists h \in C (n) \exists i \in C (n) \exists j \in C (n) \exists e \in C (n) \exists f \in C (n) (g \neq j \land \|\overline{y} - g\| = \|h - i\| \land \|\overline{y} - j\| = \|e - f\|)$
520	483 519	sylibr	$⊢ (((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \to \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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|)$
521	520	ex	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to (\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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|) \to \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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
522	251 387 521	3orim123d	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (y = a + t (b - a) \land y = 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 ℝ (y = a + t (b - a) \land \|y - 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 \|y - a\| = \|b - c\| \land \|y - d\| = \|e - f\|)) \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = 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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - 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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|)))$
523	51 522	mpd	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = 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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - 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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))$
524	50 523	jca	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to (\overline{y} \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = 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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - 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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|)))$
525	45	adantr	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to n \in On$
526	1 525 46	constrsuc	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to (\overline{y} \in C (suc n) \leftrightarrow (\overline{y} \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 ℝ (\overline{y} = a + t (b - a) \land \overline{y} = 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 ℝ (\overline{y} = a + t (b - a) \land \|\overline{y} - 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 \|\overline{y} - a\| = \|b - c\| \land \|\overline{y} - d\| = \|e - f\|))))$
527	524 526	mpbird	$⊢ ((n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (suc n)) \to \overline{y} \in C (suc n)$
528	527	ralrimiva	$⊢ (n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \to \forall y \in C (suc n) \overline{y} \in C (suc n)$
529		fveq2	$⊢ x = y \to \overline{x} = \overline{y}$
530	529	eleq1d	$⊢ x = y \to (\overline{x} \in C (suc n) \leftrightarrow \overline{y} \in C (suc n))$
531	530	cbvralvw	$⊢ \forall x \in C (suc n) \overline{x} \in C (suc n) \leftrightarrow \forall y \in C (suc n) \overline{y} \in C (suc n)$
532	528 531	sylibr	$⊢ (n \in On \land \forall x \in C (n) \overline{x} \in C (n)) \to \forall x \in C (suc n) \overline{x} \in C (suc n)$
533	532	ex	$⊢ n \in On \to (\forall x \in C (n) \overline{x} \in C (n) \to \forall x \in C (suc n) \overline{x} \in C (suc n))$
534		simpr	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to y \in C (m)$
535		vex	$⊢ m \in V$
536	535	a1i	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to m \in V$
537		simpll	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to Lim m$
538	1 536 537	constrlim	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to C (m) = ⋃_{z \in m} C (z)$
539	534 538	eleqtrd	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to y \in ⋃_{z \in m} C (z)$
540		eliun	$⊢ y \in ⋃_{z \in m} C (z) \leftrightarrow \exists z \in m y \in C (z)$
541	539 540	sylib	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to \exists z \in m y \in C (z)$
542	529	eleq1d	$⊢ x = y \to (\overline{x} \in C (z) \leftrightarrow \overline{y} \in C (z))$
543		fveq2	$⊢ n = z \to C (n) = C (z)$
544	543	eleq2d	$⊢ n = z \to (\overline{x} \in C (n) \leftrightarrow \overline{x} \in C (z))$
545	543 544	raleqbidv	$⊢ n = z \to (\forall x \in C (n) \overline{x} \in C (n) \leftrightarrow \forall x \in C (z) \overline{x} \in C (z))$
546		simp-4r	$⊢ ((((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \land y \in C (z)) \to \forall n \in m \forall x \in C (n) \overline{x} \in C (n)$
547		simplr	$⊢ ((((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \land y \in C (z)) \to z \in m$
548	545 546 547	rspcdva	$⊢ ((((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \land y \in C (z)) \to \forall x \in C (z) \overline{x} \in C (z)$
549		simpr	$⊢ ((((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \land y \in C (z)) \to y \in C (z)$
550	542 548 549	rspcdva	$⊢ ((((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \land y \in C (z)) \to \overline{y} \in C (z)$
551	550	ex	$⊢ (((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \land z \in m) \to (y \in C (z) \to \overline{y} \in C (z))$
552	551	reximdva	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to (\exists z \in m y \in C (z) \to \exists z \in m \overline{y} \in C (z))$
553	541 552	mpd	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to \exists z \in m \overline{y} \in C (z)$
554		eliun	$⊢ \overline{y} \in ⋃_{z \in m} C (z) \leftrightarrow \exists z \in m \overline{y} \in C (z)$
555	553 554	sylibr	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to \overline{y} \in ⋃_{z \in m} C (z)$
556	555 538	eleqtrrd	$⊢ ((Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \land y \in C (m)) \to \overline{y} \in C (m)$
557	556	ralrimiva	$⊢ (Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \to \forall y \in C (m) \overline{y} \in C (m)$
558	529	eleq1d	$⊢ x = y \to (\overline{x} \in C (m) \leftrightarrow \overline{y} \in C (m))$
559	558	cbvralvw	$⊢ \forall x \in C (m) \overline{x} \in C (m) \leftrightarrow \forall y \in C (m) \overline{y} \in C (m)$
560	557 559	sylibr	$⊢ (Lim m \land \forall n \in m \forall x \in C (n) \overline{x} \in C (n)) \to \forall x \in C (m) \overline{x} \in C (m)$
561	560	ex	$⊢ Lim m \to (\forall n \in m \forall x \in C (n) \overline{x} \in C (n) \to \forall x \in C (m) \overline{x} \in C (m))$
562	6 9 12 15 44 533 561	tfinds	$⊢ N \in On \to \forall x \in C (N) \overline{x} \in C (N)$
563	2 562	syl	$⊢ φ \to \forall x \in C (N) \overline{x} \in C (N)$
564		fveq2	$⊢ x = X \to \overline{x} = \overline{X}$
565	564	eleq1d	$⊢ x = X \to (\overline{x} \in C (N) \leftrightarrow \overline{X} \in C (N))$
566	565	adantl	$⊢ (φ \land x = X) \to (\overline{x} \in C (N) \leftrightarrow \overline{X} \in C (N))$
567	3 566	rspcdv	$⊢ φ \to (\forall x \in C (N) \overline{x} \in C (N) \to \overline{X} \in C (N))$
568	563 567	mpd	$⊢ φ \to \overline{X} \in C (N)$

Metamath Proof Explorer

Theorem constrconj

Proof