Metamath Proof Explorer

Theorem constrextdg2

Description: Any step ( CN ) of the construction of constructible numbers is contained in the last field of a tower of quadratic field extensions starting with QQ . (Contributed by Thierry Arnoux, 19-Oct-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 } )
constrextdg2.1 
|- E = ( CCfld |`s e )
constrextdg2.2 
|- F = ( CCfld |`s f )
constrextdg2.l 
|- .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
constrextdg2.n 
|- ( ph -> N e. _om )
Assertion constrextdg2 
|- ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` N ) C_ ( lastS ` v ) ) )

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 constrextdg2.1 
 |-  E = ( CCfld |`s e )
3 constrextdg2.2 
 |-  F = ( CCfld |`s f )
4 constrextdg2.l 
 |-  .< = { <. f , e >. | ( E /FldExt F /\ ( E [:] F ) = 2 ) }
5 constrextdg2.n 
 |-  ( ph -> N e. _om )
6 fveq2 
 |-  ( m = (/) -> ( C ` m ) = ( C ` (/) ) )
7 6 sseq1d 
 |-  ( m = (/) -> ( ( C ` m ) C_ ( lastS ` v ) <-> ( C ` (/) ) C_ ( lastS ` v ) ) )
8 7 anbi2d 
 |-  ( m = (/) -> ( ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` v ) ) ) )
9 8 rexbidv 
 |-  ( m = (/) -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` v ) ) ) )
10 fveq2 
 |-  ( m = n -> ( C ` m ) = ( C ` n ) )
11 10 sseq1d 
 |-  ( m = n -> ( ( C ` m ) C_ ( lastS ` v ) <-> ( C ` n ) C_ ( lastS ` v ) ) )
12 11 anbi2d 
 |-  ( m = n -> ( ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` v ) ) ) )
13 12 rexbidv 
 |-  ( m = n -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` v ) ) ) )
14 fveq1 
 |-  ( v = u -> ( v ` 0 ) = ( u ` 0 ) )
15 14 eqeq1d 
 |-  ( v = u -> ( ( v ` 0 ) = QQ <-> ( u ` 0 ) = QQ ) )
16 fveq2 
 |-  ( v = u -> ( lastS ` v ) = ( lastS ` u ) )
17 16 sseq2d 
 |-  ( v = u -> ( ( C ` n ) C_ ( lastS ` v ) <-> ( C ` n ) C_ ( lastS ` u ) ) )
18 15 17 anbi12d 
 |-  ( v = u -> ( ( ( v ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` v ) ) <-> ( ( u ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` u ) ) ) )
19 18 cbvrexvw 
 |-  ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` v ) ) <-> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` u ) ) )
20 13 19 bitrdi 
 |-  ( m = n -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` u ) ) ) )
21 fveq2 
 |-  ( m = suc n -> ( C ` m ) = ( C ` suc n ) )
22 21 sseq1d 
 |-  ( m = suc n -> ( ( C ` m ) C_ ( lastS ` v ) <-> ( C ` suc n ) C_ ( lastS ` v ) ) )
23 22 anbi2d 
 |-  ( m = suc n -> ( ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( C ` suc n ) C_ ( lastS ` v ) ) ) )
24 23 rexbidv 
 |-  ( m = suc n -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc n ) C_ ( lastS ` v ) ) ) )
25 fveq2 
 |-  ( m = N -> ( C ` m ) = ( C ` N ) )
26 25 sseq1d 
 |-  ( m = N -> ( ( C ` m ) C_ ( lastS ` v ) <-> ( C ` N ) C_ ( lastS ` v ) ) )
