Step |
Hyp |
Ref |
Expression |
0 |
|
cconstr |
|- Constr |
1 |
|
vs |
|- s |
2 |
|
cvv |
|- _V |
3 |
|
vx |
|- x |
4 |
|
cc |
|- CC |
5 |
|
va |
|- a |
6 |
1
|
cv |
|- s |
7 |
|
vb |
|- b |
8 |
|
vc |
|- c |
9 |
|
vd |
|- d |
10 |
|
vt |
|- t |
11 |
|
cr |
|- RR |
12 |
|
vr |
|- r |
13 |
3
|
cv |
|- x |
14 |
5
|
cv |
|- a |
15 |
|
caddc |
|- + |
16 |
10
|
cv |
|- t |
17 |
|
cmul |
|- x. |
18 |
7
|
cv |
|- b |
19 |
|
cmin |
|- - |
20 |
18 14 19
|
co |
|- ( b - a ) |
21 |
16 20 17
|
co |
|- ( t x. ( b - a ) ) |
22 |
14 21 15
|
co |
|- ( a + ( t x. ( b - a ) ) ) |
23 |
13 22
|
wceq |
|- x = ( a + ( t x. ( b - a ) ) ) |
24 |
8
|
cv |
|- c |
25 |
12
|
cv |
|- r |
26 |
9
|
cv |
|- d |
27 |
26 24 19
|
co |
|- ( d - c ) |
28 |
25 27 17
|
co |
|- ( r x. ( d - c ) ) |
29 |
24 28 15
|
co |
|- ( c + ( r x. ( d - c ) ) ) |
30 |
13 29
|
wceq |
|- x = ( c + ( r x. ( d - c ) ) ) |
31 |
|
cim |
|- Im |
32 |
|
ccj |
|- * |
33 |
20 32
|
cfv |
|- ( * ` ( b - a ) ) |
34 |
33 27 17
|
co |
|- ( ( * ` ( b - a ) ) x. ( d - c ) ) |
35 |
34 31
|
cfv |
|- ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) |
36 |
|
cc0 |
|- 0 |
37 |
35 36
|
wne |
|- ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 |
38 |
23 30 37
|
w3a |
|- ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) |
39 |
38 12 11
|
wrex |
|- E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) |
40 |
39 10 11
|
wrex |
|- 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 ) |
41 |
40 9 6
|
wrex |
|- 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 ) |
42 |
41 8 6
|
wrex |
|- 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 ) |
43 |
42 7 6
|
wrex |
|- 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 ) |
44 |
43 5 6
|
wrex |
|- 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 ) |
45 |
|
ve |
|- e |
46 |
|
vf |
|- f |
47 |
|
cabs |
|- abs |
48 |
13 24 19
|
co |
|- ( x - c ) |
49 |
48 47
|
cfv |
|- ( abs ` ( x - c ) ) |
50 |
45
|
cv |
|- e |
51 |
46
|
cv |
|- f |
52 |
50 51 19
|
co |
|- ( e - f ) |
53 |
52 47
|
cfv |
|- ( abs ` ( e - f ) ) |
54 |
49 53
|
wceq |
|- ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) |
55 |
23 54
|
wa |
|- ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) |
56 |
55 10 11
|
wrex |
|- E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) |
57 |
56 46 6
|
wrex |
|- E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) |
58 |
57 45 6
|
wrex |
|- E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) |
59 |
58 8 6
|
wrex |
|- 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 ) ) ) |
60 |
59 7 6
|
wrex |
|- 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 ) ) ) |
61 |
60 5 6
|
wrex |
|- 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 ) ) ) |
62 |
14 26
|
wne |
|- a =/= d |
63 |
13 14 19
|
co |
|- ( x - a ) |
64 |
63 47
|
cfv |
|- ( abs ` ( x - a ) ) |
65 |
18 24 19
|
co |
|- ( b - c ) |
66 |
65 47
|
cfv |
|- ( abs ` ( b - c ) ) |
67 |
64 66
|
wceq |
|- ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) |
68 |
13 26 19
|
co |
|- ( x - d ) |
69 |
68 47
|
cfv |
|- ( abs ` ( x - d ) ) |
70 |
69 53
|
wceq |
|- ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) |
71 |
62 67 70
|
w3a |
|- ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) |
72 |
71 46 6
|
wrex |
|- E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) |
73 |
72 45 6
|
wrex |
|- E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) |
74 |
73 9 6
|
wrex |
|- 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 ) ) ) |
75 |
74 8 6
|
wrex |
|- 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 ) ) ) |
76 |
75 7 6
|
wrex |
|- 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 ) ) ) |
77 |
76 5 6
|
wrex |
|- 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 ) ) ) |
78 |
44 61 77
|
w3o |
|- ( 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 ) ) ) ) |
79 |
78 3 4
|
crab |
|- { 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 ) ) ) ) } |
80 |
1 2 79
|
cmpt |
|- ( 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 ) ) ) ) } ) |
81 |
|
c1 |
|- 1 |
82 |
36 81
|
cpr |
|- { 0 , 1 } |
83 |
80 82
|
crdg |
|- 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 } ) |
84 |
|
com |
|- _om |
85 |
83 84
|
cima |
|- ( 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 } ) " _om ) |
86 |
0 85
|
wceq |
|- Constr = ( 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 } ) " _om ) |