Metamath Proof Explorer

Theorem constrext2chn

Description: If a constructible number generates some subfield L of CC , then the degree of the extension of L over QQ is a power of two. Theorem 7.12 of Stewart p. 98. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses constrext2chn.q ⊢ Q = ℂ fld ↾ 𝑠 ℚ
constrext2chn.l ⊢ L = ℂ fld ↾ 𝑠 S
constrext2chn.s ⊢ S = ℂ fld fldGen ℚ ∪ A
constrext2chn.a ⊢ φ → A ∈ Constr
Assertion constrext2chn ⊢ φ → ∃ n ∈ ℕ 0 L .:. Q = 2 n

Proof

Step Hyp Ref Expression
1 constrext2chn.q ⊢ Q = ℂ fld ↾ 𝑠 ℚ
2 constrext2chn.l ⊢ L = ℂ fld ↾ 𝑠 S
3 constrext2chn.s ⊢ S = ℂ fld fldGen ℚ ∪ A
4 constrext2chn.a ⊢ φ → A ∈ Constr
5 constrcbvlem ⊢ rec ⁡ z ∈ V ⟼ y ∈ ℂ | ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ l ∈ z ∃ o ∈ ℝ ∃ p ∈ ℝ y = i + o ⁢ j − i ∧ y = k + p ⁢ l − k ∧ ℑ ⁡ j − i ‾ ⁢ l − k ≠ 0 ∨ ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ m ∈ z ∃ q ∈ z ∃ o ∈ ℝ y = i + o ⁢ j − i ∧ y − k = m − q ∨ ∃ i ∈ z ∃ j ∈ z ∃ k ∈ z ∃ l ∈ z ∃ m ∈ z ∃ q ∈ z i ≠ l ∧ y − i = j − k ∧ y − l = m − q 0 1 = 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
6 eqid ⊢ ℂ fld ↾ 𝑠 e = ℂ fld ↾ 𝑠 e
7 eqid ⊢ ℂ fld ↾ 𝑠 f = ℂ fld ↾ 𝑠 f
8 oveq2 ⊢ h = e → ℂ fld ↾ 𝑠 h = ℂ fld ↾ 𝑠 e
9 8 adantl ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 h = ℂ fld ↾ 𝑠 e
10 oveq2 ⊢ g = f → ℂ fld ↾ 𝑠 g = ℂ fld ↾ 𝑠 f
11 10 adantr ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 g = ℂ fld ↾ 𝑠 f
12 9 11 breq12d ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 h /FldExt ℂ fld ↾ 𝑠 g ↔ ℂ fld ↾ 𝑠 e /FldExt ℂ fld ↾ 𝑠 f
13 9 11 oveq12d ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 h .:. ℂ fld ↾ 𝑠 g = ℂ fld ↾ 𝑠 e .:. ℂ fld ↾ 𝑠 f
14 13 eqeq1d ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 h .:. ℂ fld ↾ 𝑠 g = 2 ↔ ℂ fld ↾ 𝑠 e .:. ℂ fld ↾ 𝑠 f = 2
15 12 14 anbi12d ⊢ g = f ∧ h = e → ℂ fld ↾ 𝑠 h /FldExt ℂ fld ↾ 𝑠 g ∧ ℂ fld ↾ 𝑠 h .:. ℂ fld ↾ 𝑠 g = 2 ↔ ℂ fld ↾ 𝑠 e /FldExt ℂ fld ↾ 𝑠 f ∧ ℂ fld ↾ 𝑠 e .:. ℂ fld ↾ 𝑠 f = 2
16 15 cbvopabv ⊢ g h | ℂ fld ↾ 𝑠 h /FldExt ℂ fld ↾ 𝑠 g ∧ ℂ fld ↾ 𝑠 h .:. ℂ fld ↾ 𝑠 g = 2 = f e | ℂ fld ↾ 𝑠 e /FldExt ℂ fld ↾ 𝑠 f ∧ ℂ fld ↾ 𝑠 e .:. ℂ fld ↾ 𝑠 f = 2
17 peano1 ⊢ ∅ ∈ ω
18 17 a1i ⊢ φ → ∅ ∈ ω
19 3 oveq2i ⊢ ℂ fld ↾ 𝑠 S = ℂ fld ↾ 𝑠 ℂ fld fldGen ℚ ∪ A
20 2 19 eqtri ⊢ L = ℂ fld ↾ 𝑠 ℂ fld fldGen ℚ ∪ A
21 5 6 7 16 18 1 20 4 constrext2chnlem ⊢ φ → ∃ n ∈ ℕ 0 L .:. Q = 2 n