Metamath Proof Explorer

Theorem constrsuc

Description: Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-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 } )
constrsuc.1 
|- ( ph -> N e. On )
constrsuc.2 
|- S = ( C ` N )
Assertion constrsuc 
|- ( ph -> ( X e. ( C ` suc N ) <-> ( 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 ) ) ) ) ) ) )

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 constrsuc.1 
 |-  ( ph -> N e. On )
3 constrsuc.2 
 |-  S = ( C ` N )
4 1 fveq1i 
 |-  ( C ` suc N ) = ( 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 } ) ` suc N )
5 rdgsuc 
 |-  ( N e. On -> ( 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 } ) ` suc N ) = ( ( 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 ) ) ) ) } ) ` ( 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 } ) ` N ) ) )
6 2 5 syl 
 |-  ( ph -> ( 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 } ) ` suc N ) = ( ( 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 ) ) ) ) } ) ` ( 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 } ) ` N ) ) )
7 4 6 eqtrid 
 |-  ( ph -> ( C ` suc N ) = ( ( 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 ) ) ) ) } ) ` ( 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 } ) ` N ) ) )
8 1 fveq1i 
 |-  ( C ` N ) = ( 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 } ) ` N )
9 3 8 eqtri 
 |-  S = ( 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 } ) ` N )
10 9 fveq2i 
 |-  ( ( 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 ) ) ) ) } ) ` S ) = ( ( 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 ) ) ) ) } ) ` ( 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 } ) ` N ) )
11 7 10 eqtr4di 
 |-  ( ph -> ( C ` suc N ) = ( ( 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 ) ) ) ) } ) ` S ) )
12 11 eleq2d 
 |-  ( ph -> ( X e. ( C ` suc N ) <-> X e. ( ( 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 ) ) ) ) } ) ` S ) ) )
13 eqid 
 |-  ( 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 ) ) ) ) } ) = ( 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 ) ) ) ) } )
14 id 
 |-  ( s = S -> s = S )
15 rexeq 
 |-  ( s = 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. 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 ) ) )
16 14 15 rexeqbidv 
 |-  ( s = 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. 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 ) ) )
17 14 16 rexeqbidv 
 |-  ( s = 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. 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 ) ) )
18 14 17 rexeqbidv 
 |-  ( s = S -> ( 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. 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 ) ) )
19 rexeq 
 |-  ( s = S -> ( E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. S E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
20 14 19 rexeqbidv 
 |-  ( s = 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. e e. S E. f e. S E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
21 14 20 rexeqbidv 
 |-  ( s = 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. 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 ) ) ) ) )
22 14 21 rexeqbidv 
 |-  ( s = 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. 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 ) ) ) ) )
23 14 22 rexeqbidvv 
 |-  ( s = S -> ( 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. e e. S E. f e. S E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
24 rexeq 
 |-  ( s = S -> ( E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. S ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
25 14 24 rexeqbidv 
 |-  ( s = S -> ( E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
26 14 25 rexeqbidv 
 |-  ( s = 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 ) ) ) <-> 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 ) ) ) ) )
27 14 26 rexeqbidv 
 |-  ( s = 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 ) ) ) <-> 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 ) ) ) ) )
28 14 27 rexeqbidv 
 |-  ( s = 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 ) ) ) <-> 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 ) ) ) ) )
29 14 28 rexeqbidvv 
 |-  ( s = S -> ( 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 ) ) ) <-> 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 ) ) ) ) )
30 18 23 29 3orbi123d 
 |-  ( s = S -> ( ( 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
31 30 rabbidv 
 |-  ( s = S -> { 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 ) ) ) ) } = { 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 ) ) ) ) } )
32 31 adantl 
 |-  ( ( ph /\ s = S ) -> { 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 ) ) ) ) } = { 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 ) ) ) ) } )
33 3 fvexi 
 |-  S e. _V
34 33 a1i 
 |-  ( ph -> S e. _V )
35 cnex 
 |-  CC e. _V
36 ssrab2 
 |-  { 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 ) ) ) ) } C_ CC
37 35 36 ssexi 
 |-  { 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 ) ) ) ) } e. _V
38 37 a1i 
 |-  ( ph -> { 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 ) ) ) ) } e. _V )
39 13 32 34 38 fvmptd2 
 |-  ( ph -> ( ( 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 ) ) ) ) } ) ` S ) = { 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 ) ) ) ) } )
40 39 eleq2d 
 |-  ( ph -> ( X e. ( ( 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 ) ) ) ) } ) ` S ) <-> X e. { 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 ) ) ) ) } ) )
41 eqeq1 
 |-  ( x = y -> ( x = ( a + ( t x. ( b - a ) ) ) <-> y = ( a + ( t x. ( b - a ) ) ) ) )
42 eqeq1 
 |-  ( x = y -> ( x = ( c + ( r x. ( d - c ) ) ) <-> y = ( c + ( r x. ( d - c ) ) ) ) )
