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

Metamath Proof Explorer

Theorem constrconj

Proof