27 26 anbi2d 
 |-  ( m = N -> ( ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> ( ( v ` 0 ) = QQ /\ ( C ` N ) C_ ( lastS ` v ) ) ) )
28 27 rexbidv 
 |-  ( m = N -> ( E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` m ) C_ ( lastS ` v ) ) <-> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` N ) C_ ( lastS ` v ) ) ) )
29 fveq1 
 |-  ( v = <" QQ "> -> ( v ` 0 ) = ( <" QQ "> ` 0 ) )
30 29 eqeq1d 
 |-  ( v = <" QQ "> -> ( ( v ` 0 ) = QQ <-> ( <" QQ "> ` 0 ) = QQ ) )
31 fveq2 
 |-  ( v = <" QQ "> -> ( lastS ` v ) = ( lastS ` <" QQ "> ) )
32 31 sseq2d 
 |-  ( v = <" QQ "> -> ( ( C ` (/) ) C_ ( lastS ` v ) <-> ( C ` (/) ) C_ ( lastS ` <" QQ "> ) ) )
33 30 32 anbi12d 
 |-  ( v = <" QQ "> -> ( ( ( v ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` v ) ) <-> ( ( <" QQ "> ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` <" QQ "> ) ) ) )
34 cndrng 
 |-  CCfld e. DivRing
35 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
36 35 simpli 
 |-  QQ e. ( SubRing ` CCfld )
37 35 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
38 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
39 34 36 37 38 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
40 39 a1i 
 |-  ( T. -> QQ e. ( SubDRing ` CCfld ) )
41 40 s1chn 
 |-  ( T. -> <" QQ "> e. ( .< Chain ( SubDRing ` CCfld ) ) )
42 s1fv 
 |-  ( QQ e. ( SubDRing ` CCfld ) -> ( <" QQ "> ` 0 ) = QQ )
43 40 42 syl 
 |-  ( T. -> ( <" QQ "> ` 0 ) = QQ )
44 0z 
 |-  0 e. ZZ
45 1z 
 |-  1 e. ZZ
46 prssi 
 |-  ( ( 0 e. ZZ /\ 1 e. ZZ ) -> { 0 , 1 } C_ ZZ )
47 44 45 46 mp2an 
 |-  { 0 , 1 } C_ ZZ
48 zssq 
 |-  ZZ C_ QQ
49 47 48 sstri 
 |-  { 0 , 1 } C_ QQ
50 1 constr0 
 |-  ( C ` (/) ) = { 0 , 1 }
51 lsws1 
 |-  ( QQ e. ( SubDRing ` CCfld ) -> ( lastS ` <" QQ "> ) = QQ )
52 39 51 ax-mp 
 |-  ( lastS ` <" QQ "> ) = QQ
53 49 50 52 3sstr4i 
 |-  ( C ` (/) ) C_ ( lastS ` <" QQ "> )
54 43 53 jctir 
 |-  ( T. -> ( ( <" QQ "> ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` <" QQ "> ) ) )
55 33 41 54 rspcedvdw 
 |-  ( T. -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` v ) ) )
56 55 mptru 
 |-  E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` (/) ) C_ ( lastS ` v ) )
57 simplll 
 |-  ( ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( u ` 0 ) = QQ ) /\ ( C ` n ) C_ ( lastS ` u ) ) -> n e. _om )
58 simpllr 
 |-  ( ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( u ` 0 ) = QQ ) /\ ( C ` n ) C_ ( lastS ` u ) ) -> u e. ( .< Chain ( SubDRing ` CCfld ) ) )
59 simplr 
 |-  ( ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( u ` 0 ) = QQ ) /\ ( C ` n ) C_ ( lastS ` u ) ) -> ( u ` 0 ) = QQ )
60 simpr 
 |-  ( ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( u ` 0 ) = QQ ) /\ ( C ` n ) C_ ( lastS ` u ) ) -> ( C ` n ) C_ ( lastS ` u ) )
61 1 2 3 4 57 58 59 60 constrextdg2lem 
 |-  ( ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( u ` 0 ) = QQ ) /\ ( C ` n ) C_ ( lastS ` u ) ) -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc n ) C_ ( lastS ` v ) ) )
62 61 anasss 
 |-  ( ( ( n e. _om /\ u e. ( .< Chain ( SubDRing ` CCfld ) ) ) /\ ( ( u ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` u ) ) ) -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc n ) C_ ( lastS ` v ) ) )
63 62 rexlimdva2 
 |-  ( n e. _om -> ( E. u e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( u ` 0 ) = QQ /\ ( C ` n ) C_ ( lastS ` u ) ) -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` suc n ) C_ ( lastS ` v ) ) ) )
64 9 20 24 28 56 63 finds 
 |-  ( N e. _om -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` N ) C_ ( lastS ` v ) ) )
65 5 64 syl 
 |-  ( ph -> E. v e. ( .< Chain ( SubDRing ` CCfld ) ) ( ( v ` 0 ) = QQ /\ ( C ` N ) C_ ( lastS ` v ) ) )