Metamath Proof Explorer

Theorem constrlccllem

Description: Constructible numbers are closed under line-circle 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 } )
constrlccllem.a 
|- ( ph -> A e. Constr )
constrlccllem.b 
|- ( ph -> B e. Constr )
constrlccllem.c 
|- ( ph -> G e. Constr )
constrlccllem.e 
|- ( ph -> E e. Constr )
constrlccllem.f 
|- ( ph -> F e. Constr )
constrlccllem.t 
|- ( ph -> T e. RR )
constrlccllem.x 
|- ( ph -> X e. CC )
constrlccllem.1 
|- ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
constrlccllem.2 
|- ( ph -> ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) )
Assertion constrlccllem 
|- ( 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 constrlccllem.a 
 |-  ( ph -> A e. Constr )
3 constrlccllem.b 
 |-  ( ph -> B e. Constr )
4 constrlccllem.c 
 |-  ( ph -> G e. Constr )
5 constrlccllem.e 
 |-  ( ph -> E e. Constr )
6 constrlccllem.f 
 |-  ( ph -> F e. Constr )
7 constrlccllem.t 
 |-  ( ph -> T e. RR )
8 constrlccllem.x 
 |-  ( ph -> X e. CC )
9 constrlccllem.1 
 |-  ( ph -> X = ( A + ( T x. ( B - A ) ) ) )
10 constrlccllem.2 
 |-  ( ph -> ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) )
11 peano2b 
 |-  ( n e. _om <-> suc n e. _om )
12 11 biimpi 
 |-  ( n e. _om -> suc n e. _om )
13 12 ad2antlr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> suc n e. _om )
14 fveq2 
 |-  ( m = suc n -> ( C ` m ) = ( C ` suc n ) )
15 14 eleq2d 
 |-  ( m = suc n -> ( X e. ( C ` m ) <-> X e. ( C ` suc n ) ) )
16 15 adantl 
 |-  ( ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) /\ m = suc n ) -> ( X e. ( C ` m ) <-> X e. ( C ` suc n ) ) )
17 8 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> X e. CC )
18 id 
 |-  ( a = A -> a = A )
19 oveq2 
 |-  ( a = A -> ( b - a ) = ( b - A ) )
20 19 oveq2d 
 |-  ( a = A -> ( t x. ( b - a ) ) = ( t x. ( b - A ) ) )
21 18 20 oveq12d 
 |-  ( a = A -> ( a + ( t x. ( b - a ) ) ) = ( A + ( t x. ( b - A ) ) ) )
22 21 eqeq2d 
 |-  ( a = A -> ( X = ( a + ( t x. ( b - a ) ) ) <-> X = ( A + ( t x. ( b - A ) ) ) ) )
