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 . (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypotheses	constr0.1	⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
	constrextdg2.1	⊢ 𝐸 = ( ℂ_fld ↾_s 𝑒 )
	constrextdg2.2	⊢ 𝐹 = ( ℂ_fld ↾_s 𝑓 )
	constrextdg2.l	⊢ < = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) }
	constrextdg2.n	⊢ ( 𝜑 → 𝑁 ∈ ω )
Assertion	constrextdg2	⊢ ( 𝜑 → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) )

Proof

Step	Hyp	Ref	Expression
1		constr0.1	⊢ 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
2		constrextdg2.1	⊢ 𝐸 = ( ℂ_fld ↾_s 𝑒 )
3		constrextdg2.2	⊢ 𝐹 = ( ℂ_fld ↾_s 𝑓 )
4		constrextdg2.l	⊢ < = { ⟨ 𝑓 , 𝑒 ⟩ ∣ ( 𝐸 /_FldExt 𝐹 ∧ ( 𝐸 [:] 𝐹 ) = 2 ) }
5		constrextdg2.n	⊢ ( 𝜑 → 𝑁 ∈ ω )
6		fveq2	⊢ ( 𝑚 = ∅ → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ ∅ ) )
7	6	sseq1d	⊢ ( 𝑚 = ∅ → ( ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ) )
8	7	anbi2d	⊢ ( 𝑚 = ∅ → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
9	8	rexbidv	⊢ ( 𝑚 = ∅ → ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
10		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑛 ) )
11	10	sseq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) )
12	11	anbi2d	⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
13	12	rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
14		fveq1	⊢ ( 𝑣 = 𝑢 → ( 𝑣 ‘ 0 ) = ( 𝑢 ‘ 0 ) )
15	14	eqeq1d	⊢ ( 𝑣 = 𝑢 → ( ( 𝑣 ‘ 0 ) = ℚ ↔ ( 𝑢 ‘ 0 ) = ℚ ) )
16		fveq2	⊢ ( 𝑣 = 𝑢 → ( lastS ‘ 𝑣 ) = ( lastS ‘ 𝑢 ) )
17	16	sseq2d	⊢ ( 𝑣 = 𝑢 → ( ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) )
18	15 17	anbi12d	⊢ ( 𝑣 = 𝑢 → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( 𝑢 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑢 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) )
20	13 19	bitrdi	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑢 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) ) )
21		fveq2	⊢ ( 𝑚 = suc 𝑛 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ suc 𝑛 ) )
22	21	sseq1d	⊢ ( 𝑚 = suc 𝑛 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) )
23	22	anbi2d	⊢ ( 𝑚 = suc 𝑛 → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
24	23	rexbidv	⊢ ( 𝑚 = suc 𝑛 → ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
25		fveq2	⊢ ( 𝑚 = 𝑁 → ( 𝐶 ‘ 𝑚 ) = ( 𝐶 ‘ 𝑁 ) )
26	25	sseq1d	⊢ ( 𝑚 = 𝑁 → ( ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) )
27	26	anbi2d	⊢ ( 𝑚 = 𝑁 → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
28	27	rexbidv	⊢ ( 𝑚 = 𝑁 → ( ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
29		fveq1	⊢ ( 𝑣 = ⟨“ ℚ ”⟩ → ( 𝑣 ‘ 0 ) = ( ⟨“ ℚ ”⟩ ‘ 0 ) )
30	29	eqeq1d	⊢ ( 𝑣 = ⟨“ ℚ ”⟩ → ( ( 𝑣 ‘ 0 ) = ℚ ↔ ( ⟨“ ℚ ”⟩ ‘ 0 ) = ℚ ) )
31		fveq2	⊢ ( 𝑣 = ⟨“ ℚ ”⟩ → ( lastS ‘ 𝑣 ) = ( lastS ‘ ⟨“ ℚ ”⟩ ) )
32	31	sseq2d	⊢ ( 𝑣 = ⟨“ ℚ ”⟩ → ( ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ↔ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ ⟨“ ℚ ”⟩ ) ) )
33	30 32	anbi12d	⊢ ( 𝑣 = ⟨“ ℚ ”⟩ → ( ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ) ↔ ( ( ⟨“ ℚ ”⟩ ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ ⟨“ ℚ ”⟩ ) ) ) )
34		cndrng	⊢ ℂ_fld ∈ DivRing
35		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂ_fld ) ∧ ( ℂ_fld ↾_s ℚ ) ∈ DivRing )
36	35	simpli	⊢ ℚ ∈ ( SubRing ‘ ℂ_fld )
37	35	simpri	⊢ ( ℂ_fld ↾_s ℚ ) ∈ DivRing
38		issdrg	⊢ ( ℚ ∈ ( SubDRing ‘ ℂ_fld ) ↔ ( ℂ_fld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂ_fld ) ∧ ( ℂ_fld ↾_s ℚ ) ∈ 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	⊢ ( 𝐶 ‘ ∅ ) = { 0 , 1 }
51		lsws1	⊢ ( ℚ ∈ ( SubDRing ‘ ℂ_fld ) → ( lastS ‘ ⟨“ ℚ ”⟩ ) = ℚ )
52	39 51	ax-mp	⊢ ( lastS ‘ ⟨“ ℚ ”⟩ ) = ℚ
53	49 50 52	3sstr4i	⊢ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ ⟨“ ℚ ”⟩ )
54	43 53	jctir	⊢ ( ⊤ → ( ( ⟨“ ℚ ”⟩ ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ ⟨“ ℚ ”⟩ ) ) )
55	33 41 54	rspcedvdw	⊢ ( ⊤ → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) ) )
56	55	mptru	⊢ ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ ∅ ) ⊆ ( lastS ‘ 𝑣 ) )
57		simplll	⊢ ( ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( 𝑢 ‘ 0 ) = ℚ ) ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → 𝑛 ∈ ω )
58		simpllr	⊢ ( ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( 𝑢 ‘ 0 ) = ℚ ) ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) )
59		simplr	⊢ ( ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( 𝑢 ‘ 0 ) = ℚ ) ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → ( 𝑢 ‘ 0 ) = ℚ )
60		simpr	⊢ ( ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( 𝑢 ‘ 0 ) = ℚ ) ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) )
61	1 2 3 4 57 58 59 60	constrextdg2lem	⊢ ( ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( 𝑢 ‘ 0 ) = ℚ ) ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) )
62	61	anasss	⊢ ( ( ( 𝑛 ∈ ω ∧ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑢 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) ) → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) )
63	62	rexlimdva2	⊢ ( 𝑛 ∈ ω → ( ∃ 𝑢 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑢 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑛 ) ⊆ ( lastS ‘ 𝑢 ) ) → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ suc 𝑛 ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
64	9 20 24 28 56 63	finds	⊢ ( 𝑁 ∈ ω → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) )
65	5 64	syl	⊢ ( 𝜑 → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑁 ) ⊆ ( lastS ‘ 𝑣 ) ) )

Metamath Proof Explorer

Theorem constrextdg2

Proof