43 41 42 3anbi12d 
 |-  ( x = y -> ( ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
44 43 2rexbidv 
 |-  ( x = y -> ( 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. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
45 44 2rexbidv 
 |-  ( x = y -> ( 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. c e. S E. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
46 45 2rexbidv 
 |-  ( x = y -> ( 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. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
47 fvoveq1 
 |-  ( x = y -> ( abs ` ( x - c ) ) = ( abs ` ( y - c ) ) )
48 47 eqeq1d 
 |-  ( x = y -> ( ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
49 41 48 anbi12d 
 |-  ( x = y -> ( ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
50 49 2rexbidv 
 |-  ( x = y -> ( E. f e. S E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
51 50 2rexbidv 
 |-  ( x = y -> ( 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. c e. S E. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
52 51 2rexbidv 
 |-  ( x = y -> ( 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. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
53 fvoveq1 
 |-  ( x = y -> ( abs ` ( x - a ) ) = ( abs ` ( y - a ) ) )
54 53 eqeq1d 
 |-  ( x = y -> ( ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) <-> ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) ) )
55 fvoveq1 
 |-  ( x = y -> ( abs ` ( x - d ) ) = ( abs ` ( y - d ) ) )
56 55 eqeq1d 
 |-  ( x = y -> ( ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
57 54 56 3anbi23d 
 |-  ( x = y -> ( ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
58 57 2rexbidv 
 |-  ( x = y -> ( E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
59 58 2rexbidv 
 |-  ( x = y -> ( 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 ) ) ) <-> E. c e. S E. d e. S E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
60 59 2rexbidv 
 |-  ( x = y -> ( 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 ) ) ) <-> 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
61 46 52 60 3orbi123d 
 |-  ( x = y -> ( ( 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 ) ) ) ) <-> ( E. a e. S E. b e. S E. c e. S E. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. S E. b e. S E. c e. S E. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
62 61 cbvrabv 
 |-  { 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 ) ) ) ) } = { y 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) }
63 62 eleq2i 
 |-  ( X e. { 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 ) ) ) ) } <-> X e. { y 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) } )
64 eqeq1 
 |-  ( y = X -> ( y = ( a + ( t x. ( b - a ) ) ) <-> X = ( a + ( t x. ( b - a ) ) ) ) )
65 eqeq1 
 |-  ( y = X -> ( y = ( c + ( r x. ( d - c ) ) ) <-> X = ( c + ( r x. ( d - c ) ) ) ) )
66 64 65 3anbi12d 
 |-  ( y = X -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
67 66 2rexbidv 
 |-  ( y = X -> ( E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
68 67 2rexbidv 
 |-  ( y = X -> ( E. c e. S E. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. 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 ) ) )
69 68 2rexbidv 
 |-  ( y = X -> ( E. a e. S E. b e. S E. c e. S E. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. 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 ) ) )
70 fvoveq1 
 |-  ( y = X -> ( abs ` ( y - c ) ) = ( abs ` ( X - c ) ) )
71 70 eqeq1d 
 |-  ( y = X -> ( ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) )
72 64 71 anbi12d 
 |-  ( y = X -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
73 72 2rexbidv 
 |-  ( y = X -> ( E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. S E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
74 73 2rexbidv 
 |-  ( y = X -> ( E. c e. S E. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> 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 ) ) ) ) )
75 74 2rexbidv 
 |-  ( y = X -> ( E. a e. S E. b e. S E. c e. S E. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> 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 ) ) ) ) )
76 fvoveq1 
 |-  ( y = X -> ( abs ` ( y - a ) ) = ( abs ` ( X - a ) ) )
77 76 eqeq1d 
 |-  ( y = X -> ( ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) <-> ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) ) )
78 fvoveq1 
 |-  ( y = X -> ( abs ` ( y - d ) ) = ( abs ` ( X - d ) ) )
79 78 eqeq1d 
 |-  ( y = X -> ( ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) )
80 77 79 3anbi23d 
 |-  ( y = X -> ( ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) )
81 80 2rexbidv 
 |-  ( y = X -> ( E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( X - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( X - d ) ) = ( abs ` ( e - f ) ) ) ) )
82 81 2rexbidv 
 |-  ( y = X -> ( E. c e. S E. d e. S E. e e. S E. f e. S ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> 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 ) ) ) ) )
83 82 2rexbidv 
 |-  ( y = X -> ( 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( 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 ) ) ) ) )
84 69 75 83 3orbi123d 
 |-  ( y = X -> ( ( E. a e. S E. b e. S E. c e. S E. d e. S E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. S E. b e. S E. c e. S E. e e. S E. f e. S E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( 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 ) ) ) ) ) )
85 84 elrab 
 |-  ( X e. { y 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( 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 ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - 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 ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) } <-> ( 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 ) ) ) ) ) )
86 63 85 bitri 
 |-  ( X e. { 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) )
87 86 a1i 
 |-  ( ph -> ( X e. { 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) ) )
88 12 40 87 3bitrd 
 |-  ( ph -> ( X e. ( C ` suc N ) <-> ( 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 ) ) ) ) ) ) )