23 22 anbi1d 
 |-  ( a = A -> ( ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> ( X = ( A + ( t x. ( b - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
24 23 rexbidv 
 |-  ( a = A -> ( E. t e. RR ( X = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> E. t e. RR ( X = ( A + ( t x. ( b - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
25 24 2rexbidv 
 |-  ( a = A -> ( 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. 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 ) ) ) ) )
26 oveq1 
 |-  ( b = B -> ( b - A ) = ( B - A ) )
27 26 oveq2d 
 |-  ( b = B -> ( t x. ( b - A ) ) = ( t x. ( B - A ) ) )
28 27 oveq2d 
 |-  ( b = B -> ( A + ( t x. ( b - A ) ) ) = ( A + ( t x. ( B - A ) ) ) )
29 28 eqeq2d 
 |-  ( b = B -> ( X = ( A + ( t x. ( b - A ) ) ) <-> X = ( A + ( t x. ( B - A ) ) ) ) )
30 29 anbi1d 
 |-  ( b = B -> ( ( X = ( A + ( t x. ( b - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
31 30 rexbidv 
 |-  ( b = B -> ( E. t e. RR ( X = ( A + ( t x. ( b - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> E. t e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) ) )
32 31 2rexbidv 
 |-  ( b = B -> ( 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. 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 ) ) ) ) )
33 oveq2 
 |-  ( c = G -> ( X - c ) = ( X - G ) )
34 33 fveq2d 
 |-  ( c = G -> ( abs ` ( X - c ) ) = ( abs ` ( X - G ) ) )
35 34 eqeq1d 
 |-  ( c = G -> ( ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) )
36 35 anbi2d 
 |-  ( c = G -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) ) )
37 36 rexbidv 
 |-  ( c = G -> ( E. t e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - c ) ) = ( abs ` ( e - f ) ) ) <-> E. t e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) ) )
38 37 2rexbidv 
 |-  ( c = G -> ( 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. e e. ( C ` n ) E. f e. ( C ` n ) E. t e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) ) )
39 2 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> A e. Constr )
40 simpr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> ( { A , B , G } u. { E , F } ) C_ ( C ` n ) )
41 40 unssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> { A , B , G } C_ ( C ` n ) )
42 39 41 tpssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> A e. ( C ` n ) )
43 3 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> B e. Constr )
44 43 41 tpssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> B e. ( C ` n ) )
45 4 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> G e. Constr )
46 45 41 tpsscd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> G e. ( C ` n ) )
47 oveq1 
 |-  ( e = E -> ( e - f ) = ( E - f ) )
48 47 fveq2d 
 |-  ( e = E -> ( abs ` ( e - f ) ) = ( abs ` ( E - f ) ) )
49 48 eqeq2d 
 |-  ( e = E -> ( ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( X - G ) ) = ( abs ` ( E - f ) ) ) )
50 49 anbi2d 
 |-  ( e = E -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) <-> ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - f ) ) ) ) )
51 oveq2 
 |-  ( f = F -> ( E - f ) = ( E - F ) )
52 51 fveq2d 
 |-  ( f = F -> ( abs ` ( E - f ) ) = ( abs ` ( E - F ) ) )
53 52 eqeq2d 
 |-  ( f = F -> ( ( abs ` ( X - G ) ) = ( abs ` ( E - f ) ) <-> ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) ) )
54 53 anbi2d 
 |-  ( f = F -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - f ) ) ) <-> ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) ) ) )
55 oveq1 
 |-  ( t = T -> ( t x. ( B - A ) ) = ( T x. ( B - A ) ) )
56 55 oveq2d 
 |-  ( t = T -> ( A + ( t x. ( B - A ) ) ) = ( A + ( T x. ( B - A ) ) ) )
57 56 eqeq2d 
 |-  ( t = T -> ( X = ( A + ( t x. ( B - A ) ) ) <-> X = ( A + ( T x. ( B - A ) ) ) ) )
58 57 anbi1d 
 |-  ( t = T -> ( ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) ) <-> ( X = ( A + ( T x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) ) ) )
59 5 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> E e. Constr )
60 40 unssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> { E , F } C_ ( C ` n ) )
61 59 60 prssad 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> E e. ( C ` n ) )
62 6 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> F e. Constr )
63 62 60 prssbd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> F e. ( C ` n ) )
64 7 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> T e. RR )
65 9 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> X = ( A + ( T x. ( B - A ) ) ) )
66 10 ad2antrr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) )
67 65 66 jca 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> ( X = ( A + ( T x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( E - F ) ) ) )
68 50 54 58 61 63 64 67 3rspcedvdw 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> E. e e. ( C ` n ) E. f e. ( C ` n ) E. t e. RR ( X = ( A + ( t x. ( B - A ) ) ) /\ ( abs ` ( X - G ) ) = ( abs ` ( e - f ) ) ) )
69 25 32 38 42 44 46 68 3rspcedvdw 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> 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 ) ) ) )
70 69 3mix2d 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) 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 ) ) ) ) )
71 nnon 
 |-  ( n e. _om -> n e. On )
72 71 ad2antlr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> n e. On )
73 eqid 
 |-  ( C ` n ) = ( C ` n )
74 1 72 73 constrsuc 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) 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 ) ) ) ) ) ) )
75 17 70 74 mpbir2and 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> X e. ( C ` suc n ) )
76 13 16 75 rspcedvd 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> E. m e. _om X e. ( C ` m ) )
77 1 isconstr 
 |-  ( X e. Constr <-> E. m e. _om X e. ( C ` m ) )
78 76 77 sylibr 
 |-  ( ( ( ph /\ n e. _om ) /\ ( { A , B , G } u. { E , F } ) C_ ( C ` n ) ) -> X e. Constr )
79 2 3 4 tpssd 
 |-  ( ph -> { A , B , G } C_ Constr )
80 5 6 prssd 
 |-  ( ph -> { E , F } C_ Constr )
81 79 80 unssd 
 |-  ( ph -> ( { A , B , G } u. { E , F } ) C_ Constr )
82 tpfi 
 |-  { A , B , G } e. Fin
83 82 a1i 
 |-  ( ph -> { A , B , G } e. Fin )
84 prfi 
 |-  { E , F } e. Fin
85 84 a1i 
 |-  ( ph -> { E , F } e. Fin )
86 83 85 unfid 
 |-  ( ph -> ( { A , B , G } u. { E , F } ) e. Fin )
87 1 81 86 constrfiss 
 |-  ( ph -> E. n e. _om ( { A , B , G } u. { E , F } ) C_ ( C ` n ) )
88 78 87 r19.29a 
 |-  ( ph -> X e. Constr )