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 ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → 𝑥 ∈ Constr )
7 6 constrcn ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → 𝑥 ∈ ℂ )
8 7 ex ⊢ ( ⊤ → ( 𝑥 ∈ Constr → 𝑥 ∈ ℂ ) )
9 8 ssrdv ⊢ ( ⊤ → Constr ⊆ ℂ )
10 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
11 10 zconstr ⊢ ( ⊤ → 1 ∈ Constr )
12 11 ne0d ⊢ ( ⊤ → Constr ≠ ∅ )
13 simplr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ Constr ) ∧ 𝑦 ∈ Constr ) → 𝑥 ∈ Constr )
14 simpr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ Constr ) ∧ 𝑦 ∈ Constr ) → 𝑦 ∈ Constr )
15 13 14 constraddcl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ Constr ) ∧ 𝑦 ∈ Constr ) → ( 𝑥 + 𝑦 ) ∈ Constr )
16 15 ralrimiva ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → ∀ 𝑦 ∈ Constr ( 𝑥 + 𝑦 ) ∈ Constr )
17 cnfldneg ⊢ ( 𝑥 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) = - 𝑥 )
18 7 17 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) = - 𝑥 )
19 6 constrnegcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → - 𝑥 ∈ Constr )
20 18 19 eqeltrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr )
21 16 20 jca ⊢ ( ( ⊤ ∧ 𝑥 ∈ Constr ) → ( ∀ 𝑦 ∈ Constr ( 𝑥 + 𝑦 ) ∈ Constr ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr ) )
22 21 ralrimiva ⊢ ( ⊤ → ∀ 𝑥 ∈ Constr ( ∀ 𝑦 ∈ Constr ( 𝑥 + 𝑦 ) ∈ Constr ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr ) )
23 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
24 cnfldadd ⊢ + = ( +g ‘ ℂfld )
25 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
26 23 24 25 issubg2 ⊢ ( ℂfld ∈ Grp → ( Constr ∈ ( SubGrp ‘ ℂfld ) ↔ ( Constr ⊆ ℂ ∧ Constr ≠ ∅ ∧ ∀ 𝑥 ∈ Constr ( ∀ 𝑦 ∈ Constr ( 𝑥 + 𝑦 ) ∈ Constr ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr ) ) ) )
27 26 biimpar ⊢ ( ( ℂfld ∈ Grp ∧ ( Constr ⊆ ℂ ∧ Constr ≠ ∅ ∧ ∀ 𝑥 ∈ Constr ( ∀ 𝑦 ∈ Constr ( 𝑥 + 𝑦 ) ∈ Constr ∧ ( ( invg ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr ) ) ) → Constr ∈ ( SubGrp ‘ ℂfld ) )
28 5 9 12 22 27 syl13anc ⊢ ( ⊤ → Constr ∈ ( SubGrp ‘ ℂfld ) )
29 13 14 constrmulcl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ Constr ) ∧ 𝑦 ∈ Constr ) → ( 𝑥 · 𝑦 ) ∈ Constr )
30 29 anasss ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ Constr ∧ 𝑦 ∈ Constr ) ) → ( 𝑥 · 𝑦 ) ∈ Constr )
31 30 ralrimivva ⊢ ( ⊤ → ∀ 𝑥 ∈ Constr ∀ 𝑦 ∈ Constr ( 𝑥 · 𝑦 ) ∈ Constr )
32 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
33 cnfldmul ⊢ · = ( .r ‘ ℂfld )
34 23 32 33 issubrg2 ⊢ ( ℂfld ∈ Ring → ( Constr ∈ ( SubRing ‘ ℂfld ) ↔ ( Constr ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ Constr ∧ ∀ 𝑥 ∈ Constr ∀ 𝑦 ∈ Constr ( 𝑥 · 𝑦 ) ∈ Constr ) ) )
35 34 biimpar ⊢ ( ( ℂfld ∈ Ring ∧ ( Constr ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ Constr ∧ ∀ 𝑥 ∈ Constr ∀ 𝑦 ∈ Constr ( 𝑥 · 𝑦 ) ∈ Constr ) ) → Constr ∈ ( SubRing ‘ ℂfld ) )
36 4 28 11 31 35 syl13anc ⊢ ( ⊤ → Constr ∈ ( SubRing ‘ ℂfld ) )
37 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → 𝑥 ∈ ( Constr ∖ { 0 } ) )
38 37 eldifad ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → 𝑥 ∈ Constr )
39 38 constrcn ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
40 eldifsni ⊢ ( 𝑥 ∈ ( Constr ∖ { 0 } ) → 𝑥 ≠ 0 )
41 40 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → 𝑥 ≠ 0 )
42 cnfldinv ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
43 39 41 42 syl2anc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
44 38 41 constrinvcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → ( 1 / 𝑥 ) ∈ Constr )
45 43 44 eqeltrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( Constr ∖ { 0 } ) ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr )
46 45 ralrimiva ⊢ ( ⊤ → ∀ 𝑥 ∈ ( Constr ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr )
47 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
48 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
49 47 48 issdrg2 ⊢ ( Constr ∈ ( SubDRing ‘ ℂfld ) ↔ ( ℂfld ∈ DivRing ∧ Constr ∈ ( SubRing ‘ ℂfld ) ∧ ∀ 𝑥 ∈ ( Constr ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ Constr ) )
50 3 36 46 49 syl3anbrc ⊢ ( ⊤ → Constr ∈ ( SubDRing ‘ ℂfld ) )
51 50 mptru ⊢ Constr ∈ ( SubDRing ‘ ℂfld )