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	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	constrext2chn.l	⊢ 𝐿 = ( ℂfld ↾s 𝑆 )
	constrext2chn.s	⊢ 𝑆 = ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) )
	constrext2chn.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
Assertion	constrext2chn	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		constrext2chn.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		constrext2chn.l	⊢ 𝐿 = ( ℂfld ↾s 𝑆 )
3		constrext2chn.s	⊢ 𝑆 = ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) )
4		constrext2chn.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
5		constrcbvlem	⊢ rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
6		eqid	⊢ ( ℂfld ↾s 𝑒 ) = ( ℂfld ↾s 𝑒 )
7		eqid	⊢ ( ℂfld ↾s 𝑓 ) = ( ℂfld ↾s 𝑓 )
8		oveq2	⊢ ( ℎ = 𝑒 → ( ℂfld ↾s ℎ ) = ( ℂfld ↾s 𝑒 ) )
9	8	adantl	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ℂfld ↾s ℎ ) = ( ℂfld ↾s 𝑒 ) )
10		oveq2	⊢ ( 𝑔 = 𝑓 → ( ℂfld ↾s 𝑔 ) = ( ℂfld ↾s 𝑓 ) )
11	10	adantr	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ℂfld ↾s 𝑔 ) = ( ℂfld ↾s 𝑓 ) )
12	9 11	breq12d	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ( ℂfld ↾s ℎ ) /FldExt ( ℂfld ↾s 𝑔 ) ↔ ( ℂfld ↾s 𝑒 ) /FldExt ( ℂfld ↾s 𝑓 ) ) )
13	9 11	oveq12d	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ( ℂfld ↾s ℎ ) [:] ( ℂfld ↾s 𝑔 ) ) = ( ( ℂfld ↾s 𝑒 ) [:] ( ℂfld ↾s 𝑓 ) ) )
14	13	eqeq1d	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ( ( ℂfld ↾s ℎ ) [:] ( ℂfld ↾s 𝑔 ) ) = 2 ↔ ( ( ℂfld ↾s 𝑒 ) [:] ( ℂfld ↾s 𝑓 ) ) = 2 ) )
15	12 14	anbi12d	⊢ ( ( 𝑔 = 𝑓 ∧ ℎ = 𝑒 ) → ( ( ( ℂfld ↾s ℎ ) /FldExt ( ℂfld ↾s 𝑔 ) ∧ ( ( ℂfld ↾s ℎ ) [:] ( ℂfld ↾s 𝑔 ) ) = 2 ) ↔ ( ( ℂfld ↾s 𝑒 ) /FldExt ( ℂfld ↾s 𝑓 ) ∧ ( ( ℂfld ↾s 𝑒 ) [:] ( ℂfld ↾s 𝑓 ) ) = 2 ) ) )
16	15	cbvopabv	⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( ℂfld ↾s ℎ ) /FldExt ( ℂfld ↾s 𝑔 ) ∧ ( ( ℂfld ↾s ℎ ) [:] ( ℂfld ↾s 𝑔 ) ) = 2 ) } = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( ( ℂfld ↾s 𝑒 ) /FldExt ( ℂfld ↾s 𝑓 ) ∧ ( ( ℂfld ↾s 𝑒 ) [:] ( ℂfld ↾s 𝑓 ) ) = 2 ) }
17		peano1	⊢ ∅ ∈ ω
18	17	a1i	⊢ ( 𝜑 → ∅ ∈ ω )
19	3	oveq2i	⊢ ( ℂfld ↾s 𝑆 ) = ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) )
20	2 19	eqtri	⊢ 𝐿 = ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) )
21	5 6 7 16 18 1 20 4	constrext2chnlem	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )