Metamath Proof Explorer

Theorem constrllcllem

Description: Constructible numbers are closed under line-line intersections. (Contributed by Thierry Arnoux, 2-Nov-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 } )
constrllcllem.a 
|- ( ph -> A e. Constr )
constrllcllem.b 
|- ( ph -> B e. Constr )
constrllcllem.c 
|- ( ph -> G e. Constr )
constrllcllem.e 
|- ( ph -> D e. Constr )
constrllcllem.t 
|- ( ph -> T e. RR )
constrllcllem.r 
|- ( ph -> R e. RR )
constrllcllem.x 
|- ( ph -> X e. CC )
constrllcllem.1 
|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
constrllcllem.2 
|- ( ph -> X = ( G + ( R x. ( D - G ) ) ) )
constrllcllem.3 
|- ( ph -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 )
Assertion constrllcllem 
|- ( ph -> X e. Constr )

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 constrllcllem.a 
 |-  ( ph -> A e. Constr )
3 constrllcllem.b 
 |-  ( ph -> B e. Constr )
4 constrllcllem.c 
 |-  ( ph -> G e. Constr )
5 constrllcllem.e 
 |-  ( ph -> D e. Constr )
6 constrllcllem.t 
 |-  ( ph -> T e. RR )
7 constrllcllem.r 
 |-  ( ph -> R e. RR )
8 constrllcllem.x 
 |-  ( ph -> X e. CC )
9 constrllcllem.1 
 |-  ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
10 constrllcllem.2 
 |-  ( ph -> X = ( G + ( R x. ( D - G ) ) ) )
11 constrllcllem.3 
 |-  ( ph -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 )
12 peano2b 
 |-  ( n e. _om <-> suc n e. _om )
13 12 biimpi 
 |-  ( n e. _om -> suc n e. _om )
14 13 ad2antlr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> suc n e. _om )
15 fveq2 
 |-  ( m = suc n -> ( C ` m ) = ( C ` suc n ) )
16 15 eleq2d 
 |-  ( m = suc n -> ( X e. ( C ` m ) <-> X e. ( C ` suc n ) ) )
17 16 adantl 
 |-  ( ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) /\ m = suc n ) -> ( X e. ( C ` m ) <-> X e. ( C ` suc n ) ) )
18 8 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> X e. CC )
19 id 
 |-  ( a = A -> a = A )
20 oveq2 
 |-  ( a = A -> ( b - a ) = ( b - A ) )
21 20 oveq2d 
 |-  ( a = A -> ( t x. ( b - a ) ) = ( t x. ( b - A ) ) )
22 19 21 oveq12d 
 |-  ( a = A -> ( a + ( t x. ( b - a ) ) ) = ( A + ( t x. ( b - A ) ) ) )
23 22 eqeq2d 
 |-  ( a = A -> ( X = ( a + ( t x. ( b - a ) ) ) <-> X = ( A + ( t x. ( b - A ) ) ) ) )
24 20 fveq2d 
 |-  ( a = A -> ( * ` ( b - a ) ) = ( * ` ( b - A ) ) )
25 24 oveq1d 
 |-  ( a = A -> ( ( * ` ( b - a ) ) x. ( d - c ) ) = ( ( * ` ( b - A ) ) x. ( d - c ) ) )
26 25 fveq2d 
 |-  ( a = A -> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) )
27 26 neeq1d 
 |-  ( a = A -> ( ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) =/= 0 ) )
28 23 27 3anbi13d 
 |-  ( a = A -> ( ( 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 ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) =/= 0 ) ) )
