Theorem constrext2chn

Description: If a constructible number generates some subfield L of CC , then the degree of the extension of L over QQ is a power of two. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	constrext2chn.q	|- Q = ( CCfld |`s QQ )
	constrext2chn.l	|- L = ( CCfld |`s S )
	constrext2chn.s	|- S = ( CCfld fldGen ( QQ u. { A } ) )
	constrext2chn.a	|- ( ph -> A e. Constr )
Assertion	constrext2chn	|- ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )

Proof

Step	Hyp	Ref	Expression
1		constrext2chn.q	|- Q = ( CCfld |`s QQ )
2		constrext2chn.l	|- L = ( CCfld |`s S )
3		constrext2chn.s	|- S = ( CCfld fldGen ( QQ u. { A } ) )
4		constrext2chn.a	|- ( ph -> A e. Constr )
5		oveq1	|- ( o = t -> ( o x. ( j - i ) ) = ( t x. ( j - i ) ) )
6	5	oveq2d	|- ( o = t -> ( i + ( o x. ( j - i ) ) ) = ( i + ( t x. ( j - i ) ) ) )
7	6	eqeq2d	|- ( o = t -> ( y = ( i + ( o x. ( j - i ) ) ) <-> y = ( i + ( t x. ( j - i ) ) ) ) )
8	7	3anbi1d	|- ( o = t -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) ) )
9		oveq1	|- ( p = r -> ( p x. ( l - k ) ) = ( r x. ( l - k ) ) )
10	9	oveq2d	|- ( p = r -> ( k + ( p x. ( l - k ) ) ) = ( k + ( r x. ( l - k ) ) ) )
11	10	eqeq2d	|- ( p = r -> ( y = ( k + ( p x. ( l - k ) ) ) <-> y = ( k + ( r x. ( l - k ) ) ) ) )
12	11	3anbi2d	|- ( p = r -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) ) )
13	8 12	cbvrex2vw	|- ( E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) )
14	13	2rexbii	|- ( E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. k e. z E. l e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) )
15		id	|- ( k = c -> k = c )
16		oveq2	|- ( k = c -> ( l - k ) = ( l - c ) )
17	16	oveq2d	|- ( k = c -> ( r x. ( l - k ) ) = ( r x. ( l - c ) ) )
18	15 17	oveq12d	|- ( k = c -> ( k + ( r x. ( l - k ) ) ) = ( c + ( r x. ( l - c ) ) ) )
19	18	eqeq2d	|- ( k = c -> ( y = ( k + ( r x. ( l - k ) ) ) <-> y = ( c + ( r x. ( l - c ) ) ) ) )
20	16	oveq2d	|- ( k = c -> ( ( * ` ( j - i ) ) x. ( l - k ) ) = ( ( * ` ( j - i ) ) x. ( l - c ) ) )
21	20	fveq2d	|- ( k = c -> ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) = ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) )
22	21	neeq1d	|- ( k = c -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) )
23	19 22	3anbi23d	|- ( k = c -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) ) )
24	23	2rexbidv	|- ( k = c -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) ) )
25		oveq1	|- ( l = d -> ( l - c ) = ( d - c ) )
26	25	oveq2d	|- ( l = d -> ( r x. ( l - c ) ) = ( r x. ( d - c ) ) )
27	26	oveq2d	|- ( l = d -> ( c + ( r x. ( l - c ) ) ) = ( c + ( r x. ( d - c ) ) ) )
28	27	eqeq2d	|- ( l = d -> ( y = ( c + ( r x. ( l - c ) ) ) <-> y = ( c + ( r x. ( d - c ) ) ) ) )
29	25	oveq2d	|- ( l = d -> ( ( * ` ( j - i ) ) x. ( l - c ) ) = ( ( * ` ( j - i ) ) x. ( d - c ) ) )
30	29	fveq2d	|- ( l = d -> ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) = ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) )
31	30	neeq1d	|- ( l = d -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
32	28 31	3anbi23d	|- ( l = d -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) ) )
33	32	2rexbidv	|- ( l = d -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) ) )
34	24 33	cbvrex2vw	|- ( E. k e. z E. l e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
35	14 34	bitri	|- ( E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
36	35	2rexbii	|- ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
37		oveq2	|- ( q = f -> ( m - q ) = ( m - f ) )
38	37	fveq2d	|- ( q = f -> ( abs ` ( m - q ) ) = ( abs ` ( m - f ) ) )
39	38	eqeq2d	|- ( q = f -> ( ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) <-> ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
40	39	anbi2d	|- ( q = f -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) ) )
41	7	anbi1d	|- ( o = t -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) ) )
42	40 41	cbvrex2vw	|- ( E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
43	42	2rexbii	|- ( E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. k e. z E. m e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
44		oveq2	|- ( k = c -> ( y - k ) = ( y - c ) )
45	44	fveq2d	|- ( k = c -> ( abs ` ( y - k ) ) = ( abs ` ( y - c ) ) )
46	45	eqeq1d	|- ( k = c -> ( ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) <-> ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) )
47	46	anbi2d	|- ( k = c -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) ) )
48	47	2rexbidv	|- ( k = c -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) ) )
49		oveq1	|- ( m = e -> ( m - f ) = ( e - f ) )
50	49	fveq2d	|- ( m = e -> ( abs ` ( m - f ) ) = ( abs ` ( e - f ) ) )
51	50	eqeq2d	|- ( m = e -> ( ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) <-> ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
52	51	anbi2d	|- ( m = e -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
53	52	2rexbidv	|- ( m = e -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
54	48 53	cbvrex2vw	|- ( E. k e. z E. m e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
55	43 54	bitri	|- ( E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
56	55	2rexbii	|- ( E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
57		oveq1	|- ( m = e -> ( m - q ) = ( e - q ) )
58	57	fveq2d	|- ( m = e -> ( abs ` ( m - q ) ) = ( abs ` ( e - q ) ) )
59	58	eqeq2d	|- ( m = e -> ( ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) <-> ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) )
60	59	3anbi3d	|- ( m = e -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) ) )
61		oveq2	|- ( q = f -> ( e - q ) = ( e - f ) )
62	61	fveq2d	|- ( q = f -> ( abs ` ( e - q ) ) = ( abs ` ( e - f ) ) )
63	62	eqeq2d	|- ( q = f -> ( ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) <-> ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
64	63	3anbi3d	|- ( q = f -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
65	60 64	cbvrex2vw	|- ( E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
66	65	2rexbii	|- ( E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. k e. z E. l e. z E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
67		oveq2	|- ( k = c -> ( j - k ) = ( j - c ) )
68	67	fveq2d	|- ( k = c -> ( abs ` ( j - k ) ) = ( abs ` ( j - c ) ) )
69	68	eqeq2d	|- ( k = c -> ( ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) <-> ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) ) )
70	69	3anbi2d	|- ( k = c -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
71	70	2rexbidv	|- ( k = c -> ( E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
72		neeq2	|- ( l = d -> ( i =/= l <-> i =/= d ) )
73		oveq2	|- ( l = d -> ( y - l ) = ( y - d ) )
74	73	fveq2d	|- ( l = d -> ( abs ` ( y - l ) ) = ( abs ` ( y - d ) ) )
75	74	eqeq1d	|- ( l = d -> ( ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
76	72 75	3anbi13d	|- ( l = d -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
77	76	2rexbidv	|- ( l = d -> ( E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
78	71 77	cbvrex2vw	|- ( E. k e. z E. l e. z E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
79	66 78	bitri	|- ( E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
80	79	2rexbii	|- ( E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
81	36 56 80	3orbi123i	|- ( ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) <-> ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
82		id	|- ( i = a -> i = a )
83		oveq2	|- ( i = a -> ( j - i ) = ( j - a ) )
84	83	oveq2d	|- ( i = a -> ( t x. ( j - i ) ) = ( t x. ( j - a ) ) )
85	82 84	oveq12d	|- ( i = a -> ( i + ( t x. ( j - i ) ) ) = ( a + ( t x. ( j - a ) ) ) )
86	85	eqeq2d	|- ( i = a -> ( y = ( i + ( t x. ( j - i ) ) ) <-> y = ( a + ( t x. ( j - a ) ) ) ) )
87	83	fveq2d	|- ( i = a -> ( * ` ( j - i ) ) = ( * ` ( j - a ) ) )
88	87	oveq1d	|- ( i = a -> ( ( * ` ( j - i ) ) x. ( d - c ) ) = ( ( * ` ( j - a ) ) x. ( d - c ) ) )
89	88	fveq2d	|- ( i = a -> ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) )
90	89	neeq1d	|- ( i = a -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) )
91	86 90	3anbi13d	|- ( i = a -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
92	91	2rexbidv	|- ( i = a -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
93	92	2rexbidv	|- ( i = a -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
94		oveq1	|- ( j = b -> ( j - a ) = ( b - a ) )
95	94	oveq2d	|- ( j = b -> ( t x. ( j - a ) ) = ( t x. ( b - a ) ) )
96	95	oveq2d	|- ( j = b -> ( a + ( t x. ( j - a ) ) ) = ( a + ( t x. ( b - a ) ) ) )
97	96	eqeq2d	|- ( j = b -> ( y = ( a + ( t x. ( j - a ) ) ) <-> y = ( a + ( t x. ( b - a ) ) ) ) )
98	94	fveq2d	|- ( j = b -> ( * ` ( j - a ) ) = ( * ` ( b - a ) ) )
99	98	oveq1d	|- ( j = b -> ( ( * ` ( j - a ) ) x. ( d - c ) ) = ( ( * ` ( b - a ) ) x. ( d - c ) ) )
100	99	fveq2d	|- ( j = b -> ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) )
101	100	neeq1d	|- ( j = b -> ( ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
102	97 101	3anbi13d	|- ( j = b -> ( ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
103	102	2rexbidv	|- ( j = b -> ( E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
104	103	2rexbidv	|- ( j = b -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
105	93 104	cbvrex2vw	|- ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
106	86	anbi1d	|- ( i = a -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
107	106	2rexbidv	|- ( i = a -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
108	107	2rexbidv	|- ( i = a -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
109	97	anbi1d	|- ( j = b -> ( ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
110	109	2rexbidv	|- ( j = b -> ( E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
111	110	2rexbidv	|- ( j = b -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
112	108 111	cbvrex2vw	|- ( E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
113		neeq1	|- ( i = a -> ( i =/= d <-> a =/= d ) )
114		oveq2	|- ( i = a -> ( y - i ) = ( y - a ) )
115	114	fveq2d	|- ( i = a -> ( abs ` ( y - i ) ) = ( abs ` ( y - a ) ) )
116	115	eqeq1d	|- ( i = a -> ( ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) <-> ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) ) )
117	113 116	3anbi12d	|- ( i = a -> ( ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
118	117	2rexbidv	|- ( i = a -> ( E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
119	118	2rexbidv	|- ( i = a -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
120		oveq1	|- ( j = b -> ( j - c ) = ( b - c ) )
121	120	fveq2d	|- ( j = b -> ( abs ` ( j - c ) ) = ( abs ` ( b - c ) ) )
122	121	eqeq2d	|- ( j = b -> ( ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) <-> ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) ) )
123	122	3anbi2d	|- ( j = b -> ( ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
124	123	2rexbidv	|- ( j = b -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
125	124	2rexbidv	|- ( j = b -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
126	119 125	cbvrex2vw	|- ( E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
127	105 112 126	3orbi123i	|- ( ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
128	81 127	bitri	|- ( ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
129	128	rabbii	|- { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } = { y e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) }
130		eqeq1	|- ( y = x -> ( y = ( a + ( t x. ( b - a ) ) ) <-> x = ( a + ( t x. ( b - a ) ) ) ) )
131		eqeq1	|- ( y = x -> ( y = ( c + ( r x. ( d - c ) ) ) <-> x = ( c + ( r x. ( d - c ) ) ) ) )
132		biidd	|- ( y = x -> ( ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
133	130 131 132	3anbi123d	|- ( y = x -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
134	133	2rexbidv	|- ( y = x -> ( E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
135	134	2rexbidv	|- ( y = x -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
136	135	2rexbidv	|- ( y = x -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
137		oveq1	|- ( y = x -> ( y - c ) = ( x - c ) )
138	137	fveq2d	|- ( y = x -> ( abs ` ( y - c ) ) = ( abs ` ( x - c ) ) )
139	138	eqeq1d	|- ( y = x -> ( ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) )
140	130 139	anbi12d	|- ( y = x -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
141	140	2rexbidv	|- ( y = x -> ( E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
142	141	2rexbidv	|- ( y = x -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
143	142	2rexbidv	|- ( y = x -> ( E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
144		biidd	|- ( y = x -> ( a =/= d <-> a =/= d ) )
145		oveq1	|- ( y = x -> ( y - a ) = ( x - a ) )
146	145	fveq2d	|- ( y = x -> ( abs ` ( y - a ) ) = ( abs ` ( x - a ) ) )
147	146	eqeq1d	|- ( y = x -> ( ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) <-> ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) ) )
148		oveq1	|- ( y = x -> ( y - d ) = ( x - d ) )
149	148	fveq2d	|- ( y = x -> ( abs ` ( y - d ) ) = ( abs ` ( x - d ) ) )
150	149	eqeq1d	|- ( y = x -> ( ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) )
151	144 147 150	3anbi123d	|- ( y = x -> ( ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
152	151	2rexbidv	|- ( y = x -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
153	152	2rexbidv	|- ( y = x -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
154	153	2rexbidv	|- ( y = x -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
155	136 143 154	3orbi123d	|- ( y = x -> ( ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
156	155	cbvrabv	|- { y e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) } = { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
157	129 156	eqtri	|- { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } = { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
158	157	mpteq2i	|- ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( z e. _V |-> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
159		elequ2	|- ( z = s -> ( a e. z <-> a e. s ) )
160		elequ2	|- ( z = s -> ( b e. z <-> b e. s ) )
161		elequ2	|- ( z = s -> ( c e. z <-> c e. s ) )
162		rexeq	|- ( z = s -> ( E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
163	161 162	anbi12d	|- ( z = s -> ( ( c e. z /\ E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( c e. s /\ E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
164	163	rexbidv2	|- ( z = s -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
165	160 164	anbi12d	|- ( z = s -> ( ( b e. z /\ E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( b e. s /\ E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
166	165	rexbidv2	|- ( z = s -> ( E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
167	159 166	anbi12d	|- ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
168	167	rexbidv2	|- ( z = s -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
169		elequ2	|- ( z = s -> ( e e. z <-> e e. s ) )
170		rexeq	|- ( z = s -> ( E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
171	169 170	anbi12d	|- ( z = s -> ( ( e e. z /\ E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( e e. s /\ E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
172	171	rexbidv2	|- ( z = s -> ( E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
173	161 172	anbi12d	|- ( z = s -> ( ( c e. z /\ E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( c e. s /\ E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
174	173	rexbidv2	|- ( z = s -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
175	160 174	anbi12d	|- ( z = s -> ( ( b e. z /\ E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( b e. s /\ E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
176	175	rexbidv2	|- ( z = s -> ( E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
177	159 176	anbi12d	|- ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
178	177	rexbidv2	|- ( z = s -> ( E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
179		elequ2	|- ( z = s -> ( d e. z <-> d e. s ) )
180		rexeq	|- ( z = s -> ( E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
181	169 180	anbi12d	|- ( z = s -> ( ( e e. z /\ E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( e e. s /\ E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
182	181	rexbidv2	|- ( z = s -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
183	179 182	anbi12d	|- ( z = s -> ( ( d e. z /\ E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( d e. s /\ E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
184	183	rexbidv2	|- ( z = s -> ( E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
185	161 184	anbi12d	|- ( z = s -> ( ( c e. z /\ E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( c e. s /\ E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
186	185	rexbidv2	|- ( z = s -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
187	160 186	anbi12d	|- ( z = s -> ( ( b e. z /\ E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( b e. s /\ E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
188	187	rexbidv2	|- ( z = s -> ( E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
189	159 188	anbi12d	|- ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
190	189	rexbidv2	|- ( z = s -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
191	168 178 190	3orbi123d	|- ( z = s -> ( ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
192	191	rabbidv	|- ( z = s -> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } = { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
193	192	cbvmptv	|- ( z e. _V |-> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
194	158 193	eqtri	|- ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
195		rdgeq1	|- ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) -> rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } ) )
196	194 195	ax-mp	|- rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
197		eqid	|- ( CCfld |`s e ) = ( CCfld |`s e )
198		eqid	|- ( CCfld |`s f ) = ( CCfld |`s f )
199		oveq2	|- ( h = e -> ( CCfld |`s h ) = ( CCfld |`s e ) )
200	199	adantl	|- ( ( g = f /\ h = e ) -> ( CCfld |`s h ) = ( CCfld |`s e ) )
201		oveq2	|- ( g = f -> ( CCfld |`s g ) = ( CCfld |`s f ) )
202	201	adantr	|- ( ( g = f /\ h = e ) -> ( CCfld |`s g ) = ( CCfld |`s f ) )
203	200 202	breq12d	|- ( ( g = f /\ h = e ) -> ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) <-> ( CCfld |`s e ) /FldExt ( CCfld |`s f ) ) )
204	200 202	oveq12d	|- ( ( g = f /\ h = e ) -> ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) )
205	204	eqeq1d	|- ( ( g = f /\ h = e ) -> ( ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 <-> ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) )
206	203 205	anbi12d	|- ( ( g = f /\ h = e ) -> ( ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) /\ ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 ) <-> ( ( CCfld |`s e ) /FldExt ( CCfld |`s f ) /\ ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) ) )
207	206	cbvopabv	|- { <. g , h >. | ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) /\ ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 ) } = { <. f , e >. | ( ( CCfld |`s e ) /FldExt ( CCfld |`s f ) /\ ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) }
208		peano1	|- (/) e. _om
209	208	a1i	|- ( ph -> (/) e. _om )
210	3	oveq2i	|- ( CCfld |`s S ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
211	2 210	eqtri	|- L = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
212	196 197 198 207 209 1 211 4	constrext2chnlem	|- ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )