Metamath Proof Explorer

Theorem constrcccllem

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