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 ∈ SubDRing ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 cnfldfld ⊢ ℂ fld ∈ Field
2 1 a1i ⊢ ⊤ → ℂ fld ∈ Field
3 2 flddrngd ⊢ ⊤ → ℂ fld ∈ DivRing
4 3 drngringd ⊢ ⊤ → ℂ fld ∈ Ring
5 3 drnggrpd ⊢ ⊤ → ℂ fld ∈ Grp
6 simpr ⊢ ⊤ ∧ x ∈ Constr → x ∈ Constr
7 6 constrcn ⊢ ⊤ ∧ x ∈ Constr → x ∈ ℂ
8 7 ex ⊢ ⊤ → x ∈ Constr → x ∈ ℂ
9 8 ssrdv ⊢ ⊤ → Constr ⊆ ℂ
10 1zzd ⊢ ⊤ → 1 ∈ ℤ
11 10 zconstr ⊢ ⊤ → 1 ∈ Constr
12 11 ne0d ⊢ ⊤ → Constr ≠ ∅
13 simplr ⊢ ⊤ ∧ x ∈ Constr ∧ y ∈ Constr → x ∈ Constr
14 simpr ⊢ ⊤ ∧ x ∈ Constr ∧ y ∈ Constr → y ∈ Constr
15 13 14 constraddcl ⊢ ⊤ ∧ x ∈ Constr ∧ y ∈ Constr → x + y ∈ Constr
16 15 ralrimiva ⊢ ⊤ ∧ x ∈ Constr → ∀ y ∈ Constr x + y ∈ Constr
17 cnfldneg ⊢ x ∈ ℂ → inv g ⁡ ℂ fld ⁡ x = − x
18 7 17 syl ⊢ ⊤ ∧ x ∈ Constr → inv g ⁡ ℂ fld ⁡ x = − x
19 6 constrnegcl ⊢ ⊤ ∧ x ∈ Constr → − x ∈ Constr
20 18 19 eqeltrd ⊢ ⊤ ∧ x ∈ Constr → inv g ⁡ ℂ fld ⁡ x ∈ Constr
21 16 20 jca ⊢ ⊤ ∧ x ∈ Constr → ∀ y ∈ Constr x + y ∈ Constr ∧ inv g ⁡ ℂ fld ⁡ x ∈ Constr
22 21 ralrimiva ⊢ ⊤ → ∀ x ∈ Constr ∀ y ∈ Constr x + y ∈ Constr ∧ inv g ⁡ ℂ fld ⁡ x ∈ Constr
23 cnfldbas ⊢ ℂ = Base ℂ fld
24 cnfldadd ⊢ + = + ℂ fld
25 eqid ⊢ inv g ⁡ ℂ fld = inv g ⁡ ℂ fld
26 23 24 25 issubg2 ⊢ ℂ fld ∈ Grp → Constr ∈ SubGrp ⁡ ℂ fld ↔ Constr ⊆ ℂ ∧ Constr ≠ ∅ ∧ ∀ x ∈ Constr ∀ y ∈ Constr x + y ∈ Constr ∧ inv g ⁡ ℂ fld ⁡ x ∈ Constr
27 26 biimpar ⊢ ℂ fld ∈ Grp ∧ Constr ⊆ ℂ ∧ Constr ≠ ∅ ∧ ∀ x ∈ Constr ∀ y ∈ Constr x + y ∈ Constr ∧ inv g ⁡ ℂ fld ⁡ x ∈ Constr → Constr ∈ SubGrp ⁡ ℂ fld
28 5 9 12 22 27 syl13anc ⊢ ⊤ → Constr ∈ SubGrp ⁡ ℂ fld
29 13 14 constrmulcl ⊢ ⊤ ∧ x ∈ Constr ∧ y ∈ Constr → x ⁢ y ∈ Constr
30 29 anasss ⊢ ⊤ ∧ x ∈ Constr ∧ y ∈ Constr → x ⁢ y ∈ Constr
31 30 ralrimivva ⊢ ⊤ → ∀ x ∈ Constr ∀ y ∈ Constr x ⁢ y ∈ Constr
32 cnfld1 ⊢ 1 = 1 ℂ fld
33 cnfldmul ⊢ × = ⋅ ℂ fld
34 23 32 33 issubrg2 ⊢ ℂ fld ∈ Ring → Constr ∈ SubRing ⁡ ℂ fld ↔ Constr ∈ SubGrp ⁡ ℂ fld ∧ 1 ∈ Constr ∧ ∀ x ∈ Constr ∀ y ∈ Constr x ⁢ y ∈ Constr
35 34 biimpar ⊢ ℂ fld ∈ Ring ∧ Constr ∈ SubGrp ⁡ ℂ fld ∧ 1 ∈ Constr ∧ ∀ x ∈ Constr ∀ y ∈ Constr x ⁢ y ∈ Constr → Constr ∈ SubRing ⁡ ℂ fld
36 4 28 11 31 35 syl13anc ⊢ ⊤ → Constr ∈ SubRing ⁡ ℂ fld
37 simpr ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → x ∈ Constr ∖ 0
38 37 eldifad ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → x ∈ Constr
39 38 constrcn ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → x ∈ ℂ
40 eldifsni ⊢ x ∈ Constr ∖ 0 → x ≠ 0
41 40 adantl ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → x ≠ 0
42 cnfldinv ⊢ x ∈ ℂ ∧ x ≠ 0 → inv r ⁡ ℂ fld ⁡ x = 1 x
43 39 41 42 syl2anc ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → inv r ⁡ ℂ fld ⁡ x = 1 x
44 38 41 constrinvcl ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → 1 x ∈ Constr
45 43 44 eqeltrd ⊢ ⊤ ∧ x ∈ Constr ∖ 0 → inv r ⁡ ℂ fld ⁡ x ∈ Constr
46 45 ralrimiva ⊢ ⊤ → ∀ x ∈ Constr ∖ 0 inv r ⁡ ℂ fld ⁡ x ∈ Constr
47 eqid ⊢ inv r ⁡ ℂ fld = inv r ⁡ ℂ fld
48 cnfld0 ⊢ 0 = 0 ℂ fld
49 47 48 issdrg2 ⊢ Constr ∈ SubDRing ⁡ ℂ fld ↔ ℂ fld ∈ DivRing ∧ Constr ∈ SubRing ⁡ ℂ fld ∧ ∀ x ∈ Constr ∖ 0 inv r ⁡ ℂ fld ⁡ x ∈ Constr
50 3 36 46 49 syl3anbrc ⊢ ⊤ → Constr ∈ SubDRing ⁡ ℂ fld
51 50 mptru ⊢ Constr ∈ SubDRing ⁡ ℂ fld