Metamath Proof Explorer

Theorem constrsdrg

Description: Constructible numbers form a subfield of the complex numbers. (Contributed by Thierry Arnoux, 5-Nov-2025)

Ref Expression
Assertion constrsdrg 
|- Constr e. ( SubDRing ` CCfld )

Proof

Step Hyp Ref Expression
1 cnfldfld 
 |-  CCfld e. Field
2 1 a1i 
 |-  ( T. -> CCfld e. Field )
3 2 flddrngd 
 |-  ( T. -> CCfld e. DivRing )
4 3 drngringd 
 |-  ( T. -> CCfld e. Ring )
5 3 drnggrpd 
 |-  ( T. -> CCfld e. Grp )
6 simpr 
 |-  ( ( T. /\ x e. Constr ) -> x e. Constr )
7 6 constrcn 
 |-  ( ( T. /\ x e. Constr ) -> x e. CC )
8 7 ex 
 |-  ( T. -> ( x e. Constr -> x e. CC ) )
9 8 ssrdv 
 |-  ( T. -> Constr C_ CC )
10 1zzd 
 |-  ( T. -> 1 e. ZZ )
11 10 zconstr 
 |-  ( T. -> 1 e. Constr )
12 11 ne0d 
 |-  ( T. -> Constr =/= (/) )
13 simplr 
 |-  ( ( ( T. /\ x e. Constr ) /\ y e. Constr ) -> x e. Constr )
14 simpr 
 |-  ( ( ( T. /\ x e. Constr ) /\ y e. Constr ) -> y e. Constr )
15 13 14 constraddcl 
 |-  ( ( ( T. /\ x e. Constr ) /\ y e. Constr ) -> ( x + y ) e. Constr )
16 15 ralrimiva 
 |-  ( ( T. /\ x e. Constr ) -> A. y e. Constr ( x + y ) e. Constr )
17 cnfldneg 
 |-  ( x e. CC -> ( ( invg ` CCfld ) ` x ) = -u x )
18 7 17 syl 
 |-  ( ( T. /\ x e. Constr ) -> ( ( invg ` CCfld ) ` x ) = -u x )
19 6 constrnegcl 
 |-  ( ( T. /\ x e. Constr ) -> -u x e. Constr )
20 18 19 eqeltrd 
 |-  ( ( T. /\ x e. Constr ) -> ( ( invg ` CCfld ) ` x ) e. Constr )
21 16 20 jca 
 |-  ( ( T. /\ x e. Constr ) -> ( A. y e. Constr ( x + y ) e. Constr /\ ( ( invg ` CCfld ) ` x ) e. Constr ) )
22 21 ralrimiva 
 |-  ( T. -> A. x e. Constr ( A. y e. Constr ( x + y ) e. Constr /\ ( ( invg ` CCfld ) ` x ) e. Constr ) )
23 cnfldbas 
 |-  CC = ( Base ` CCfld )
24 cnfldadd 
 |-  + = ( +g ` CCfld )
25 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
26 23 24 25 issubg2 
 |-  ( CCfld e. Grp -> ( Constr e. ( SubGrp ` CCfld ) <-> ( Constr C_ CC /\ Constr =/= (/) /\ A. x e. Constr ( A. y e. Constr ( x + y ) e. Constr /\ ( ( invg ` CCfld ) ` x ) e. Constr ) ) ) )
27 26 biimpar 
 |-  ( ( CCfld e. Grp /\ ( Constr C_ CC /\ Constr =/= (/) /\ A. x e. Constr ( A. y e. Constr ( x + y ) e. Constr /\ ( ( invg ` CCfld ) ` x ) e. Constr ) ) ) -> Constr e. ( SubGrp ` CCfld ) )
28 5 9 12 22 27 syl13anc 
 |-  ( T. -> Constr e. ( SubGrp ` CCfld ) )
29 13 14 constrmulcl 
 |-  ( ( ( T. /\ x e. Constr ) /\ y e. Constr ) -> ( x x. y ) e. Constr )
30 29 anasss 
 |-  ( ( T. /\ ( x e. Constr /\ y e. Constr ) ) -> ( x x. y ) e. Constr )
31 30 ralrimivva 
 |-  ( T. -> A. x e. Constr A. y e. Constr ( x x. y ) e. Constr )
32 cnfld1 
 |-  1 = ( 1r ` CCfld )
33 cnfldmul 
 |-  x. = ( .r ` CCfld )
34 23 32 33 issubrg2 
 |-  ( CCfld e. Ring -> ( Constr e. ( SubRing ` CCfld ) <-> ( Constr e. ( SubGrp ` CCfld ) /\ 1 e. Constr /\ A. x e. Constr A. y e. Constr ( x x. y ) e. Constr ) ) )
35 34 biimpar 
 |-  ( ( CCfld e. Ring /\ ( Constr e. ( SubGrp ` CCfld ) /\ 1 e. Constr /\ A. x e. Constr A. y e. Constr ( x x. y ) e. Constr ) ) -> Constr e. ( SubRing ` CCfld ) )
36 4 28 11 31 35 syl13anc 
 |-  ( T. -> Constr e. ( SubRing ` CCfld ) )
37 simpr 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> x e. ( Constr \ { 0 } ) )
38 37 eldifad 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> x e. Constr )
39 38 constrcn 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> x e. CC )
40 eldifsni 
 |-  ( x e. ( Constr \ { 0 } ) -> x =/= 0 )
41 40 adantl 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> x =/= 0 )
42 cnfldinv 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
43 39 41 42 syl2anc 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> ( ( invr ` CCfld ) ` x ) = ( 1 / x ) )
44 38 41 constrinvcl 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> ( 1 / x ) e. Constr )
45 43 44 eqeltrd 
 |-  ( ( T. /\ x e. ( Constr \ { 0 } ) ) -> ( ( invr ` CCfld ) ` x ) e. Constr )
46 45 ralrimiva 
 |-  ( T. -> A. x e. ( Constr \ { 0 } ) ( ( invr ` CCfld ) ` x ) e. Constr )
47 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
48 cnfld0 
 |-  0 = ( 0g ` CCfld )
49 47 48 issdrg2 
 |-  ( Constr e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ Constr e. ( SubRing ` CCfld ) /\ A. x e. ( Constr \ { 0 } ) ( ( invr ` CCfld ) ` x ) e. Constr ) )
50 3 36 46 49 syl3anbrc 
 |-  ( T. -> Constr e. ( SubDRing ` CCfld ) )
51 50 mptru 
 |-  Constr e. ( SubDRing ` CCfld )