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 . See Theorem 7.11 of Stewart p. 97. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses constr0.1 ⊢ C = rec ⁡ s ∈ V ⟼ x ∈ ℂ | ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ t ∈ ℝ ∃ r ∈ ℝ x = a + t ⁢ b − a ∧ x = c + r ⁢ d − c ∧ ℑ ⁡ b − a ‾ ⁢ d − c ≠ 0 ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ e ∈ s ∃ f ∈ s ∃ t ∈ ℝ x = a + t ⁢ b − a ∧ x − c = e − f ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ e ∈ s ∃ f ∈ s a ≠ d ∧ x − a = b − c ∧ x − d = e − f 0 1
constrextdg2.1 ⊢ E = ℂ fld ↾ 𝑠 e
constrextdg2.2 ⊢ F = ℂ fld ↾ 𝑠 f
constrextdg2.l ⊢ < ˙ = f e | E /FldExt F ∧ E .:. F = 2
constrextdg2.n ⊢ φ → N ∈ ω
Assertion constrextdg2 ⊢ φ → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ N ⊆ lastS ⁡ v

Proof

Step Hyp Ref Expression
1 constr0.1 ⊢ C = rec ⁡ s ∈ V ⟼ x ∈ ℂ | ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ t ∈ ℝ ∃ r ∈ ℝ x = a + t ⁢ b − a ∧ x = c + r ⁢ d − c ∧ ℑ ⁡ b − a ‾ ⁢ d − c ≠ 0 ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ e ∈ s ∃ f ∈ s ∃ t ∈ ℝ x = a + t ⁢ b − a ∧ x − c = e − f ∨ ∃ a ∈ s ∃ b ∈ s ∃ c ∈ s ∃ d ∈ s ∃ e ∈ s ∃ f ∈ s a ≠ d ∧ x − a = b − c ∧ x − d = e − f 0 1
2 constrextdg2.1 ⊢ E = ℂ fld ↾ 𝑠 e
3 constrextdg2.2 ⊢ F = ℂ fld ↾ 𝑠 f
4 constrextdg2.l ⊢ < ˙ = f e | E /FldExt F ∧ E .:. F = 2
5 constrextdg2.n ⊢ φ → N ∈ ω
6 fveq2 ⊢ m = ∅ → C ⁡ m = C ⁡ ∅
7 6 sseq1d ⊢ m = ∅ → C ⁡ m ⊆ lastS ⁡ v ↔ C ⁡ ∅ ⊆ lastS ⁡ v
8 7 anbi2d ⊢ m = ∅ → v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ v ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ v
9 8 rexbidv ⊢ m = ∅ → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ v
10 fveq2 ⊢ m = n → C ⁡ m = C ⁡ n
11 10 sseq1d ⊢ m = n → C ⁡ m ⊆ lastS ⁡ v ↔ C ⁡ n ⊆ lastS ⁡ v
12 11 anbi2d ⊢ m = n → v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ v ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ v
13 12 rexbidv ⊢ m = n → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ v
14 fveq1 ⊢ v = u → v ⁡ 0 = u ⁡ 0
15 14 eqeq1d ⊢ v = u → v ⁡ 0 = ℚ ↔ u ⁡ 0 = ℚ
16 fveq2 ⊢ v = u → lastS ⁡ v = lastS ⁡ u
17 16 sseq2d ⊢ v = u → C ⁡ n ⊆ lastS ⁡ v ↔ C ⁡ n ⊆ lastS ⁡ u
18 15 17 anbi12d ⊢ v = u → v ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ v ↔ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u
19 18 cbvrexvw ⊢ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ v ↔ ∃ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u
20 13 19 bitrdi ⊢ m = n → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ ∃ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u
21 fveq2 ⊢ m = suc ⁡ n → C ⁡ m = C ⁡ suc ⁡ n
22 21 sseq1d ⊢ m = suc ⁡ n → C ⁡ m ⊆ lastS ⁡ v ↔ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
23 22 anbi2d ⊢ m = suc ⁡ n → v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ v ⁡ 0 = ℚ ∧ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
24 23 rexbidv ⊢ m = suc ⁡ n → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
25 fveq2 ⊢ m = N → C ⁡ m = C ⁡ N
26 25 sseq1d ⊢ m = N → C ⁡ m ⊆ lastS ⁡ v ↔ C ⁡ N ⊆ lastS ⁡ v
27 26 anbi2d ⊢ m = N → v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ v ⁡ 0 = ℚ ∧ C ⁡ N ⊆ lastS ⁡ v
28 27 rexbidv ⊢ m = N → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ m ⊆ lastS ⁡ v ↔ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ N ⊆ lastS ⁡ v
29 fveq1 ⊢ v = ⟨“ ℚ ”⟩ → v ⁡ 0 = ⟨“ ℚ ”⟩ ⁡ 0
30 29 eqeq1d ⊢ v = ⟨“ ℚ ”⟩ → v ⁡ 0 = ℚ ↔ ⟨“ ℚ ”⟩ ⁡ 0 = ℚ
31 fveq2 ⊢ v = ⟨“ ℚ ”⟩ → lastS ⁡ v = lastS ⁡ ⟨“ ℚ ”⟩
32 31 sseq2d ⊢ v = ⟨“ ℚ ”⟩ → C ⁡ ∅ ⊆ lastS ⁡ v ↔ C ⁡ ∅ ⊆ lastS ⁡ ⟨“ ℚ ”⟩
33 30 32 anbi12d ⊢ v = ⟨“ ℚ ”⟩ → v ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ v ↔ ⟨“ ℚ ”⟩ ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ ⟨“ ℚ ”⟩
34 cndrng ⊢ ℂ fld ∈ DivRing
35 qsubdrg ⊢ ℚ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
36 35 simpli ⊢ ℚ ∈ SubRing ⁡ ℂ fld
37 35 simpri ⊢ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
38 issdrg ⊢ ℚ ∈ SubDRing ⁡ ℂ fld ↔ ℂ fld ∈ DivRing ∧ ℚ ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 ℚ ∈ DivRing
39 34 36 37 38 mpbir3an ⊢ ℚ ∈ SubDRing ⁡ ℂ fld
40 39 a1i ⊢ ⊤ → ℚ ∈ SubDRing ⁡ ℂ fld
41 40 s1chn ⊢ ⊤ → ⟨“ ℚ ”⟩ ∈ Chain SubDRing ⁡ ℂ fld < ˙
42 s1fv ⊢ ℚ ∈ SubDRing ⁡ ℂ fld → ⟨“ ℚ ”⟩ ⁡ 0 = ℚ
43 40 42 syl ⊢ ⊤ → ⟨“ ℚ ”⟩ ⁡ 0 = ℚ
44 0z ⊢ 0 ∈ ℤ
45 1z ⊢ 1 ∈ ℤ
46 prssi ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ → 0 1 ⊆ ℤ
47 44 45 46 mp2an ⊢ 0 1 ⊆ ℤ
48 zssq ⊢ ℤ ⊆ ℚ
49 47 48 sstri ⊢ 0 1 ⊆ ℚ
50 1 constr0 ⊢ C ⁡ ∅ = 0 1
51 lsws1 ⊢ ℚ ∈ SubDRing ⁡ ℂ fld → lastS ⁡ ⟨“ ℚ ”⟩ = ℚ
52 39 51 ax-mp ⊢ lastS ⁡ ⟨“ ℚ ”⟩ = ℚ
53 49 50 52 3sstr4i ⊢ C ⁡ ∅ ⊆ lastS ⁡ ⟨“ ℚ ”⟩
54 43 53 jctir ⊢ ⊤ → ⟨“ ℚ ”⟩ ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ ⟨“ ℚ ”⟩
55 33 41 54 rspcedvdw ⊢ ⊤ → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ v
56 55 mptru ⊢ ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ ∅ ⊆ lastS ⁡ v
57 simplll ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → n ∈ ω
58 simpllr ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → u ∈ Chain SubDRing ⁡ ℂ fld < ˙
59 simplr ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → u ⁡ 0 = ℚ
60 simpr ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → C ⁡ n ⊆ lastS ⁡ u
61 1 2 3 4 57 58 59 60 constrextdg2lem ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
62 61 anasss ⊢ n ∈ ω ∧ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ ∧ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
63 62 rexlimdva2 ⊢ n ∈ ω → ∃ u ∈ Chain SubDRing ⁡ ℂ fld < ˙ u ⁡ 0 = ℚ ∧ C ⁡ n ⊆ lastS ⁡ u → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ suc ⁡ n ⊆ lastS ⁡ v
64 9 20 24 28 56 63 finds ⊢ N ∈ ω → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ N ⊆ lastS ⁡ v
65 5 64 syl ⊢ φ → ∃ v ∈ Chain SubDRing ⁡ ℂ fld < ˙ v ⁡ 0 = ℚ ∧ C ⁡ N ⊆ lastS ⁡ v