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 37 fvexi 
 |-  0 e. _V
176 175 prid1 
 |-  0 e. { 0 , 1 }
177 176 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 } )
178 174 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. ( C ` N ) )
179 133 178 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 )
180 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 )
181 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 )
182 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 )
183 39 132 181 182 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 )
184 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 ) )
185 133 184 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 )
186 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 ) )
187 133 186 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 )
188 39 132 185 187 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 )
189 33 138 183 188 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 )
190 28 132 180 189 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 )
191 39 132 179 190 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 )
192 173 191 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 )
193 36 37 126 192 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 )
194 2nn0 
 |-  2 e. NN0
195 194 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 )
196 cnfldexp 
 |-  ( ( X e. CC /\ 2 e. NN0 ) -> ( 2 ( .g ` ( mulGrp ` CCfld ) ) X ) = ( X ^ 2 ) )
197 131 195 196 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 ) )
198 197 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 ) ) ) ) ) )
199 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 )
200 198 199 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 )
201 2 3 37 122 8 33 28 123 125 126 131 172 193 200 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 ) )
202 exmidne 
 |-  ( a = b \/ a =/= b )
203 202 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 ) )
204 121 201 203 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 ) )
205 204 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 ) )
206 205 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 ) )
207 206 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 ) )
208 207 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 ) )
209 208 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 ) )
210 209 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 ) )
211 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 )
212 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 ) )
213 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 )
214 212 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 ) )
215 212 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 ) )
216 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 )
217 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 ) )
218 216 217 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 )
219 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 ) )
220 216 219 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 )
221 39 214 218 220 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 )
222 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 )
223 222 217 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 )
224 222 219 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 )
225 223 224 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 ) ) )
226 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 )
227 1 226 217 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 ) )
228 216 227 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 )
229 1 226 219 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 ) )
230 216 229 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 )
231 39 214 228 230 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 )
232 225 231 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 )
233 33 215 221 232 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 )
234 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 ) )
235 1 226 234 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 ) )
236 216 235 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 216 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 )
238 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 ) )
239 216 238 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 )
240 28 214 237 239 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 )
241 33 215 236 240 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 )
242 39 214 233 241 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 )
243 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 ) )
244 216 243 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 )
245 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 ) )
246 216 245 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 )
247 39 214 244 246 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 )
248 222 243 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 )
249 222 245 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 )
250 248 249 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 ) ) )
251 1 226 243 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 ) )
252 216 251 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 )
253 1 226 245 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 ) )
254 216 253 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 )
255 39 214 252 254 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 )
256 250 255 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 )
257 33 215 247 256 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 )
258 1 226 238 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 ) )
259 216 258 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 )
260 33 215 259 240 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 )
261 39 214 257 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 ) ) ) ) -> ( ( ( b - c ) x. ( * ` ( b - c ) ) ) - ( ( * ` a ) x. ( d + a ) ) ) e. F )
262 39 214 242 261 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 )
263 39 214 236 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 ) ) ) ) -> ( ( * ` d ) - ( * ` a ) ) e. F )
264 222 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. CC )
265 222 238 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 )
266 264 265 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 ) ) )
267 264 265 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 )
268 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 )
269 268 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 )
270 264 265 269 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 )
271 267 270 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 )
272 266 271 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 )
273 36 37 212 262 263 272 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 )
274 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 ) ) ) )
275 1 226 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 ) )
276 176 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 } )
277 275 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. ( C ` N ) )
278 216 277 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 )
279 33 215 237 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. a ) e. F )
280 33 215 259 279 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 )
281 33 215 257 237 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 )
282 39 214 280 281 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 )
283 33 215 236 279 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 )
284 33 215 233 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 ) ) ) ) -> ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) e. F )
285 39 214 283 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 ) ) ) ) -> ( ( ( * ` d ) x. ( d x. a ) ) - ( ( ( e - f ) x. ( * ` ( e - f ) ) ) x. a ) ) e. F )
286 39 214 282 285 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 )
287 36 37 212 286 263 272 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 )
288 39 214 278 287 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 )
289 274 288 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 )
290 213 194 196 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 ) )
291 290 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 ) ) ) ) ) )
292 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 ) ) )
293 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 ) ) )
294 eqid 
 |-  ( ( b - c ) x. ( * ` ( b - c ) ) ) = ( ( b - c ) x. ( * ` ( b - c ) ) )
295 eqid 
 |-  ( ( e - f ) x. ( * ` ( e - f ) ) ) = ( ( e - f ) x. ( * ` ( e - f ) ) )
296 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 ) ) )
297 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 ) ) )
298 222 238 243 245 234 217 219 213 268 292 293 294 295 296 297 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 )
299 291 298 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 )
300 2 3 37 122 8 33 28 123 211 212 213 273 289 299 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 ) )
301 300 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 ) )
302 301 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 ) )
303 302 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 ) )
304 303 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 ) )
305 304 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 ) )
306 305 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 ) )
307 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 ) ) ) ) )
308 105 210 306 307 mpjao3dan 
 |-  ( ph -> ( X e. F \/ ( L [:] K ) = 2 ) )