Metamath Proof Explorer

Theorem constrelextdg2

Description: If the N -th step ( CN ) of the construction of constuctible numbers is included in a subfield F of the complex numbers, then any element X of the next step ( Csuc N ) is either in F or in a quadratic extension of F . (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 } )
constrelextdg2.k 
|- K = ( CCfld |`s F )
constrelextdg2.l 
|- L = ( CCfld |`s ( CCfld fldGen ( F u. { X } ) ) )
constrelextdg2.f 
|- ( ph -> F e. ( SubDRing ` CCfld ) )
constrelextdg2.n 
|- ( ph -> N e. On )
constrelextdg2.1 
|- ( ph -> ( C ` N ) C_ F )
constrelextdg2.x 
|- ( ph -> X e. ( C ` suc N ) )
Assertion constrelextdg2 
|- ( ph -> ( X e. F \/ ( L [:] K ) = 2 ) )

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 constrelextdg2.k 
 |-  K = ( CCfld |`s F )
3 constrelextdg2.l 
 |-  L = ( CCfld |`s ( CCfld fldGen ( F u. { X } ) ) )
4 constrelextdg2.f 
 |-  ( ph -> F e. ( SubDRing ` CCfld ) )
5 constrelextdg2.n 
 |-  ( ph -> N e. On )
6 constrelextdg2.1 
 |-  ( ph -> ( C ` N ) C_ F )
7 constrelextdg2.x 
 |-  ( ph -> X e. ( C ` suc N ) )
8 cnfldbas 
 |-  CC = ( Base ` CCfld )
9 8 sdrgss 
 |-  ( F e. ( SubDRing ` CCfld ) -> F C_ CC )
10 4 9 syl 
 |-  ( ph -> F C_ CC )
11 10 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> F C_ CC )
12 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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_ F )
13 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
14 12 13 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
15 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
16 12 15 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
17 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
18 12 17 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
19 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
20 12 19 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
21 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 )
22 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 )
23 simpr1 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) ) )
24 simpr2 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) ) )
25 simpr3 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 )
26 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 ) ) )
27 11 14 16 18 20 21 22 23 24 25 26 constrrtll 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) ) )
28 cnfldadd 
 |-  + = ( +g ` CCfld )
29 sdrgsubrg 
 |-  ( F e. ( SubDRing ` CCfld ) -> F e. ( SubRing ` CCfld ) )
30 subrgsubg 
 |-  ( F e. ( SubRing ` CCfld ) -> F e. ( SubGrp ` CCfld ) )
31 4 29 30 3syl 
 |-  ( ph -> F e. ( SubGrp ` CCfld ) )
32 31 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> F e. ( SubGrp ` CCfld ) )
33 cnfldmul 
 |-  x. = ( .r ` CCfld )
34 4 29 syl 
 |-  ( ph -> F e. ( SubRing ` CCfld ) )
35 34 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> F e. ( SubRing ` CCfld ) )
36 cnflddiv 
 |-  / = ( /r ` CCfld )
37 cnfld0 
 |-  0 = ( 0g ` CCfld )
38 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> F e. ( SubDRing ` CCfld ) )
39 cnfldsub 
 |-  - = ( -g ` CCfld )
