Metamath Proof Explorer

Theorem constrfin

Description: Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-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 } )
constrfin.1 
|- ( ph -> N e. _om )
Assertion constrfin 
|- ( ph -> ( C ` N ) e. Fin )

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 constrfin.1 
 |-  ( ph -> N e. _om )
3 fveq2 
 |-  ( m = (/) -> ( C ` m ) = ( C ` (/) ) )
4 3 eleq1d 
 |-  ( m = (/) -> ( ( C ` m ) e. Fin <-> ( C ` (/) ) e. Fin ) )
5 fveq2 
 |-  ( m = n -> ( C ` m ) = ( C ` n ) )
6 5 eleq1d 
 |-  ( m = n -> ( ( C ` m ) e. Fin <-> ( C ` n ) e. Fin ) )
7 fveq2 
 |-  ( m = suc n -> ( C ` m ) = ( C ` suc n ) )
8 7 eleq1d 
 |-  ( m = suc n -> ( ( C ` m ) e. Fin <-> ( C ` suc n ) e. Fin ) )
9 fveq2 
 |-  ( m = N -> ( C ` m ) = ( C ` N ) )
10 9 eleq1d 
 |-  ( m = N -> ( ( C ` m ) e. Fin <-> ( C ` N ) e. Fin ) )
11 1 constr0 
 |-  ( C ` (/) ) = { 0 , 1 }
12 prfi 
 |-  { 0 , 1 } e. Fin
13 11 12 eqeltri 
 |-  ( C ` (/) ) e. Fin
14 nfv 
 |-  F/ x ( n e. _om /\ ( C ` n ) e. Fin )
15 nfcv 
 |-  F/_ x ( C ` suc n )
16 nfrab1 
 |-  F/_ x { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
17 nnon 
 |-  ( n e. _om -> n e. On )
18 17 adantr 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> n e. On )
19 eqid 
 |-  ( C ` n ) = ( C ` n )
20 1 18 19 constrsuc 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( x e. ( C ` suc n ) <-> ( x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) ) )
21 rabid 
 |-  ( x e. { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } <-> ( x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
22 20 21 bitr4di 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( x e. ( C ` suc n ) <-> x e. { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) )
23 14 15 16 22 eqrd 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( C ` suc n ) = { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
24 3unrab 
 |-  ( ( { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } u. { x e. CC | 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } ) u. { x e. CC | 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } ) = { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
25 23 24 eqtr4di 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( C ` suc n ) = ( ( { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } u. { x e. CC | 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } ) u. { x e. CC | 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } ) )
26 simpr 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( C ` n ) e. Fin )
27 26 adantr 
 |-  ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) -> ( C ` n ) e. Fin )
28 27 adantr 
 |-  ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) -> ( C ` n ) e. Fin )
29 28 adantr 
 |-  ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) -> ( C ` n ) e. Fin )
30 snfi 
 |-  { ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) } e. Fin
31 30 a1i 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> { ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) } e. Fin )
32 1 17 constrsscn 
 |-  ( n e. _om -> ( C ` n ) C_ CC )
33 32 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> ( C ` n ) C_ CC )
34 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> a e. ( C ` n ) )
35 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> b e. ( C ` n ) )
36 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> c e. ( C ` n ) )
37 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> d e. ( C ` n ) )
38 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> t e. RR )
39 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> r e. RR )
40 simpr1 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> x = ( a + ( t x. ( b - a ) ) ) )
41 simpr2 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> x = ( c + ( r x. ( d - c ) ) ) )
42 simpr3 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 )
43 eqid 
 |-  ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) )
44 33 34 35 36 37 38 39 40 41 42 43 constrrtll 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ t e. RR ) /\ r e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) )
45 44 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ 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 ) ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) )
46 45 r19.29an 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) /\ 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 ) ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) )
47 46 ex 
 |-  ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ x e. CC ) -> ( 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 ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) ) )
48 47 ralrimiva 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> A. x e. CC ( 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 ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) ) )
49 rabsssn 
 |-  ( { x e. CC | E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } C_ { ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) } <-> A. x e. CC ( 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 ) -> x = ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) ) )
50 48 49 sylibr 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> { x e. CC | E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } C_ { ( a + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) } )
51 31 50 ssfid 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> { x e. CC | 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. Fin )
52 29 51 rabrexfi 
 |-  ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) -> { x e. CC | E. d e. ( C ` n ) 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. Fin )
