Metamath Proof Explorer

Theorem constrext2chn

Description: If a constructible number generates some subfield L of CC , then the degree of the extension of L over QQ is a power of two. Theorem 7.12 of Stewart p. 98. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses constrext2chn.q 
|- Q = ( CCfld |`s QQ )
constrext2chn.l 
|- L = ( CCfld |`s S )
constrext2chn.s 
|- S = ( CCfld fldGen ( QQ u. { A } ) )
constrext2chn.a 
|- ( ph -> A e. Constr )
Assertion constrext2chn 
|- ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )

Proof

Step Hyp Ref Expression
1 constrext2chn.q 
 |-  Q = ( CCfld |`s QQ )
2 constrext2chn.l 
 |-  L = ( CCfld |`s S )
3 constrext2chn.s 
 |-  S = ( CCfld fldGen ( QQ u. { A } ) )
4 constrext2chn.a 
 |-  ( ph -> A e. Constr )
5 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 } )
6 eqid 
 |-  ( CCfld |`s e ) = ( CCfld |`s e )
7 eqid 
 |-  ( CCfld |`s f ) = ( CCfld |`s f )
8 oveq2 
 |-  ( h = e -> ( CCfld |`s h ) = ( CCfld |`s e ) )
9 8 adantl 
 |-  ( ( g = f /\ h = e ) -> ( CCfld |`s h ) = ( CCfld |`s e ) )
10 oveq2 
 |-  ( g = f -> ( CCfld |`s g ) = ( CCfld |`s f ) )
11 10 adantr 
 |-  ( ( g = f /\ h = e ) -> ( CCfld |`s g ) = ( CCfld |`s f ) )
12 9 11 breq12d 
 |-  ( ( g = f /\ h = e ) -> ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) <-> ( CCfld |`s e ) /FldExt ( CCfld |`s f ) ) )
13 9 11 oveq12d 
 |-  ( ( g = f /\ h = e ) -> ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) )
14 13 eqeq1d 
 |-  ( ( g = f /\ h = e ) -> ( ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 <-> ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) )
15 12 14 anbi12d 
 |-  ( ( g = f /\ h = e ) -> ( ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) /\ ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 ) <-> ( ( CCfld |`s e ) /FldExt ( CCfld |`s f ) /\ ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) ) )
16 15 cbvopabv 
 |-  { <. g , h >. | ( ( CCfld |`s h ) /FldExt ( CCfld |`s g ) /\ ( ( CCfld |`s h ) [:] ( CCfld |`s g ) ) = 2 ) } = { <. f , e >. | ( ( CCfld |`s e ) /FldExt ( CCfld |`s f ) /\ ( ( CCfld |`s e ) [:] ( CCfld |`s f ) ) = 2 ) }
17 peano1 
 |-  (/) e. _om
18 17 a1i 
 |-  ( ph -> (/) e. _om )
19 3 oveq2i 
 |-  ( CCfld |`s S ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
20 2 19 eqtri 
 |-  L = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
21 5 6 7 16 18 1 20 4 constrext2chnlem 
 |-  ( ph -> E. n e. NN0 ( L [:] Q ) = ( 2 ^ n ) )