40 39 32 14 18 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) e. F )
41 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> N e. On )
42 1 41 19 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
43 12 42 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
44 1 41 17 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
45 12 44 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
46 39 32 43 45 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` c ) ) e. F )
47 33 35 40 46 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) x. ( ( * ` d ) - ( * ` c ) ) ) e. F )
48 1 41 13 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
49 12 48 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
50 39 32 49 45 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` c ) ) e. F )
51 39 32 20 18 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) e. F )
52 33 35 50 51 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` c ) ) x. ( d - c ) ) e. F )
53 39 32 47 52 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) e. F )
54 1 41 15 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) )
55 12 54 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. F )
56 39 32 55 49 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` a ) ) e. F )
57 33 35 56 51 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` a ) ) x. ( d - c ) ) e. F )
58 39 32 16 14 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) e. F )
59 33 35 58 46 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) x. ( ( * ` d ) - ( * ` c ) ) ) e. F )
60 39 32 57 59 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) e. F )
61 11 16 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. CC )
62 11 14 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. CC )
63 61 62 cjsubd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) = ( ( * ` b ) - ( * ` a ) ) )
64 63 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) = ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) )
65 11 58 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) e. CC )
66 65 cjcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) e. CC )
67 11 51 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) e. CC )
68 66 67 cjmuld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) ) = ( ( * ` ( * ` ( b - a ) ) ) x. ( * ` ( d - c ) ) ) )
69 65 cjcjd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) ) = ( b - a ) )
70 11 20 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. CC )
71 11 18 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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. CC )
72 70 71 cjsubd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) ) = ( ( * ` d ) - ( * ` c ) ) )
73 69 72 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) ) x. ( * ` ( d - c ) ) ) = ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) )
74 68 73 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) ) = ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) )
75 64 74 oveq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) = ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) )
76 66 67 mulcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) e. CC )
77 imval2 
 |-  ( ( ( * ` ( b - a ) ) x. ( d - c ) ) e. CC -> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = ( ( ( ( * ` ( b - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) / ( 2 x. _i ) ) )
78 76 77 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) ) = ( ( ( ( * ` ( b - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) / ( 2 x. _i ) ) )
79 78 neeq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 <-> ( ( ( ( * ` ( b - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) / ( 2 x. _i ) ) =/= 0 ) )
80 25 79 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) / ( 2 x. _i ) ) =/= 0 )
81 76 cjcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) ) e. CC )
82 76 81 subcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) e. CC )
83 2cnd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> 2 e. CC )
84 ax-icn 
 |-  _i e. CC
85 84 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> _i e. CC )
86 83 85 mulcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> ( 2 x. _i ) e. CC )
87 2cn 
 |-  2 e. CC
88 2ne0 
 |-  2 =/= 0
89 ine0 
 |-  _i =/= 0
90 87 84 88 89 mulne0i 
 |-  ( 2 x. _i ) =/= 0
91 90 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) ) -> ( 2 x. _i ) =/= 0 )
92 82 86 91 divne0bd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) =/= 0 <-> ( ( ( ( * ` ( b - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) / ( 2 x. _i ) ) =/= 0 ) )
93 80 92 mpbird 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - a ) ) x. ( d - c ) ) - ( * ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) ) =/= 0 )
94 75 93 eqnetrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) =/= 0 )
95 36 37 38 53 60 94 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) e. F )
96 33 35 95 58 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) e. F )
97 28 32 14 96 subgcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 + ( ( ( ( ( a - c ) x. ( ( * ` d ) - ( * ` c ) ) ) - ( ( ( * ` a ) - ( * ` c ) ) x. ( d - c ) ) ) / ( ( ( ( * ` b ) - ( * ` a ) ) x. ( d - c ) ) - ( ( b - a ) x. ( ( * ` d ) - ( * ` c ) ) ) ) ) x. ( b - a ) ) ) e. F )
98 27 97 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 e. F )
99 98 orcd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 e. F \/ ( L [:] K ) = 2 ) )
100 99 r19.29an 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ 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 e. F \/ ( L [:] K ) = 2 ) )
101 100 r19.29an 
 |-  ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ 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 ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
102 101 r19.29an 
 |-  ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ E. d e. ( C ` N ) E. t e. RR E. r e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
103 102 r19.29an 
 |-  ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ E. c e. ( C ` N ) E. d e. ( C ` N ) E. t e. RR E. r e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
104 103 r19.29an 
 |-  ( ( ( ph /\ 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 ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
105 104 r19.29an 
 |-  ( ( ph /\ 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 ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
106 1 5 constrsscn 
 |-  ( ph -> ( C ` N ) C_ CC )
