constrext2chnlem

	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	⊢ ( 𝜑 → 𝑁 ∈ ω )
	constrext2chnlem.q	⊢ 𝑄 = ( ℂ_fld ↾_s ℚ )
	constrext2chnlem.l	⊢ 𝐿 = ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) )
	constrext2chnlem.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
Assertion	constrext2chnlem	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )

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		constrext2chnlem.q	⊢ 𝑄 = ( ℂ_fld ↾_s ℚ )
7		constrext2chnlem.l	⊢ 𝐿 = ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) )
8		constrext2chnlem.a	⊢ ( 𝜑 → 𝐴 ∈ Constr )
9		2prm	⊢ 2 ∈ ℙ
10	9	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → 2 ∈ ℙ )
11	7 6	oveq12i	⊢ ( 𝐿 [:] 𝑄 ) = ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) )
12		cnfldbas	⊢ ℂ = ( Base ‘ ℂ_fld )
13		eqid	⊢ ( ℂ_fld ↾_s ℚ ) = ( ℂ_fld ↾_s ℚ )
14		eqid	⊢ ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) = ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) )
15		cnfldfld	⊢ ℂ_fld ∈ Field
16	15	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℂ_fld ∈ Field )
17		cndrng	⊢ ℂ_fld ∈ DivRing
18		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂ_fld ) ∧ ( ℂ_fld ↾_s ℚ ) ∈ DivRing )
19	18	simpli	⊢ ℚ ∈ ( SubRing ‘ ℂ_fld )
20	18	simpri	⊢ ( ℂ_fld ↾_s ℚ ) ∈ DivRing
21		issdrg	⊢ ( ℚ ∈ ( SubDRing ‘ ℂ_fld ) ↔ ( ℂ_fld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂ_fld ) ∧ ( ℂ_fld ↾_s ℚ ) ∈ DivRing ) )
22	17 19 20 21	mpbir3an	⊢ ℚ ∈ ( SubDRing ‘ ℂ_fld )
23	22	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℚ ∈ ( SubDRing ‘ ℂ_fld ) )
24		nnon	⊢ ( 𝑚 ∈ ω → 𝑚 ∈ On )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ω ) → 𝑚 ∈ On )
26	1 25	constrsscn	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ω ) → ( 𝐶 ‘ 𝑚 ) ⊆ ℂ )
27	26	sselda	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → 𝐴 ∈ ℂ )
28	27	snssd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → { 𝐴 } ⊆ ℂ )
29	28	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → { 𝐴 } ⊆ ℂ )
30	12 13 14 16 23 29	fldgenfldext	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) )
31	30	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) )
32		extdgcl	⊢ ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℕ₀^* )
33	31 32	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℕ₀^* )
34		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) )
35		2z	⊢ 2 ∈ ℤ
36	35	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → 2 ∈ ℤ )
37		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → 𝑝 ∈ ℕ₀ )
38	36 37	zexpcld	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( 2 ↑ 𝑝 ) ∈ ℤ )
39	34 38	eqeltrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℤ )
40	39	zred	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ )
41		xnn0xr	⊢ ( ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℕ₀^* → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ^* )
42	31 32 41	3syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ^* )
43		eqid	⊢ ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) = ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) )
44		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) )
45		simprl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( 𝑣 ‘ 0 ) = ℚ )
46	45	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( 𝑣 ‘ 0 ) ) = ( ℂ_fld ↾_s ℚ ) )
47		eqidd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) = ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) )
48		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → 𝑣 = ∅ )
49	48	fveq1d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ( 𝑣 ‘ 0 ) = ( ∅ ‘ 0 ) )
50		0fv	⊢ ( ∅ ‘ 0 ) = ∅
51	50	a1i	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ( ∅ ‘ 0 ) = ∅ )
52	49 51	eqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ( 𝑣 ‘ 0 ) = ∅ )
53	45	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ( 𝑣 ‘ 0 ) = ℚ )
54		1nn	⊢ 1 ∈ ℕ
55		nnq	⊢ ( 1 ∈ ℕ → 1 ∈ ℚ )
56	54 55	ax-mp	⊢ 1 ∈ ℚ
57	56	ne0ii	⊢ ℚ ≠ ∅
58	57	a1i	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ℚ ≠ ∅ )
59	53 58	eqnetrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ( 𝑣 ‘ 0 ) ≠ ∅ )
60	59	neneqd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑣 = ∅ ) → ¬ ( 𝑣 ‘ 0 ) = ∅ )
61	52 60	pm2.65da	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ¬ 𝑣 = ∅ )
62	61	neqned	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 𝑣 ≠ ∅ )
63	44 62	hashne0	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 0 < ( ♯ ‘ 𝑣 ) )
64	2 3 4 44 16 46 47 63	fldext2chn	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) ∧ ∃ 𝑝 ∈ ℕ₀ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) )
65	64	simpld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) )
66		fldextfld1	⊢ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ∈ Field )
67	65 66	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ∈ Field )
68	44	chnwrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 𝑣 ∈ Word ( SubDRing ‘ ℂ_fld ) )
69		lswcl	⊢ ( ( 𝑣 ∈ Word ( SubDRing ‘ ℂ_fld ) ∧ 𝑣 ≠ ∅ ) → ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) )
70	68 62 69	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) )
71	17	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℂ_fld ∈ DivRing )
72		qsscn	⊢ ℚ ⊆ ℂ
73	72	a1i	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → ℚ ⊆ ℂ )
74	73 28	unssd	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → ( ℚ ∪ { 𝐴 } ) ⊆ ℂ )
75	74	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℚ ∪ { 𝐴 } ) ⊆ ℂ )
76	12 71 75	fldgensdrg	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ℂ_fld ) )
77	13	qrngbas	⊢ ℚ = ( Base ‘ ( ℂ_fld ↾_s ℚ ) )
78	77 65	fldextsdrg	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℚ ∈ ( SubDRing ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
79	43	sdrgss	⊢ ( ℚ ∈ ( SubDRing ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) → ℚ ⊆ ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
80	78 79	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℚ ⊆ ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
81	12	sdrgss	⊢ ( ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) → ( lastS ‘ 𝑣 ) ⊆ ℂ )
82	70 81	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( lastS ‘ 𝑣 ) ⊆ ℂ )
83		eqid	⊢ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) = ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) )
84	83 12	ressbas2	⊢ ( ( lastS ‘ 𝑣 ) ⊆ ℂ → ( lastS ‘ 𝑣 ) = ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
85	82 84	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( lastS ‘ 𝑣 ) = ( Base ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
86	80 85	sseqtrrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ℚ ⊆ ( lastS ‘ 𝑣 ) )
87		simprr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) )
88		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) )
89	87 88	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → 𝐴 ∈ ( lastS ‘ 𝑣 ) )
90	89	snssd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → { 𝐴 } ⊆ ( lastS ‘ 𝑣 ) )
91	86 90	unssd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℚ ∪ { 𝐴 } ) ⊆ ( lastS ‘ 𝑣 ) )
92	12 71 70 91	fldgenssp	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ⊆ ( lastS ‘ 𝑣 ) )
93		id	⊢ ( ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) → ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) )
94	83 93	subsdrg	⊢ ( ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) → ( ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) ↔ ( ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ℂ_fld ) ∧ ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ⊆ ( lastS ‘ 𝑣 ) ) ) )
95	94	biimpar	⊢ ( ( ( lastS ‘ 𝑣 ) ∈ ( SubDRing ‘ ℂ_fld ) ∧ ( ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ℂ_fld ) ∧ ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
96	70 76 92 95	syl12anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ) )
97	43 67 96	sdrgfldext	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) )
98	70	elexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( lastS ‘ 𝑣 ) ∈ V )
99		ressabs	⊢ ( ( ( lastS ‘ 𝑣 ) ∈ V ∧ ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ⊆ ( lastS ‘ 𝑣 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) = ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) )
100	98 92 99	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) = ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) )
101	97 100	breqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) )
102	101	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) )
103		extdgcl	⊢ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℕ₀^* )
104	102 103	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℕ₀^* )
105		xnn0xr	⊢ ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℕ₀^* → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℝ^* )
106	104 105	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℝ^* )
107		extdggt0	⊢ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) → 0 < ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) )
108	102 107	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → 0 < ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) )
109		extdgmul	⊢ ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) /_FldExt ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ∧ ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
110	101 30 109	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
111	110	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
112		xmulcom	⊢ ( ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℝ^* ∧ ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ^* ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ·_e ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ) )
113	106 42 112	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ·_e ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ) )
114	111 113	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ·_e ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ) )
115	40 42 106 108 114	rexmul2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ )
116		extdggt0	⊢ ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) /_FldExt ( ℂ_fld ↾_s ℚ ) → 0 < ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) )
117	31 116	syl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → 0 < ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) )
118	33 115 117	xnn0nnd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℕ )
119	11 118	eqeltrid	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( 𝐿 [:] 𝑄 ) ∈ ℕ )
120	40 106 42 117 111	rexmul2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℝ )
121	104 120	xnn0nn0d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℕ₀ )
122	121	nn0zd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℤ )
123	118	nnnn0d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℕ₀ )
124	123	nn0zd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℤ )
125		rexmul	⊢ ( ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℝ ∧ ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℝ ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
126	120 115 125	syl2anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ·_e ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
127	111 126	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) )
128	127	eqcomd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) )
129	128 34	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( 2 ↑ 𝑝 ) )
130		dvds0lem	⊢ ( ( ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) ∈ ℤ ∧ ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∈ ℤ ∧ ( 2 ↑ 𝑝 ) ∈ ℤ ) ∧ ( ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) ) · ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∥ ( 2 ↑ 𝑝 ) )
131	122 124 38 129 130	syl31anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( ( ℂ_fld ↾_s ( ℂ_fld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂ_fld ↾_s ℚ ) ) ∥ ( 2 ↑ 𝑝 ) )
132	11 131	eqbrtrid	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ( 𝐿 [:] 𝑄 ) ∥ ( 2 ↑ 𝑝 ) )
133		dvdsprmpweq	⊢ ( ( 2 ∈ ℙ ∧ ( 𝐿 [:] 𝑄 ) ∈ ℕ ∧ 𝑝 ∈ ℕ₀ ) → ( ( 𝐿 [:] 𝑄 ) ∥ ( 2 ↑ 𝑝 ) → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) ) )
134	133	imp	⊢ ( ( ( 2 ∈ ℙ ∧ ( 𝐿 [:] 𝑄 ) ∈ ℕ ∧ 𝑝 ∈ ℕ₀ ) ∧ ( 𝐿 [:] 𝑄 ) ∥ ( 2 ↑ 𝑝 ) ) → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )
135	10 119 37 132 134	syl31anc	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) ∧ 𝑝 ∈ ℕ₀ ) ∧ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) ) → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )
136	64	simprd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ∃ 𝑝 ∈ ℕ₀ ( ( ℂ_fld ↾_s ( lastS ‘ 𝑣 ) ) [:] ( ℂ_fld ↾_s ℚ ) ) = ( 2 ↑ 𝑝 ) )
137	135 136	r19.29a	⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) ∧ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ) ∧ ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) ) → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )
138		simplr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → 𝑚 ∈ ω )
139	1 2 3 4 138	constrextdg2	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → ∃ 𝑣 ∈ ( < Chain ( SubDRing ‘ ℂ_fld ) ) ( ( 𝑣 ‘ 0 ) = ℚ ∧ ( 𝐶 ‘ 𝑚 ) ⊆ ( lastS ‘ 𝑣 ) ) )
140	137 139	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ω ) ∧ 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )
141	1	isconstr	⊢ ( 𝐴 ∈ Constr ↔ ∃ 𝑚 ∈ ω 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) )
142	8 141	sylib	⊢ ( 𝜑 → ∃ 𝑚 ∈ ω 𝐴 ∈ ( 𝐶 ‘ 𝑚 ) )
143	140 142	r19.29a	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ₀ ( 𝐿 [:] 𝑄 ) = ( 2 ↑ 𝑛 ) )

Metamath Proof Explorer

Theorem constrext2chnlem

Proof