fldext2chn

Description: In a non-empty tower T of quadratic field extensions, the degree of the extension of the first member by the last is a power of two. (Contributed by Thierry Arnoux, 19-Jun-2025)

	Ref	Expression
Hypotheses	fldext2chn.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (e /_{FldExt} f \land e [. : .] f = 2)\}$
	fldext2chn.t	$⊢ φ \to T \in {Chain}_{Field} \underset{˙}{<}$
	fldext2chn.1	$⊢ φ \to T (0) = Q$
	fldext2chn.2	$⊢ φ \to lastS (T) = F$
	fldext2chn.3	$⊢ φ \to 0 < \|T\|$
Assertion	fldext2chn	$⊢ φ \to \exists n \in ℕ_{0} F [. : .] Q = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		fldext2chn.l	$⊢ \underset{˙}{<} = \{⟨f, e⟩ \| (e /_{FldExt} f \land e [. : .] f = 2)\}$
2		fldext2chn.t	$⊢ φ \to T \in {Chain}_{Field} \underset{˙}{<}$
3		fldext2chn.1	$⊢ φ \to T (0) = Q$
4		fldext2chn.2	$⊢ φ \to lastS (T) = F$
5		fldext2chn.3	$⊢ φ \to 0 < \|T\|$
6		fveq2	$⊢ d = \emptyset \to \|d\| = \|\emptyset\|$
7	6	breq2d	$⊢ d = \emptyset \to (0 < \|d\| \leftrightarrow 0 < \|\emptyset\|)$
8		fveq2	$⊢ d = \emptyset \to lastS (d) = lastS (\emptyset)$
9		fveq1	$⊢ d = \emptyset \to d (0) = \emptyset (0)$
10	8 9	breq12d	$⊢ d = \emptyset \to (lastS (d) /_{FldExt} d (0) \leftrightarrow lastS (\emptyset) /_{FldExt} \emptyset (0))$
11	8 9	oveq12d	$⊢ d = \emptyset \to lastS (d) [. : .] d (0) = lastS (\emptyset) [. : .] \emptyset (0)$
12	11	eqeq1d	$⊢ d = \emptyset \to (lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow lastS (\emptyset) [. : .] \emptyset (0) = 2^{n})$
13	12	rexbidv	$⊢ d = \emptyset \to (\exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow \exists n \in ℕ_{0} lastS (\emptyset) [. : .] \emptyset (0) = 2^{n})$
14	10 13	anbi12d	$⊢ d = \emptyset \to ((lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n}) \leftrightarrow (lastS (\emptyset) /_{FldExt} \emptyset (0) \land \exists n \in ℕ_{0} lastS (\emptyset) [. : .] \emptyset (0) = 2^{n}))$
15	7 14	imbi12d	$⊢ d = \emptyset \to ((0 < \|d\| \to (lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n})) \leftrightarrow (0 < \|\emptyset\| \to (lastS (\emptyset) /_{FldExt} \emptyset (0) \land \exists n \in ℕ_{0} lastS (\emptyset) [. : .] \emptyset (0) = 2^{n})))$
16		fveq2	$⊢ d = c \to \|d\| = \|c\|$
17	16	breq2d	$⊢ d = c \to (0 < \|d\| \leftrightarrow 0 < \|c\|)$
18		fveq2	$⊢ d = c \to lastS (d) = lastS (c)$
19		fveq1	$⊢ d = c \to d (0) = c (0)$
20	18 19	breq12d	$⊢ d = c \to (lastS (d) /_{FldExt} d (0) \leftrightarrow lastS (c) /_{FldExt} c (0))$
21	18 19	oveq12d	$⊢ d = c \to lastS (d) [. : .] d (0) = lastS (c) [. : .] c (0)$
22	21	eqeq1d	$⊢ d = c \to (lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow lastS (c) [. : .] c (0) = 2^{n})$
23	22	rexbidv	$⊢ d = c \to (\exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n})$
24	20 23	anbi12d	$⊢ d = c \to ((lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n}) \leftrightarrow (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))$
25	17 24	imbi12d	$⊢ d = c \to ((0 < \|d\| \to (lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n})) \leftrightarrow (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n})))$
26		fveq2	$⊢ d = c ++ ⟨“ g ”⟩ \to \|d\| = \|c ++ ⟨“ g ”⟩\|$
27	26	breq2d	$⊢ d = c ++ ⟨“ g ”⟩ \to (0 < \|d\| \leftrightarrow 0 < \|c ++ ⟨“ g ”⟩\|)$
28		fveq2	$⊢ d = c ++ ⟨“ g ”⟩ \to lastS (d) = lastS (c ++ ⟨“ g ”⟩)$
29		fveq1	$⊢ d = c ++ ⟨“ g ”⟩ \to d (0) = (c ++ ⟨“ g ”⟩) (0)$
30	28 29	breq12d	$⊢ d = c ++ ⟨“ g ”⟩ \to (lastS (d) /_{FldExt} d (0) \leftrightarrow lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0))$
31	28 29	oveq12d	$⊢ d = c ++ ⟨“ g ”⟩ \to lastS (d) [. : .] d (0) = lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0)$
32	31	eqeq1d	$⊢ d = c ++ ⟨“ g ”⟩ \to (lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{n})$
33	32	rexbidv	$⊢ d = c ++ ⟨“ g ”⟩ \to (\exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow \exists n \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{n})$
34		oveq2	$⊢ n = m \to 2^{n} = 2^{m}$
35	34	eqeq2d	$⊢ n = m \to (lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{n} \leftrightarrow lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})$
36	35	cbvrexvw	$⊢ \exists n \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{n} \leftrightarrow \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}$
37	33 36	bitrdi	$⊢ d = c ++ ⟨“ g ”⟩ \to (\exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})$
38	30 37	anbi12d	$⊢ d = c ++ ⟨“ g ”⟩ \to ((lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n}) \leftrightarrow (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}))$
39	27 38	imbi12d	$⊢ d = c ++ ⟨“ g ”⟩ \to ((0 < \|d\| \to (lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n})) \leftrightarrow (0 < \|c ++ ⟨“ g ”⟩\| \to (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})))$
40		fveq2	$⊢ d = T \to \|d\| = \|T\|$
41	40	breq2d	$⊢ d = T \to (0 < \|d\| \leftrightarrow 0 < \|T\|)$
42		fveq2	$⊢ d = T \to lastS (d) = lastS (T)$
43		fveq1	$⊢ d = T \to d (0) = T (0)$
44	42 43	breq12d	$⊢ d = T \to (lastS (d) /_{FldExt} d (0) \leftrightarrow lastS (T) /_{FldExt} T (0))$
45	42 43	oveq12d	$⊢ d = T \to lastS (d) [. : .] d (0) = lastS (T) [. : .] T (0)$
46	45	eqeq1d	$⊢ d = T \to (lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow lastS (T) [. : .] T (0) = 2^{n})$
47	46	rexbidv	$⊢ d = T \to (\exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n} \leftrightarrow \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n})$
48	44 47	anbi12d	$⊢ d = T \to ((lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n}) \leftrightarrow (lastS (T) /_{FldExt} T (0) \land \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n}))$
49	41 48	imbi12d	$⊢ d = T \to ((0 < \|d\| \to (lastS (d) /_{FldExt} d (0) \land \exists n \in ℕ_{0} lastS (d) [. : .] d (0) = 2^{n})) \leftrightarrow (0 < \|T\| \to (lastS (T) /_{FldExt} T (0) \land \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n})))$
50		0re	$⊢ 0 \in ℝ$
51	50	ltnri	$⊢ \neg 0 < 0$
52	51	a1i	$⊢ φ \to \neg 0 < 0$
53		hash0	$⊢ \|\emptyset\| = 0$
54	53	breq2i	$⊢ 0 < \|\emptyset\| \leftrightarrow 0 < 0$
55	52 54	sylnibr	$⊢ φ \to \neg 0 < \|\emptyset\|$
56	55	pm2.21d	$⊢ φ \to (0 < \|\emptyset\| \to (lastS (\emptyset) /_{FldExt} \emptyset (0) \land \exists n \in ℕ_{0} lastS (\emptyset) [. : .] \emptyset (0) = 2^{n}))$
57		simp-5r	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to g \in Field$
58		fldextid	$⊢ g \in Field \to g /_{FldExt} g$
59	57 58	syl	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to g /_{FldExt} g$
60		simp-5r	$⊢ (((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \to c \in {Chain}_{Field} \underset{˙}{<}$
61	60	chnwrd	$⊢ (((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \to c \in Word Field$
62		lswccats1	$⊢ (c \in Word Field \land g \in Field) \to lastS (c ++ ⟨“ g ”⟩) = g$
63	61 57 62	syl2an2r	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to lastS (c ++ ⟨“ g ”⟩) = g$
64		simpr	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to c = \emptyset$
65	64	oveq1d	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to c ++ ⟨“ g ”⟩ = \emptyset ++ ⟨“ g ”⟩$
66		s0s1	$⊢ ⟨“ g ”⟩ = \emptyset ++ ⟨“ g ”⟩$
67	65 66	eqtr4di	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to c ++ ⟨“ g ”⟩ = ⟨“ g ”⟩$
68	67	fveq1d	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to (c ++ ⟨“ g ”⟩) (0) = ⟨“ g ”⟩ (0)$
69		s1fv	$⊢ g \in Field \to ⟨“ g ”⟩ (0) = g$
70	57 69	syl	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to ⟨“ g ”⟩ (0) = g$
71	68 70	eqtrd	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to (c ++ ⟨“ g ”⟩) (0) = g$
72	59 63 71	3brtr4d	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0)$
73		oveq2	$⊢ m = 0 \to 2^{m} = 2^{0}$
74		2cn	$⊢ 2 \in ℂ$
75		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
76	74 75	ax-mp	$⊢ 2^{0} = 1$
77	73 76	eqtrdi	$⊢ m = 0 \to 2^{m} = 1$
78	77	eqeq2d	$⊢ m = 0 \to (lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m} \leftrightarrow lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 1)$
79		0nn0	$⊢ 0 \in ℕ_{0}$
80	79	a1i	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to 0 \in ℕ_{0}$
81	63 71	oveq12d	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = g [. : .] g$
82		extdgid	$⊢ g \in Field \to g [. : .] g = 1$
83	57 82	syl	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to g [. : .] g = 1$
84	81 83	eqtrd	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 1$
85	78 80 84	rspcedvdw	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}$
86	72 85	jca	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c = \emptyset) \to (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})$
87		simp-6r	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to (c = \emptyset \lor lastS (c) \underset{˙}{<} g)$
88		simpllr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to c \neq \emptyset$
89	88	neneqd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to \neg c = \emptyset$
90	87 89	orcnd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c) \underset{˙}{<} g$
91	61	ad3antrrr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to c \in Word Field$
92		lswcl	$⊢ (c \in Word Field \land c \neq \emptyset) \to lastS (c) \in Field$
93	91 88 92	syl2anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c) \in Field$
94		simp-7r	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to g \in Field$
95		breq12	$⊢ (e = g \land f = lastS (c)) \to (e /_{FldExt} f \leftrightarrow g /_{FldExt} lastS (c))$
96		oveq12	$⊢ (e = g \land f = lastS (c)) \to e [. : .] f = g [. : .] lastS (c)$
97	96	eqeq1d	$⊢ (e = g \land f = lastS (c)) \to (e [. : .] f = 2 \leftrightarrow g [. : .] lastS (c) = 2)$
98	95 97	anbi12d	$⊢ (e = g \land f = lastS (c)) \to ((e /_{FldExt} f \land e [. : .] f = 2) \leftrightarrow (g /_{FldExt} lastS (c) \land g [. : .] lastS (c) = 2))$
99	98	ancoms	$⊢ (f = lastS (c) \land e = g) \to ((e /_{FldExt} f \land e [. : .] f = 2) \leftrightarrow (g /_{FldExt} lastS (c) \land g [. : .] lastS (c) = 2))$
100	99 1	brabga	$⊢ (lastS (c) \in Field \land g \in Field) \to (lastS (c) \underset{˙}{<} g \leftrightarrow (g /_{FldExt} lastS (c) \land g [. : .] lastS (c) = 2))$
101	93 94 100	syl2anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to (lastS (c) \underset{˙}{<} g \leftrightarrow (g /_{FldExt} lastS (c) \land g [. : .] lastS (c) = 2))$
102	90 101	mpbid	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to (g /_{FldExt} lastS (c) \land g [. : .] lastS (c) = 2)$
103	102	simpld	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to g /_{FldExt} lastS (c)$
104		hashgt0	$⊢ (c \in {Chain}_{Field} \underset{˙}{<} \land c \neq \emptyset) \to 0 < \|c\|$
105	60 104	sylan	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to 0 < \|c\|$
106		simpllr	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))$
107	105 106	mpd	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n})$
108	107	simprd	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}$
109		oveq2	$⊢ n = o \to 2^{n} = 2^{o}$
110	109	eqeq2d	$⊢ n = o \to (lastS (c) [. : .] c (0) = 2^{n} \leftrightarrow lastS (c) [. : .] c (0) = 2^{o})$
111	110	cbvrexvw	$⊢ \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n} \leftrightarrow \exists o \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{o}$
112	108 111	sylib	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to \exists o \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{o}$
113	103 112	r19.29a	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to g /_{FldExt} lastS (c)$
114	107	simpld	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to lastS (c) /_{FldExt} c (0)$
115		fldexttr	$⊢ (g /_{FldExt} lastS (c) \land lastS (c) /_{FldExt} c (0)) \to g /_{FldExt} c (0)$
116	113 114 115	syl2anc	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to g /_{FldExt} c (0)$
117	91 94 62	syl2anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c ++ ⟨“ g ”⟩) = g$
118	117 112	r19.29a	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to lastS (c ++ ⟨“ g ”⟩) = g$
119	94	s1cld	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to ⟨“ g ”⟩ \in Word Field$
120	105	ad2antrr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 0 < \|c\|$
121		ccatfv0	$⊢ (c \in Word Field \land ⟨“ g ”⟩ \in Word Field \land 0 < \|c\|) \to (c ++ ⟨“ g ”⟩) (0) = c (0)$
122	91 119 120 121	syl3anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to (c ++ ⟨“ g ”⟩) (0) = c (0)$
123	122 112	r19.29a	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to (c ++ ⟨“ g ”⟩) (0) = c (0)$
124	116 118 123	3brtr4d	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0)$
125		oveq2	$⊢ m = o + 1 \to 2^{m} = 2^{o + 1}$
126	125	eqeq2d	$⊢ m = o + 1 \to (lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m} \leftrightarrow lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{o + 1})$
127		simplr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to o \in ℕ_{0}$
128		1nn0	$⊢ 1 \in ℕ_{0}$
129	128	a1i	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 1 \in ℕ_{0}$
130	127 129	nn0addcld	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to o + 1 \in ℕ_{0}$
131	117 122	oveq12d	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = g [. : .] c (0)$
132	114	ad2antrr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c) /_{FldExt} c (0)$
133		extdgmul	$⊢ (g /_{FldExt} lastS (c) \land lastS (c) /_{FldExt} c (0)) \to g [. : .] c (0) = [g : lastS (c)] \cdot_{𝑒} [lastS (c) : c (0)]$
134	103 132 133	syl2anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to g [. : .] c (0) = [g : lastS (c)] \cdot_{𝑒} [lastS (c) : c (0)]$
135		2cnd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2 \in ℂ$
136	135 127	expcld	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2^{o} \in ℂ$
137	135 136	mulcomd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2 2^{o} = 2^{o} \cdot 2$
138	102	simprd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to g [. : .] lastS (c) = 2$
139		simpr	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c) [. : .] c (0) = 2^{o}$
140	138 139	oveq12d	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to [g : lastS (c)] \cdot_{𝑒} [lastS (c) : c (0)] = 2 \cdot_{𝑒} 2^{o}$
141		2re	$⊢ 2 \in ℝ$
142	141	a1i	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2 \in ℝ$
143	142 127	reexpcld	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2^{o} \in ℝ$
144		rexmul	$⊢ (2 \in ℝ \land 2^{o} \in ℝ) \to 2 \cdot_{𝑒} 2^{o} = 2 2^{o}$
145	142 143 144	syl2anc	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2 \cdot_{𝑒} 2^{o} = 2 2^{o}$
146	140 145	eqtrd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to [g : lastS (c)] \cdot_{𝑒} [lastS (c) : c (0)] = 2 2^{o}$
147	135 127	expp1d	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to 2^{o + 1} = 2^{o} \cdot 2$
148	137 146 147	3eqtr4d	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to [g : lastS (c)] \cdot_{𝑒} [lastS (c) : c (0)] = 2^{o + 1}$
149	131 134 148	3eqtrd	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{o + 1}$
150	126 130 149	rspcedvdw	$⊢ ((((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \land o \in ℕ_{0}) \land lastS (c) [. : .] c (0) = 2^{o}) \to \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}$
151	150 112	r19.29a	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}$
152	124 151	jca	$⊢ ((((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \land c \neq \emptyset) \to (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})$
153	86 152	pm2.61dane	$⊢ (((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \land 0 < \|c ++ ⟨“ g ”⟩\|) \to (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m})$
154	153	ex	$⊢ ((((φ \land c \in {Chain}_{Field} \underset{˙}{<}) \land g \in Field) \land (c = \emptyset \lor lastS (c) \underset{˙}{<} g)) \land (0 < \|c\| \to (lastS (c) /_{FldExt} c (0) \land \exists n \in ℕ_{0} lastS (c) [. : .] c (0) = 2^{n}))) \to (0 < \|c ++ ⟨“ g ”⟩\| \to (lastS (c ++ ⟨“ g ”⟩) /_{FldExt} (c ++ ⟨“ g ”⟩) (0) \land \exists m \in ℕ_{0} lastS (c ++ ⟨“ g ”⟩) [. : .] (c ++ ⟨“ g ”⟩) (0) = 2^{m}))$
155	15 25 39 49 2 56 154	chnind	$⊢ φ \to (0 < \|T\| \to (lastS (T) /_{FldExt} T (0) \land \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n}))$
156	5 155	mpd	$⊢ φ \to (lastS (T) /_{FldExt} T (0) \land \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n})$
157	156	simprd	$⊢ φ \to \exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n}$
158	4 3	oveq12d	$⊢ φ \to lastS (T) [. : .] T (0) = F [. : .] Q$
159	158	eqeq1d	$⊢ φ \to (lastS (T) [. : .] T (0) = 2^{n} \leftrightarrow F [. : .] Q = 2^{n})$
160	159	rexbidv	$⊢ φ \to (\exists n \in ℕ_{0} lastS (T) [. : .] T (0) = 2^{n} \leftrightarrow \exists n \in ℕ_{0} F [. : .] Q = 2^{n})$
161	157 160	mpbid	$⊢ φ \to \exists n \in ℕ_{0} F [. : .] Q = 2^{n}$

Metamath Proof Explorer

Theorem fldext2chn

Proof