107 106 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> ( C ` N ) C_ CC )
108 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> a e. ( C ` N ) )
109 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> b e. ( C ` N ) )
110 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> c e. ( C ` N ) )
111 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> e e. ( C ` N ) )
112 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> f e. ( C ` N ) )
113 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> t e. RR )
114 simplrl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> X = ( a + ( t x. ( b - a ) ) ) )
115 simplrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) )
116 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> a = b )
117 107 108 109 110 111 112 113 114 115 116 constrrtlc2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> X = a )
118 6 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> ( C ` N ) C_ F )
119 118 108 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> a e. F )
120 117 119 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> X e. F )
121 120 orcd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a = b ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
122 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
123 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
124 cnfldfld 
 |-  CCfld e. Field
125 124 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> CCfld e. Field )
126 4 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> F e. ( SubDRing ` CCfld ) )
127 eqid 
 |-  ( C ` N ) = ( C ` N )
128 1 5 127 constrsuc 
 |-  ( ph -> ( 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 ) ) ) ) ) ) )
129 7 128 mpbid 
 |-  ( ph -> ( 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 ) ) ) ) ) )
130 129 simpld 
 |-  ( ph -> X e. CC )
131 130 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> X e. CC )
132 31 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> F e. ( SubGrp ` CCfld ) )
133 6 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( C ` N ) C_ F )
134 5 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> N e. On )
135 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> a e. ( C ` N ) )
136 1 134 135 constrconj 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` a ) e. ( C ` N ) )
137 133 136 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` a ) e. F )
138 126 29 syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> F e. ( SubRing ` CCfld ) )
139 133 135 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> a e. F )
140 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> b e. ( C ` N ) )
141 1 134 140 constrconj 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` b ) e. ( C ` N ) )
142 133 141 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` b ) e. F )
143 39 132 142 137 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( * ` b ) - ( * ` a ) ) e. F )
144 133 140 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> b e. F )
145 39 132 144 139 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( b - a ) e. F )
146 106 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( C ` N ) C_ CC )
147 146 140 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> b e. CC )
148 146 135 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> a e. CC )
149 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> a =/= b )
150 149 necomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> b =/= a )
151 147 148 150 subne0d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( b - a ) =/= 0 )
152 36 37 126 143 145 151 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) e. F )
153 33 138 139 152 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. F )
154 39 132 137 153 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) e. F )
155 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> c e. ( C ` N ) )
156 1 134 155 constrconj 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` c ) e. ( C ` N ) )
157 133 156 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` c ) e. F )
158 39 132 154 157 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) e. F )
159 133 155 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> c e. F )
160 33 138 159 152 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. F )
161 39 132 158 160 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) e. F )
162 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> e e. ( C ` N ) )
163 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> f e. ( C ` N ) )
164 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> t e. RR )
165 simplrl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> X = ( a + ( t x. ( b - a ) ) ) )
166 simplrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) )
167 eqid 
 |-  ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) = ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) )
168 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 ) ) )
169 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 ) ) )
170 146 135 140 155 162 163 164 165 166 167 168 169 149 constrrtlc1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( 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 ) )
171 170 simprd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) =/= 0 )
172 36 37 126 161 152 171 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) - ( c x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. F )
173 df-neg 
 |-  -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) = ( 0 - ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) )
174 1 134 constr01 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> { 0 , 1 } C_ ( C ` N ) )
175 0elpr01 
 |-  0 e. { 0 , 1 }
176 175 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> 0 e. { 0 , 1 } )
177 174 176 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> 0 e. ( C ` N ) )
178 133 177 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> 0 e. F )
179 33 138 159 158 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) e. F )
180 133 162 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> e e. F )
181 133 163 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> f e. F )
182 39 132 180 181 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( e - f ) e. F )
183 1 134 162 constrconj 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` e ) e. ( C ` N ) )
184 133 183 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` e ) e. F )
185 1 134 163 constrconj 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` f ) e. ( C ` N ) )
186 133 185 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( * ` f ) e. F )
187 39 132 184 186 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( * ` e ) - ( * ` f ) ) e. F )
188 33 138 182 187 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) e. F )
189 28 132 179 188 subgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) e. F )
190 39 132 178 189 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( 0 - ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) ) e. F )
191 173 190 eqeltrid 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) e. F )
192 36 37 126 191 152 171 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( -u ( ( c x. ( ( ( * ` a ) - ( a x. ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) ) - ( * ` c ) ) ) + ( ( e - f ) x. ( ( * ` e ) - ( * ` f ) ) ) ) / ( ( ( * ` b ) - ( * ` a ) ) / ( b - a ) ) ) e. F )
193 2nn0 
 |-  2 e. NN0