29 28 rexbidv 
 |-  ( a = A -> ( E. r e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. r e. RR ( X = ( A + ( t x. ( b - A ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) =/= 0 ) ) )
30 29 2rexbidv 
 |-  ( a = A -> ( 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. 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 ) ) )
31 oveq1 
 |-  ( b = B -> ( b - A ) = ( B - A ) )
32 31 oveq2d 
 |-  ( b = B -> ( t x. ( b - A ) ) = ( t x. ( B - A ) ) )
33 32 oveq2d 
 |-  ( b = B -> ( A + ( t x. ( b - A ) ) ) = ( A + ( t x. ( B - A ) ) ) )
34 33 eqeq2d 
 |-  ( b = B -> ( X = ( A + ( t x. ( b - A ) ) ) <-> X = ( A + ( t x. ( B - A ) ) ) ) )
35 31 fveq2d 
 |-  ( b = B -> ( * ` ( b - A ) ) = ( * ` ( B - A ) ) )
36 35 oveq1d 
 |-  ( b = B -> ( ( * ` ( b - A ) ) x. ( d - c ) ) = ( ( * ` ( B - A ) ) x. ( d - c ) ) )
37 36 fveq2d 
 |-  ( b = B -> ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) )
38 37 neeq1d 
 |-  ( b = B -> ( ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) =/= 0 ) )
39 34 38 3anbi13d 
 |-  ( b = B -> ( ( 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 ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) =/= 0 ) ) )
40 39 rexbidv 
 |-  ( b = B -> ( E. r e. RR ( X = ( A + ( t x. ( b - A ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - A ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. r e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) =/= 0 ) ) )
41 40 2rexbidv 
 |-  ( b = B -> ( 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. 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 ) ) )
42 id 
 |-  ( c = G -> c = G )
43 oveq2 
 |-  ( c = G -> ( d - c ) = ( d - G ) )
44 43 oveq2d 
 |-  ( c = G -> ( r x. ( d - c ) ) = ( r x. ( d - G ) ) )
45 42 44 oveq12d 
 |-  ( c = G -> ( c + ( r x. ( d - c ) ) ) = ( G + ( r x. ( d - G ) ) ) )
46 45 eqeq2d 
 |-  ( c = G -> ( X = ( c + ( r x. ( d - c ) ) ) <-> X = ( G + ( r x. ( d - G ) ) ) ) )
47 43 oveq2d 
 |-  ( c = G -> ( ( * ` ( B - A ) ) x. ( d - c ) ) = ( ( * ` ( B - A ) ) x. ( d - G ) ) )
48 47 fveq2d 
 |-  ( c = G -> ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) )
49 48 neeq1d 
 |-  ( c = G -> ( ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) )
50 46 49 3anbi23d 
 |-  ( c = G -> ( ( 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 ) ) ) /\ X = ( G + ( r x. ( d - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) ) )
51 50 rexbidv 
 |-  ( c = G -> ( E. r e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. r e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( d - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) ) )
