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