194 193 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> 2 e. NN0 )
195 cnfldexp 
 |-  ( ( X e. CC /\ 2 e. NN0 ) -> ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) = ( X ^ 2 ) )
196 131 194 195 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) = ( X ^ 2 ) )
197 196 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) + ( ( ( ( ( ( ( * ` 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 ) ) ) ) ) )
198 170 simpld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( 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 )
199 197 198 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) + ( ( ( ( ( ( ( * ` 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 )
200 2 3 37 122 8 33 28 123 125 126 131 172 192 199 rtelextdg2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) /\ a =/= b ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
201 exmidne 
 |-  ( a = b \/ a =/= b )
202 201 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( a = b \/ a =/= b ) )
203 121 200 202 mpjaodan 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ t e. RR ) /\ ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
204 203 r19.29an 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
205 204 r19.29an 
 |-  ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ E. f e. ( C ` N ) E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
206 205 r19.29an 
 |-  ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
207 206 r19.29an 
 |-  ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
208 207 r19.29an 
 |-  ( ( ( ph /\ 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 ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
209 208 r19.29an 
 |-  ( ( ph /\ 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 ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
210 124 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> CCfld e. Field )
211 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> F e. ( SubDRing ` CCfld ) )
212 130 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> X e. CC )
213 211 29 30 3syl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> F e. ( SubGrp ` CCfld ) )
214 211 29 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> F e. ( SubRing ` CCfld ) )
215 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( C ` N ) C_ F )
216 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> e e. ( C ` N ) )
217 215 216 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> e e. F )
218 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> f e. ( C ` N ) )
219 215 218 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> f e. F )
220 39 213 217 219 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( e - f ) e. F )
221 106 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( C ` N ) C_ CC )
222 221 216 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> e e. CC )
223 221 218 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> f e. CC )
224 222 223 cjsubd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( e - f ) ) = ( ( * ` e ) - ( * ` f ) ) )
225 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> N e. On )
226 1 225 216 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` e ) e. ( C ` N ) )
227 215 226 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` e ) e. F )
228 1 225 218 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` f ) e. ( C ` N ) )
229 215 228 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` f ) e. F )
230 39 213 227 229 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` e ) - ( * ` f ) ) e. F )
231 224 230 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( e - f ) ) e. F )
232 33 214 220 231 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( e - f ) x. ( * ` ( e - f ) ) ) e. F )
233 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> d e. ( C ` N ) )
234 1 225 233 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` d ) e. ( C ` N ) )
235 215 234 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` d ) e. F )
236 215 233 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> d e. F )
237 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> a e. ( C ` N ) )
238 215 237 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> a e. F )
239 28 213 236 238 subgcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d + a ) e. F )
240 33 214 235 239 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) x. ( d + a ) ) e. F )
241 39 213 232 240 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( e - f ) x. ( * ` ( e - f ) ) ) - ( ( * ` d ) x. ( d + a ) ) ) e. F )
242 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> b e. ( C ` N ) )
243 215 242 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> b e. F )
244 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> c e. ( C ` N ) )
245 215 244 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> c e. F )
246 39 213 243 245 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( b - c ) e. F )
247 221 242 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> b e. CC )
248 221 244 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> c e. CC )
249 247 248 cjsubd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( b - c ) ) = ( ( * ` b ) - ( * ` c ) ) )
250 1 225 242 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` b ) e. ( C ` N ) )
251 215 250 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` b ) e. F )
252 1 225 244 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` c ) e. ( C ` N ) )
253 215 252 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` c ) e. F )
254 39 213 251 253 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` b ) - ( * ` c ) ) e. F )
255 249 254 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( b - c ) ) e. F )
256 33 214 246 255 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( b - c ) x. ( * ` ( b - c ) ) ) e. F )
257 1 225 237 constrconj 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` a ) e. ( C ` N ) )
258 215 257 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` a ) e. F )
259 33 214 258 239 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` a ) x. ( d + a ) ) e. F )
260 39 213 256 259 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) e. F )
261 39 213 241 260 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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. F )
262 39 213 235 258 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) - ( * ` a ) ) e. F )
263 221 233 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> d e. CC )
264 221 237 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> a e. CC )
265 263 264 cjsubd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( d - a ) ) = ( ( * ` d ) - ( * ` a ) ) )
266 263 264 subcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d - a ) e. CC )
267 simpr1 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> a =/= d )
268 267 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> d =/= a )
269 263 264 268 subne0d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d - a ) =/= 0 )
270 266 269 cjne0d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( * ` ( d - a ) ) =/= 0 )
271 265 270 eqnetrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) - ( * ` a ) ) =/= 0 )
272 36 37 211 261 262 271 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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. F )
273 df-neg 
 |-  -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 - ( ( ( ( ( * ` 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 ) ) ) )
274 1 225 constr01 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> { 0 , 1 } C_ ( C ` N ) )
275 175 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> 0 e. { 0 , 1 } )
276 274 275 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> 0 e. ( C ` N ) )
277 215 276 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> 0 e. F )
278 33 214 236 238 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( d x. a ) e. F )
279 33 214 258 278 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` a ) x. ( d x. a ) ) e. F )
280 33 214 256 236 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) e. F )
281 39 213 279 280 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` a ) x. ( d x. a ) ) - ( ( ( b - c ) x. ( * ` ( b - c ) ) ) x. d ) ) e. F )
282 33 214 235 278 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( * ` d ) x. ( d x. a ) ) e. F )
283 33 214 232 238 subrgmcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) e. F )
284 39 213 282 283 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) e. F )
285 39 213 281 284 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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. F )
286 36 37 211 285 262 271 sdrgdvcl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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. F )
287 39 213 277 286 subgsubcld 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( 0 - ( ( ( ( ( * ` 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. F )
288 273 287 eqeltrid 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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. F )
289 212 193 195 sylancl 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) = ( X ^ 2 ) )
290 289 oveq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) + ( ( ( ( ( ( ( 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 ) ) ) ) ) )
291 simpr2 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) )
292 simpr3 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) )
293 eqid 
 |-  ( ( b - c ) x. ( * ` ( b - c ) ) ) = ( ( b - c ) x. ( * ` ( b - c ) ) )