53 28 52 rabrexfi 
 |-  ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) -> { x e. CC | E. c e. ( C ` n ) E. d e. ( C ` n ) 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. Fin )
54 27 53 rabrexfi 
 |-  ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) -> { x e. CC | E. b e. ( C ` n ) E. c e. ( C ` n ) E. d e. ( C ` n ) 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. Fin )
55 26 54 rabrexfi 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } e. Fin )
56 29 adantr 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) -> ( C ` n ) e. Fin )
57 snfi 
 |-  { a } e. Fin
58 57 a1i 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) -> { a } e. Fin )
59 32 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( C ` n ) C_ CC )
60 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> a e. ( C ` n ) )
61 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> b e. ( C ` n ) )
62 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> c e. ( C ` n ) )
63 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> e e. ( C ` n ) )
64 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> f e. ( C ` n ) )
65 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> t e. RR )
66 simprl 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> x = ( a + ( t x. ( b - a ) ) ) )
67 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) )
68 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> a = b )
69 59 60 61 62 63 64 65 66 67 68 constrrtlc2 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> x = a )
70 69 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) /\ E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> x = a )
71 70 ex 
 |-  ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) /\ x e. CC ) -> ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> x = a ) )
72 71 ralrimiva 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) -> A. x e. CC ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> x = a ) )
73 rabsssn 
 |-  ( { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } C_ { a } <-> A. x e. CC ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> x = a ) )
74 72 73 sylibr 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) -> { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } C_ { a } )
75 58 74 ssfid 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a = b ) -> { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
76 prfi 
 |-  { ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } e. Fin
77 76 a1i 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) -> { ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } e. Fin )
78 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> x e. CC )
79 1cnd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> 1 e. CC )
80 ax-1ne0 
 |-  1 =/= 0
81 80 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> 1 =/= 0 )
82 32 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( C ` n ) C_ CC )
83 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> a e. ( C ` n ) )
84 82 83 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> a e. CC )
85 84 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` a ) e. CC )
86 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> b e. ( C ` n ) )
87 82 86 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> b e. CC )
88 87 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` b ) e. CC )
89 88 85 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` b ) - ( * ` a ) ) e. CC )
90 87 84 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( b - a ) e. CC )
91 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> a =/= b )
92 91 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> b =/= a )
93 87 84 92 subne0d 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( b - a ) =/= 0 )
94 89 90 93 divcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) e. CC )
95 84 94 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. CC )
96 85 95 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) e. CC )
97 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> c e. ( C ` n ) )
98 82 97 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> c e. CC )
99 98 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` c ) e. CC )
100 96 99 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) e. CC )
101 98 94 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. CC )
102 100 101 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) e. CC )
103 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> e e. ( C ` n ) )
104 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> f e. ( C ` n ) )
105 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> t e. RR )
106 simprl 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> x = ( a + ( t x. ( b - a ) ) ) )
107 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) )
108 eqid 
 |-  ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) = ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) )
109 eqid 
 |-  ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) = ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) )
110 eqid 
 |-  ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) = ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) )
111 82 83 86 97 103 104 105 106 107 108 109 110 91 constrrtlc1 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( x ^ 2 ) + ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) x. x ) + ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) = 0 /\ ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) =/= 0 ) )
112 111 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) =/= 0 )
113 102 94 112 divcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. CC )
114 98 100 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) e. CC )
115 82 103 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> e e. CC )
116 82 104 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> f e. CC )
117 115 116 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( e - f ) e. CC )
118 115 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` e ) e. CC )
119 116 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` f ) e. CC )
120 118 119 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` e ) - ( * ` f ) ) e. CC )
121 117 120 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) e. CC )
122 114 121 addcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) e. CC )
123 122 negcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) e. CC )
124 123 94 112 divcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. CC )
125 78 sqcld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( x ^ 2 ) e. CC )
126 125 mullidd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( 1 x. ( x ^ 2 ) ) = ( x ^ 2 ) )
127 126 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 1 x. ( x ^ 2 ) ) + ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) x. x ) + ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) = ( ( x ^ 2 ) + ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) x. x ) + ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) )
128 111 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( x ^ 2 ) + ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) x. x ) + ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) = 0 )
129 127 128 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 1 x. ( x ^ 2 ) ) + ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) x. x ) + ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) = 0 )
130 78 79 81 113 124 129 quad3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ t e. RR ) /\ ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) )
131 130 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) /\ E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) )
132 131 ex 
 |-  ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) /\ x e. CC ) -> ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
133 132 ralrimiva 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) -> A. x e. CC ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
134 rabsspr 
 |-  ( { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } C_ { ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } <-> A. x e. CC ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
135 133 134 sylibr 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) -> { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } C_ { ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } )
136 77 135 ssfid 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ a =/= b ) -> { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
137 exmidne 
 |-  ( a = b \/ a =/= b )
138 137 a1i 
 |-  ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) -> ( a = b \/ a =/= b ) )
139 75 136 138 mpjaodan 
 |-  ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) -> { x e. CC | E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
140 56 139 rabrexfi 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ e e. ( C ` n ) ) -> { x e. CC | E. f e. ( C ` n ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
141 29 140 rabrexfi 
 |-  ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) -> { x e. CC | E. e e. ( C ` n ) E. f e. ( C ` n ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
142 28 141 rabrexfi 
 |-  ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) -> { x e. CC | E. c e. ( C ` n ) E. e e. ( C ` n ) E. f e. ( C ` n ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
143 27 142 rabrexfi 
 |-  ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) -> { x e. CC | E. b e. ( C ` n ) E. c e. ( C ` n ) E. e e. ( C ` n ) E. f e. ( C ` n ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
144 26 143 rabrexfi 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> { x e. CC | 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
145 55 144 unfid 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } u. { x e. CC | 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } ) e. Fin )
146 29 adantr 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> ( C ` n ) e. Fin )
147 146 adantr 
 |-  ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) -> ( C ` n ) e. Fin )
