Theorem constrcjcl

Description: Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025)

	Ref	Expression
Hypothesis	constrcjcl.1	|- ( ph -> X e. Constr )
Assertion	constrcjcl	|- ( ph -> ( * ` X ) e. Constr )

Proof

Step	Hyp	Ref	Expression
1		constrcjcl.1	|- ( ph -> X e. Constr )
2		constrcbvlem	|- rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = 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 } )
3	2	isconstr	|- ( X e. Constr <-> E. n e. _om X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
4	1 3	sylib	|- ( ph -> E. n e. _om X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
5		nnon	|- ( n e. _om -> n e. On )
6	5	ad2antlr	|- ( ( ( ph /\ n e. _om ) /\ X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) ) -> n e. On )
7		simpr	|- ( ( ( ph /\ n e. _om ) /\ X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) ) -> X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
8	2 6 7	constrconj	|- ( ( ( ph /\ n e. _om ) /\ X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) ) -> ( * ` X ) e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
9	8	ex	|- ( ( ph /\ n e. _om ) -> ( X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) -> ( * ` X ) e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) ) )
10	9	reximdva	|- ( ph -> ( E. n e. _om X e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) -> E. n e. _om ( * ` X ) e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) ) )
11	4 10	mpd	|- ( ph -> E. n e. _om ( * ` X ) e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
12	2	isconstr	|- ( ( * ` X ) e. Constr <-> E. n e. _om ( * ` X ) e. ( rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) ` n ) )
13	11 12	sylibr	|- ( ph -> ( * ` X ) e. Constr )