294 eqid 
 |-  ( ( e - f ) x. ( * ` ( e - f ) ) ) = ( ( e - f ) x. ( * ` ( e - f ) ) )
295 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 ) ) )
296 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 ) ) )
297 221 237 242 244 233 216 218 212 267 291 292 293 294 295 296 constrrtcc 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( 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 )
298 290 297 eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) + ( ( ( ( ( ( ( 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 )
299 2 3 37 122 8 33 28 123 210 211 212 272 288 298 rtelextdg2 
 |-  ( ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ f e. ( C ` N ) ) /\ ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
300 299 r19.29an 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ e e. ( C ` N ) ) /\ E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
301 300 r19.29an 
 |-  ( ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ d e. ( C ` N ) ) /\ E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
302 301 r19.29an 
 |-  ( ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ c e. ( C ` N ) ) /\ E. d e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
303 302 r19.29an 
 |-  ( ( ( ( ph /\ a e. ( C ` N ) ) /\ b e. ( C ` N ) ) /\ E. c e. ( C ` N ) E. d e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) -> ( X e. F \/ ( L [:] K ) = 2 ) )
304 303 r19.29an 
 |-  ( ( ( ph /\ 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. F \/ ( L [:] K ) = 2 ) )
305 304 r19.29an 
 |-  ( ( ph /\ 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. F \/ ( L [:] K ) = 2 ) )
306 129 simprd 
 |-  ( ph -> ( 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 ) ) ) ) )
307 105 209 305 306 mpjao3dan 
 |-  ( ph -> ( X e. F \/ ( L [:] K ) = 2 ) )