52 51 2rexbidv 
 |-  ( c = G -> ( 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. d e. ( C ` n ) E. t e. RR E. r e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( d - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) ) )
53 2 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> A e. Constr )
54 simpr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> ( { A , B } u. { G , D } ) C_ ( C ` n ) )
55 54 unssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> { A , B } C_ ( C ` n ) )
56 53 55 prssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> A e. ( C ` n ) )
57 3 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> B e. Constr )
58 57 55 prssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> B e. ( C ` n ) )
59 4 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> G e. Constr )
60 54 unssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> { G , D } C_ ( C ` n ) )
61 59 60 prssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> G e. ( C ` n ) )
62 oveq1 
 |-  ( d = D -> ( d - G ) = ( D - G ) )
63 62 oveq2d 
 |-  ( d = D -> ( r x. ( d - G ) ) = ( r x. ( D - G ) ) )
64 63 oveq2d 
 |-  ( d = D -> ( G + ( r x. ( d - G ) ) ) = ( G + ( r x. ( D - G ) ) ) )
65 64 eqeq2d 
 |-  ( d = D -> ( X = ( G + ( r x. ( d - G ) ) ) <-> X = ( G + ( r x. ( D - G ) ) ) ) )
66 62 oveq2d 
 |-  ( d = D -> ( ( * ` ( B - A ) ) x. ( d - G ) ) = ( ( * ` ( B - A ) ) x. ( D - G ) ) )
67 66 fveq2d 
 |-  ( d = D -> ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) = ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) )
68 67 neeq1d 
 |-  ( d = D -> ( ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) )
69 65 68 3anbi23d 
 |-  ( d = D -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( d - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) <-> ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) ) )
70 oveq1 
 |-  ( t = T -> ( t x. ( B - A ) ) = ( T x. ( B - A ) ) )
71 70 oveq2d 
 |-  ( t = T -> ( A + ( t x. ( B - A ) ) ) = ( A + ( T x. ( B - A ) ) ) )
72 71 eqeq2d 
 |-  ( t = T -> ( X = ( A + ( t x. ( B - A ) ) ) <-> X = ( A + ( T x. ( B - A ) ) ) ) )
73 72 3anbi1d 
 |-  ( t = T -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) <-> ( X = ( A + ( T x. ( B - A ) ) ) /\ X = ( G + ( r x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) ) )
74 oveq1 
 |-  ( r = R -> ( r x. ( D - G ) ) = ( R x. ( D - G ) ) )
75 74 oveq2d 
 |-  ( r = R -> ( G + ( r x. ( D - G ) ) ) = ( G + ( R x. ( D - G ) ) ) )
76 75 eqeq2d 
 |-  ( r = R -> ( X = ( G + ( r x. ( D - G ) ) ) <-> X = ( G + ( R x. ( D - G ) ) ) ) )
77 76 3anbi2d 
 |-  ( r = R -> ( ( X = ( A + ( T x. ( B - A ) ) ) /\ X = ( G + ( r x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) <-> ( X = ( A + ( T x. ( B - A ) ) ) /\ X = ( G + ( R x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) ) )
78 5 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> D e. Constr )
79 78 60 prssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> D e. ( C ` n ) )
80 6 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> T e. RR )
81 7 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> R e. RR )
82 9 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> X = ( A + ( T x. ( B - A ) ) ) )
83 10 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> X = ( G + ( R x. ( D - G ) ) ) )
84 11 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 )
85 82 83 84 3jca 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> ( X = ( A + ( T x. ( B - A ) ) ) /\ X = ( G + ( R x. ( D - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( D - G ) ) ) =/= 0 ) )
86 69 73 77 79 80 81 85 3rspcedvdw 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> E. d e. ( C ` n ) E. t e. RR E. r e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ X = ( G + ( r x. ( d - G ) ) ) /\ ( Im ` ( ( * ` ( B - A ) ) x. ( d - G ) ) ) =/= 0 ) )
87 30 41 52 56 58 61 86 3rspcedvdw 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> E. a e. ( C ` n ) E. b e. ( C ` n ) E. c e. ( C ` n ) E. d e. ( C ` n ) E. t e. RR E. r e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ X = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
88 87 3mix1d 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> ( E. a e. ( C ` n ) E. b e. ( C ` n ) E. c e. ( C ` n ) E. d e. ( C ` n ) E. t e. RR E. r e. RR ( 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 ) ) ) ) )
89 nnon 
 |-  ( n e. _om -> n e. On )
90 89 ad2antlr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> n e. On )
91 eqid 
 |-  ( C ` n ) = ( C ` n )
92 1 90 91 constrsuc 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> ( 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 ) ) ) ) ) ) )
93 18 88 92 mpbir2and 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> X e. ( C ` suc n ) )
94 14 17 93 rspcedvd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> E. m e. _om X e. ( C ` m ) )
95 1 isconstr 
 |-  ( X e. Constr <-> E. m e. _om X e. ( C ` m ) )
96 94 95 sylibr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B } u. { G , D } ) C_ ( C ` n ) ) -> X e. Constr )
97 2 3 prssd 
 |-  ( ph -> { A , B } C_ Constr )
98 4 5 prssd 
 |-  ( ph -> { G , D } C_ Constr )
99 97 98 unssd 
 |-  ( ph -> ( { A , B } u. { G , D } ) C_ Constr )
100 prfi 
 |-  { A , B } e. Fin
101 100 a1i 
 |-  ( ph -> { A , B } e. Fin )
102 prfi 
 |-  { G , D } e. Fin
103 102 a1i 
 |-  ( ph -> { G , D } e. Fin )
104 101 103 unfid 
 |-  ( ph -> ( { A , B } u. { G , D } ) e. Fin )
105 1 99 104 constrfiss 
 |-  ( ph -> E. n e. _om ( { A , B } u. { G , D } ) C_ ( C ` n ) )
106 96 105 r19.29a 
 |-  ( ph -> X e. Constr )