constrext2chnlem

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrextdg2.1	$⊢ E = ℂ_{fld} ↾_{𝑠} e$
	constrextdg2.2	$⊢ F = ℂ_{fld} ↾_{𝑠} f$
	constrextdg2.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (E /_{FldExt} F \land E [. : .] F = 2)\}$
	constrextdg2.n	$⊢ φ \to N \in ω$
	constrext2chnlem.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	constrext2chnlem.l	$⊢ L = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
	constrext2chnlem.a	$⊢ φ \to A \in Constr$
Assertion	constrext2chnlem	$⊢ φ \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrextdg2.1	$⊢ E = ℂ_{fld} ↾_{𝑠} e$
3		constrextdg2.2	$⊢ F = ℂ_{fld} ↾_{𝑠} f$
4		constrextdg2.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (E /_{FldExt} F \land E [. : .] F = 2)\}$
5		constrextdg2.n	$⊢ φ \to N \in ω$
6		constrext2chnlem.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
7		constrext2chnlem.l	$⊢ L = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
8		constrext2chnlem.a	$⊢ φ \to A \in Constr$
9		2prm	$⊢ 2 \in ℙ$
10	9	a1i	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to 2 \in ℙ$
11	7 6	oveq12i	$⊢ L [. : .] Q = (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ)$
12		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
13		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℚ = ℂ_{fld} ↾_{𝑠} ℚ$
14		eqid	$⊢ ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
15		cnfldfld	$⊢ ℂ_{fld} \in Field$
16	15	a1i	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} \in Field$
17		cndrng	$⊢ ℂ_{fld} \in DivRing$
18		qsubdrg	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
19	18	simpli	$⊢ ℚ \in SubRing (ℂ_{fld})$
20	18	simpri	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in DivRing$
21		issdrg	$⊢ ℚ \in SubDRing (ℂ_{fld}) \leftrightarrow (ℂ_{fld} \in DivRing \land ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
22	17 19 20 21	mpbir3an	$⊢ ℚ \in SubDRing (ℂ_{fld})$
23	22	a1i	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \in SubDRing (ℂ_{fld})$
24		nnon	$⊢ m \in ω \to m \in On$
25	24	adantl	$⊢ (φ \land m \in ω) \to m \in On$
26	1 25	constrsscn	$⊢ (φ \land m \in ω) \to C (m) \subseteq ℂ$
27	26	sselda	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to A \in ℂ$
28	27	snssd	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to \{A\} \subseteq ℂ$
29	28	ad2antrr	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to \{A\} \subseteq ℂ$
30	12 13 14 16 23 29	fldgenfldext	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ)$
31	30	ad2antrr	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ)$
32		extdgcl	$⊢ (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℕ_{0}^{*}$
33	31 32	syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℕ_{0}^{*}$
34		simpr	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}$
35		2z	$⊢ 2 \in ℤ$
36	35	a1i	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to 2 \in ℤ$
37		simplr	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to p \in ℕ_{0}$
38	36 37	zexpcld	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to 2^{p} \in ℤ$
39	34 38	eqeltrd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℤ$
40	39	zred	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ$
41		xnn0xr	$⊢ (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℕ_{0}^{} \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ^{}$
42	31 32 41	3syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ^{*}$
43		eqid	$⊢ {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))} = {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))}$
44		simplr	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}$
45		simprl	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to v (0) = ℚ$
46	45	oveq2d	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} ↾_{𝑠} v (0) = ℂ_{fld} ↾_{𝑠} ℚ$
47		eqidd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} ↾_{𝑠} lastS (v) = ℂ_{fld} ↾_{𝑠} lastS (v)$
48		simpr	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to v = \emptyset$
49	48	fveq1d	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to v (0) = \emptyset (0)$
50		0fv	$⊢ \emptyset (0) = \emptyset$
51	50	a1i	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to \emptyset (0) = \emptyset$
52	49 51	eqtrd	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to v (0) = \emptyset$
53	45	adantr	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to v (0) = ℚ$
54		1nn	$⊢ 1 \in ℕ$
55		nnq	$⊢ 1 \in ℕ \to 1 \in ℚ$
56	54 55	ax-mp	$⊢ 1 \in ℚ$
57	56	ne0ii	$⊢ ℚ \neq \emptyset$
58	57	a1i	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to ℚ \neq \emptyset$
59	53 58	eqnetrd	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to v (0) \neq \emptyset$
60	59	neneqd	$⊢ (((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land v = \emptyset) \to \neg v (0) = \emptyset$
61	52 60	pm2.65da	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to \neg v = \emptyset$
62	61	neqned	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to v \neq \emptyset$
63	44 62	hashne0	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to 0 < \|v\|$
64	2 3 4 44 16 46 47 63	fldext2chn	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ((ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ) \land \exists p \in ℕ_{0} (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p})$
65	64	simpld	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ)$
66		fldextfld1	$⊢ (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ) \to ℂ_{fld} ↾_{𝑠} lastS (v) \in Field$
67	65 66	syl	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} ↾_{𝑠} lastS (v) \in Field$
68	44	chnwrd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to v \in Word SubDRing (ℂ_{fld})$
69		lswcl	$⊢ (v \in Word SubDRing (ℂ_{fld}) \land v \neq \emptyset) \to lastS (v) \in SubDRing (ℂ_{fld})$
70	68 62 69	syl2anc	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to lastS (v) \in SubDRing (ℂ_{fld})$
71	17	a1i	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} \in DivRing$
72		qsscn	$⊢ ℚ \subseteq ℂ$
73	72	a1i	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to ℚ \subseteq ℂ$
74	73 28	unssd	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to ℚ \cup \{A\} \subseteq ℂ$
75	74	ad2antrr	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \cup \{A\} \subseteq ℂ$
76	12 71 75	fldgensdrg	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld})$
77	13	qrngbas	$⊢ ℚ = {Base}_{(ℂ_{fld} ↾_{𝑠} ℚ)}$
78	77 65	fldextsdrg	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \in SubDRing (ℂ_{fld} ↾_{𝑠} lastS (v))$
79	43	sdrgss	$⊢ ℚ \in SubDRing (ℂ_{fld} ↾_{𝑠} lastS (v)) \to ℚ \subseteq {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))}$
80	78 79	syl	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \subseteq {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))}$
81	12	sdrgss	$⊢ lastS (v) \in SubDRing (ℂ_{fld}) \to lastS (v) \subseteq ℂ$
82	70 81	syl	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to lastS (v) \subseteq ℂ$
83		eqid	$⊢ ℂ_{fld} ↾_{𝑠} lastS (v) = ℂ_{fld} ↾_{𝑠} lastS (v)$
84	83 12	ressbas2	$⊢ lastS (v) \subseteq ℂ \to lastS (v) = {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))}$
85	82 84	syl	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to lastS (v) = {Base}_{(ℂ_{fld} ↾_{𝑠} lastS (v))}$
86	80 85	sseqtrrd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \subseteq lastS (v)$
87		simprr	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to C (m) \subseteq lastS (v)$
88		simpllr	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to A \in C (m)$
89	87 88	sseldd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to A \in lastS (v)$
90	89	snssd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to \{A\} \subseteq lastS (v)$
91	86 90	unssd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℚ \cup \{A\} \subseteq lastS (v)$
92	12 71 70 91	fldgenssp	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} fldGen (ℚ \cup \{A\}) \subseteq lastS (v)$
93		id	$⊢ lastS (v) \in SubDRing (ℂ_{fld}) \to lastS (v) \in SubDRing (ℂ_{fld})$
94	83 93	subsdrg	$⊢ lastS (v) \in SubDRing (ℂ_{fld}) \to (ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld} ↾_{𝑠} lastS (v)) \leftrightarrow (ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld}) \land ℂ_{fld} fldGen (ℚ \cup \{A\}) \subseteq lastS (v)))$
95	94	biimpar	$⊢ (lastS (v) \in SubDRing (ℂ_{fld}) \land (ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld}) \land ℂ_{fld} fldGen (ℚ \cup \{A\}) \subseteq lastS (v))) \to ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld} ↾_{𝑠} lastS (v))$
96	70 76 92 95	syl12anc	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to ℂ_{fld} fldGen (ℚ \cup \{A\}) \in SubDRing (ℂ_{fld} ↾_{𝑠} lastS (v))$
97	43 67 96	sdrgfldext	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} ((ℂ_{fld} ↾_{𝑠} lastS (v)) ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})))$
98	70	elexd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to lastS (v) \in V$
99		ressabs	$⊢ (lastS (v) \in V \land ℂ_{fld} fldGen (ℚ \cup \{A\}) \subseteq lastS (v)) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
100	98 92 99	syl2anc	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) = ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))$
101	97 100	breqtrd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})))$
102	101	ad2antrr	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})))$
103		extdgcl	$⊢ (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℕ_{0}^{*}$
104	102 103	syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℕ_{0}^{*}$
105		xnn0xr	$⊢ (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℕ_{0}^{} \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℝ^{}$
106	104 105	syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℝ^{*}$
107		extdggt0	$⊢ (ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \to 0 < (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})))$
108	102 107	syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to 0 < (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})))$
109		extdgmul	$⊢ ((ℂ_{fld} ↾_{𝑠} lastS (v)) /_{FldExt} (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ)) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
110	101 30 109	syl2anc	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
111	110	ad2antrr	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
112		xmulcom	$⊢ ((ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℝ^{} \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ^{}) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))]$
113	106 42 112	syl2anc	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))]$
114	111 113	eqtrd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))]$
115	40 42 106 108 114	rexmul2	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ$
116		extdggt0	$⊢ (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) /_{FldExt} (ℂ_{fld} ↾_{𝑠} ℚ) \to 0 < (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ)$
117	31 116	syl	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to 0 < (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ)$
118	33 115 117	xnn0nnd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℕ$
119	11 118	eqeltrid	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to L [. : .] Q \in ℕ$
120	40 106 42 117 111	rexmul2	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℝ$
121	104 120	xnn0nn0d	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℕ_{0}$
122	121	nn0zd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℤ$
123	118	nnnn0d	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℕ_{0}$
124	123	nn0zd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℤ$
125		rexmul	$⊢ ((ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℝ \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℝ) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
126	120 115 125	syl2anc	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] \cdot_{𝑒} [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
127	111 126	eqtrd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ]$
128	127	eqcomd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ)$
129	128 34	eqtrd	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = 2^{p}$
130		dvds0lem	$⊢ (((ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) \in ℤ \land (ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) \in ℤ \land 2^{p} \in ℤ) \land [ℂ_{fld} ↾_{𝑠} lastS (v) : ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\}))] [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] ∥ 2^{p}$
131	122 124 38 129 130	syl31anc	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [ℂ_{fld} ↾_{𝑠} (ℂ_{fld} fldGen (ℚ \cup \{A\})) : ℂ_{fld} ↾_{𝑠} ℚ] ∥ 2^{p}$
132	11 131	eqbrtrid	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to [L : Q] ∥ 2^{p}$
133		dvdsprmpweq	$⊢ (2 \in ℙ \land L [. : .] Q \in ℕ \land p \in ℕ_{0}) \to ([L : Q] ∥ 2^{p} \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n})$
134	133	imp	$⊢ ((2 \in ℙ \land L [. : .] Q \in ℕ \land p \in ℕ_{0}) \land [L : Q] ∥ 2^{p}) \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$
135	10 119 37 132 134	syl31anc	$⊢ ((((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \land p \in ℕ_{0}) \land (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}) \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$
136	64	simprd	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to \exists p \in ℕ_{0} (ℂ_{fld} ↾_{𝑠} lastS (v)) [. : .] (ℂ_{fld} ↾_{𝑠} ℚ) = 2^{p}$
137	135 136	r19.29a	$⊢ ((((φ \land m \in ω) \land A \in C (m)) \land v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<}) \land (v (0) = ℚ \land C (m) \subseteq lastS (v))) \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$
138		simplr	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to m \in ω$
139	1 2 3 4 138	constrextdg2	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to \exists v \in {Chain}_{SubDRing (ℂ_{fld})} \underset{˙}{<} (v (0) = ℚ \land C (m) \subseteq lastS (v))$
140	137 139	r19.29a	$⊢ ((φ \land m \in ω) \land A \in C (m)) \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$
141	1	isconstr	$⊢ A \in Constr \leftrightarrow \exists m \in ω A \in C (m)$
142	8 141	sylib	$⊢ φ \to \exists m \in ω A \in C (m)$
143	140 142	r19.29a	$⊢ φ \to \exists n \in ℕ_{0} L [. : .] Q = 2^{n}$

Metamath Proof Explorer

Theorem constrext2chnlem

Proof