Metamath Proof Explorer

Theorem 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 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 } )
constrconj.1 
|- ( ph -> N e. On )
constrconj.2 
|- ( ph -> X e. ( C ` N ) )
Assertion constrconj 
|- ( ph -> ( * ` X ) e. ( C ` N ) )

Proof

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