148 prfi 
 |-  { ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } e. Fin
149 148 a1i 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) -> { ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } e. Fin )
150 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> x e. CC )
151 1cnd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> 1 e. CC )
152 80 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> 1 =/= 0 )
153 32 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( C ` n ) C_ CC )
154 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> e e. ( C ` n ) )
155 153 154 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> e e. CC )
156 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> f e. ( C ` n ) )
157 153 156 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> f e. CC )
158 155 157 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( e - f ) e. CC )
159 158 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( e - f ) ) e. CC )
160 158 159 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( e - f ) x. ( * ` ( e - f ) ) ) e. CC )
161 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> d e. ( C ` n ) )
162 153 161 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> d e. CC )
163 162 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` d ) e. CC )
164 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> a e. ( C ` n ) )
165 153 164 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> a e. CC )
166 162 165 addcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d + a ) e. CC )
167 163 166 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) x. ( d + a ) ) e. CC )
168 160 167 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) e. CC )
169 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> b e. ( C ` n ) )
170 153 169 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> b e. CC )
171 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> c e. ( C ` n ) )
172 153 171 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> c e. CC )
173 170 172 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( b - c ) e. CC )
174 173 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( b - c ) ) e. CC )
175 173 174 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( b - c ) x. ( * ` ( b - c ) ) ) e. CC )
176 165 cjcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` a ) e. CC )
177 176 166 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` a ) x. ( d + a ) ) e. CC )
178 175 177 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) e. CC )
179 168 178 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) e. CC )
180 163 176 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) - ( * ` a ) ) e. CC )
181 162 165 cjsubd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( d - a ) ) = ( ( * ` d ) - ( * ` a ) ) )
182 162 165 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d - a ) e. CC )
183 simpr1 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> a =/= d )
184 183 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> d =/= a )
185 162 165 184 subne0d 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d - a ) =/= 0 )
186 182 185 cjne0d 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( d - a ) ) =/= 0 )
187 181 186 eqnetrrd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) - ( * ` a ) ) =/= 0 )
188 179 180 187 divcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) e. CC )
189 162 165 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d x. a ) e. CC )
190 176 189 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` a ) x. ( d x. a ) ) e. CC )
191 175 162 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) e. CC )
192 190 191 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) e. CC )
193 163 189 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) x. ( d x. a ) ) e. CC )
194 160 165 mulcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) e. CC )
195 193 194 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) e. CC )
196 192 195 subcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) e. CC )
197 196 180 187 divcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) e. CC )
198 197 negcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) e. CC )
199 150 sqcld 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( x ^ 2 ) e. CC )
200 199 mullidd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( 1 x. ( x ^ 2 ) ) = ( x ^ 2 ) )
201 200 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 1 x. ( x ^ 2 ) ) + ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) x. x ) + -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) = ( ( x ^ 2 ) + ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) x. x ) + -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) )
202 simpr2 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) )
203 simpr3 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) )
204 eqid 
 |-  ( ( b - c ) x. ( * ` ( b - c ) ) ) = ( ( b - c ) x. ( * ` ( b - c ) ) )
205 eqid 
 |-  ( ( e - f ) x. ( * ` ( e - f ) ) ) = ( ( e - f ) x. ( * ` ( e - f ) ) )
206 eqid 
 |-  ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) = ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) )
207 eqid 
 |-  -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) = -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) )
208 153 164 169 171 161 154 156 150 183 202 203 204 205 206 207 constrrtcc 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( x ^ 2 ) + ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) x. x ) + -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) = 0 )
209 201 208 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 1 x. ( x ^ 2 ) ) + ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) x. x ) + -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) = 0 )
210 150 151 152 188 198 209 quad3d 
 |-  ( ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) /\ ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) )
211 210 ex 
 |-  ( ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) /\ x e. CC ) -> ( ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
212 211 ralrimiva 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ 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. x e. CC ( ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
213 rabsspr 
 |-  ( { x e. CC | ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } C_ { ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } <-> A. x e. CC ( ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) -> ( x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) \/ x = ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) ) ) )
214 212 213 sylibr 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) -> { x e. CC | ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } C_ { ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) + ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) , ( ( -u ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) - ( sqrt ` ( ( ( ( ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ^ 2 ) - ( 4 x. ( 1 x. -u ( ( ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) - ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) ) / ( ( * ` d ) - ( * ` a ) ) ) ) ) ) ) ) / ( 2 x. 1 ) ) } )
215 149 214 ssfid 
 |-  ( ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) /\ f e. ( C ` n ) ) -> { x e. CC | ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
216 147 215 rabrexfi 
 |-  ( ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) /\ e e. ( C ` n ) ) -> { x e. CC | E. f e. ( C ` n ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
217 146 216 rabrexfi 
 |-  ( ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) /\ d e. ( C ` n ) ) -> { x e. CC | E. e e. ( C ` n ) E. f e. ( C ` n ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
218 29 217 rabrexfi 
 |-  ( ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) /\ c e. ( C ` n ) ) -> { x e. CC | E. d e. ( C ` n ) E. e e. ( C ` n ) E. f e. ( C ` n ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
219 28 218 rabrexfi 
 |-  ( ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) /\ b e. ( C ` n ) ) -> { x e. CC | E. c e. ( C ` n ) E. d e. ( C ` n ) E. e e. ( C ` n ) E. f e. ( C ` n ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
220 27 219 rabrexfi 
 |-  ( ( ( n e. _om /\ ( C ` n ) e. Fin ) /\ a e. ( C ` n ) ) -> { x e. CC | 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
221 26 220 rabrexfi 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> { x e. CC | 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } e. Fin )
222 145 221 unfid 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( ( { x 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) } u. { x e. CC | 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 ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) } ) u. { x e. CC | 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 ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) } ) e. Fin )
223 25 222 eqeltrd 
 |-  ( ( n e. _om /\ ( C ` n ) e. Fin ) -> ( C ` suc n ) e. Fin )
224 223 ex 
 |-  ( n e. _om -> ( ( C ` n ) e. Fin -> ( C ` suc n ) e. Fin ) )
225 4 6 8 10 13 224 finds 
 |-  ( N e. _om -> ( C ` N ) e. Fin )
226 2 225 syl 
 |-  ( ph -> ( C ` N ) e. Fin )