radcnvrat

Description: Let L be the limit, if one exists, of the ratio ( abs( ( A( k + 1 ) ) / ( Ak ) ) ) (as in the ratio test cvgdvgrat ) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( An ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020)

	Ref	Expression
Hypotheses	radcnvrat.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	radcnvrat.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	radcnvrat.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	radcnvrat.rat	$⊢ D = (k \in ℕ_{0} ⟼ \|\frac{A (k + 1)}{A (k)}\|)$
	radcnvrat.z	$⊢ Z = ℤ_{\geq M}$
	radcnvrat.m	$⊢ φ \to M \in ℕ_{0}$
	radcnvrat.n0	$⊢ (φ \land k \in Z) \to A (k) \neq 0$
	radcnvrat.l	$⊢ φ \to D ⇝ L$
	radcnvrat.ln0	$⊢ φ \to L \neq 0$
Assertion	radcnvrat	$⊢ φ \to R = \frac{1}{L}$

Proof

Step	Hyp	Ref	Expression
1		radcnvrat.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		radcnvrat.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
3		radcnvrat.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
4		radcnvrat.rat	$⊢ D = (k \in ℕ_{0} ⟼ \|\frac{A (k + 1)}{A (k)}\|)$
5		radcnvrat.z	$⊢ Z = ℤ_{\geq M}$
6		radcnvrat.m	$⊢ φ \to M \in ℕ_{0}$
7		radcnvrat.n0	$⊢ (φ \land k \in Z) \to A (k) \neq 0$
8		radcnvrat.l	$⊢ φ \to D ⇝ L$
9		radcnvrat.ln0	$⊢ φ \to L \neq 0$
10		xrltso	$⊢ < Or ℝ^{*}$
11	10	a1i	$⊢ φ \to < Or ℝ^{*}$
12	6	nn0zd	$⊢ φ \to M \in ℤ$
13	5	reseq2i	$⊢ {D ↾}_{Z} = {D ↾}_{ℤ_{\geq M}}$
14		nn0ex	$⊢ ℕ_{0} \in V$
15	14	mptex	$⊢ (k \in ℕ_{0} ⟼ \|\frac{A (k + 1)}{A (k)}\|) \in V$
16	4 15	eqeltri	$⊢ D \in V$
17		climres	$⊢ (M \in ℤ \land D \in V) \to (({D ↾}_{ℤ_{\geq M}}) ⇝ L \leftrightarrow D ⇝ L)$
18	12 16 17	sylancl	$⊢ φ \to (({D ↾}_{ℤ_{\geq M}}) ⇝ L \leftrightarrow D ⇝ L)$
19	8 18	mpbird	$⊢ φ \to ({D ↾}_{ℤ_{\geq M}}) ⇝ L$
20	13 19	eqbrtrid	$⊢ φ \to ({D ↾}_{Z}) ⇝ L$
21	4	reseq1i	$⊢ {D ↾}_{Z} = {(k \in ℕ_{0} ⟼ \|\frac{A (k + 1)}{A (k)}\|) ↾}_{Z}$
22		eluznn0	$⊢ (M \in ℕ_{0} \land k \in ℤ_{\geq M}) \to k \in ℕ_{0}$
23	6 22	sylan	$⊢ (φ \land k \in ℤ_{\geq M}) \to k \in ℕ_{0}$
24	23	ex	$⊢ φ \to (k \in ℤ_{\geq M} \to k \in ℕ_{0})$
25	24	ssrdv	$⊢ φ \to ℤ_{\geq M} \subseteq ℕ_{0}$
26	5 25	eqsstrid	$⊢ φ \to Z \subseteq ℕ_{0}$
27	26	resmptd	$⊢ φ \to {(k \in ℕ_{0} ⟼ \|\frac{A (k + 1)}{A (k)}\|) ↾}_{Z} = (k \in Z ⟼ \|\frac{A (k + 1)}{A (k)}\|)$
28	21 27	eqtrid	$⊢ φ \to {D ↾}_{Z} = (k \in Z ⟼ \|\frac{A (k + 1)}{A (k)}\|)$
29		fvexd	$⊢ (φ \land k \in Z) \to \|\frac{A (k + 1)}{A (k)}\| \in V$
30	28 29	fvmpt2d	$⊢ (φ \land k \in Z) \to ({D ↾}_{Z}) (k) = \|\frac{A (k + 1)}{A (k)}\|$
31	5	peano2uzs	$⊢ k \in Z \to k + 1 \in Z$
32	26	sselda	$⊢ (φ \land k + 1 \in Z) \to k + 1 \in ℕ_{0}$
33	2	ffvelcdmda	$⊢ (φ \land k + 1 \in ℕ_{0}) \to A (k + 1) \in ℂ$
34	32 33	syldan	$⊢ (φ \land k + 1 \in Z) \to A (k + 1) \in ℂ$
35	31 34	sylan2	$⊢ (φ \land k \in Z) \to A (k + 1) \in ℂ$
36	26	sselda	$⊢ (φ \land k \in Z) \to k \in ℕ_{0}$
37	2	ffvelcdmda	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in ℂ$
38	36 37	syldan	$⊢ (φ \land k \in Z) \to A (k) \in ℂ$
39	35 38 7	divcld	$⊢ (φ \land k \in Z) \to \frac{A (k + 1)}{A (k)} \in ℂ$
40	39	abscld	$⊢ (φ \land k \in Z) \to \|\frac{A (k + 1)}{A (k)}\| \in ℝ$
41	30 40	eqeltrd	$⊢ (φ \land k \in Z) \to ({D ↾}_{Z}) (k) \in ℝ$
42	5 12 20 41	climrecl	$⊢ φ \to L \in ℝ$
43	42 9	rereccld	$⊢ φ \to \frac{1}{L} \in ℝ$
44	43	rexrd	$⊢ φ \to \frac{1}{L} \in ℝ^{*}$
45		simpr	$⊢ (φ \land x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
46		elrabi	$⊢ x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \to x \in ℝ$
47	43	adantr	$⊢ (φ \land x \in ℝ) \to \frac{1}{L} \in ℝ$
48		recn	$⊢ x \in ℝ \to x \in ℂ$
49	48	abscld	$⊢ x \in ℝ \to \|x\| \in ℝ$
50	49	adantl	$⊢ (φ \land x \in ℝ) \to \|x\| \in ℝ$
51	47 50	ltlend	$⊢ (φ \land x \in ℝ) \to (\frac{1}{L} < \|x\| \leftrightarrow (\frac{1}{L} \leq \|x\| \land \|x\| \neq \frac{1}{L}))$
52	51	simplbda	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < \|x\|) \to \|x\| \neq \frac{1}{L}$
53	51	adantr	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} < \|x\| \leftrightarrow (\frac{1}{L} \leq \|x\| \land \|x\| \neq \frac{1}{L}))$
54		simpr	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to \|x\| \neq \frac{1}{L}$
55	54	biantrud	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} \leq \|x\| \leftrightarrow (\frac{1}{L} \leq \|x\| \land \|x\| \neq \frac{1}{L}))$
56	47 50	lenltd	$⊢ (φ \land x \in ℝ) \to (\frac{1}{L} \leq \|x\| \leftrightarrow \neg \|x\| < \frac{1}{L})$
57	56	adantr	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} \leq \|x\| \leftrightarrow \neg \|x\| < \frac{1}{L})$
58	53 55 57	3bitr2d	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} < \|x\| \leftrightarrow \neg \|x\| < \frac{1}{L})$
59		1cnd	$⊢ (φ \land x \in ℝ) \to 1 \in ℂ$
60	50	recnd	$⊢ (φ \land x \in ℝ) \to \|x\| \in ℂ$
61	42	recnd	$⊢ φ \to L \in ℂ$
62	61	adantr	$⊢ (φ \land x \in ℝ) \to L \in ℂ$
63	9	adantr	$⊢ (φ \land x \in ℝ) \to L \neq 0$
64	59 60 62 63	divmul3d	$⊢ (φ \land x \in ℝ) \to (\frac{1}{L} = \|x\| \leftrightarrow 1 = \|x\| L)$
65		eqcom	$⊢ \frac{1}{L} = \|x\| \leftrightarrow \|x\| = \frac{1}{L}$
66		eqcom	$⊢ 1 = \|x\| L \leftrightarrow \|x\| L = 1$
67	64 65 66	3bitr3g	$⊢ (φ \land x \in ℝ) \to (\|x\| = \frac{1}{L} \leftrightarrow \|x\| L = 1)$
68	67	necon3bid	$⊢ (φ \land x \in ℝ) \to (\|x\| \neq \frac{1}{L} \leftrightarrow \|x\| L \neq 1)$
69	68	biimpa	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to \|x\| L \neq 1$
70		1red	$⊢ (φ \land x \in ℝ) \to 1 \in ℝ$
71		fvres	$⊢ k \in Z \to ({D ↾}_{Z}) (k) = D (k)$
72	71	adantl	$⊢ (φ \land k \in Z) \to ({D ↾}_{Z}) (k) = D (k)$
73	72 41	eqeltrrd	$⊢ (φ \land k \in Z) \to D (k) \in ℝ$
74	39	absge0d	$⊢ (φ \land k \in Z) \to 0 \leq \|\frac{A (k + 1)}{A (k)}\|$
75	74 30	breqtrrd	$⊢ (φ \land k \in Z) \to 0 \leq ({D ↾}_{Z}) (k)$
76	75 72	breqtrd	$⊢ (φ \land k \in Z) \to 0 \leq D (k)$
77	5 12 8 73 76	climge0	$⊢ φ \to 0 \leq L$
78	42 77 9	ne0gt0d	$⊢ φ \to 0 < L$
79	42 78	elrpd	$⊢ φ \to L \in ℝ^{+}$
80	79	adantr	$⊢ (φ \land x \in ℝ) \to L \in ℝ^{+}$
81	50 70 80	ltmuldivd	$⊢ (φ \land x \in ℝ) \to (\|x\| L < 1 \leftrightarrow \|x\| < \frac{1}{L})$
82	81	adantr	$⊢ ((φ \land x \in ℝ) \land \|x\| L \neq 1) \to (\|x\| L < 1 \leftrightarrow \|x\| < \frac{1}{L})$
83		elun	$⊢ x \in ((ℝ \cap \{0\}) \cup (ℝ ∖ \{0\})) \leftrightarrow (x \in (ℝ \cap \{0\}) \lor x \in (ℝ ∖ \{0\}))$
84		inundif	$⊢ (ℝ \cap \{0\}) \cup (ℝ ∖ \{0\}) = ℝ$
85	84	eleq2i	$⊢ x \in ((ℝ \cap \{0\}) \cup (ℝ ∖ \{0\})) \leftrightarrow x \in ℝ$
86	83 85	bitr3i	$⊢ (x \in (ℝ \cap \{0\}) \lor x \in (ℝ ∖ \{0\})) \leftrightarrow x \in ℝ$
87		elin	$⊢ x \in (ℝ \cap \{0\}) \leftrightarrow (x \in ℝ \land x \in \{0\})$
88	87	simprbi	$⊢ x \in (ℝ \cap \{0\}) \to x \in \{0\}$
89		elsni	$⊢ x \in \{0\} \to x = 0$
90	88 89	syl	$⊢ x \in (ℝ \cap \{0\}) \to x = 0$
91		fveq2	$⊢ x = 0 \to \|x\| = \|0\|$
92		abs0	$⊢ \|0\| = 0$
93	91 92	eqtrdi	$⊢ x = 0 \to \|x\| = 0$
94	93	oveq1d	$⊢ x = 0 \to \|x\| L = 0 \cdot L$
95	61	mul02d	$⊢ φ \to 0 \cdot L = 0$
96	94 95	sylan9eqr	$⊢ (φ \land x = 0) \to \|x\| L = 0$
97		0lt1	$⊢ 0 < 1$
98	96 97	eqbrtrdi	$⊢ (φ \land x = 0) \to \|x\| L < 1$
99	1 2	radcnv0	$⊢ φ \to 0 \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
100		eleq1	$⊢ x = 0 \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \leftrightarrow 0 \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
101	99 100	syl5ibrcom	$⊢ φ \to (x = 0 \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
102	101	imp	$⊢ (φ \land x = 0) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
103	98 102	2thd	$⊢ (φ \land x = 0) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
104	90 103	sylan2	$⊢ (φ \land x \in (ℝ \cap \{0\})) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
105	104	adantlr	$⊢ ((φ \land \|x\| L \neq 1) \land x \in (ℝ \cap \{0\})) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
106		ax-resscn	$⊢ ℝ \subseteq ℂ$
107		ssdif	$⊢ ℝ \subseteq ℂ \to ℝ ∖ \{0\} \subseteq ℂ ∖ \{0\}$
108	106 107	ax-mp	$⊢ ℝ ∖ \{0\} \subseteq ℂ ∖ \{0\}$
109	108	sseli	$⊢ x \in (ℝ ∖ \{0\}) \to x \in (ℂ ∖ \{0\})$
110		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
111	6	ad2antrr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \to M \in ℕ_{0}$
112		fvexd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \to G (x) \in V$
113		eldifi	$⊢ x \in (ℂ ∖ \{0\}) \to x \in ℂ$
114	1	a1i	$⊢ φ \to G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
115	14	mptex	$⊢ (n \in ℕ_{0} ⟼ A (n) x^{n}) \in V$
116	115	a1i	$⊢ (φ \land x \in ℂ) \to (n \in ℕ_{0} ⟼ A (n) x^{n}) \in V$
117	114 116	fvmpt2d	$⊢ (φ \land x \in ℂ) \to G (x) = (n \in ℕ_{0} ⟼ A (n) x^{n})$
118	117	adantr	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to G (x) = (n \in ℕ_{0} ⟼ A (n) x^{n})$
119		fveq2	$⊢ n = k \to A (n) = A (k)$
120		oveq2	$⊢ n = k \to x^{n} = x^{k}$
121	119 120	oveq12d	$⊢ n = k \to A (n) x^{n} = A (k) x^{k}$
122	121	adantl	$⊢ (((φ \land x \in ℂ) \land k \in ℕ_{0}) \land n = k) \to A (n) x^{n} = A (k) x^{k}$
123		simpr	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
124		ovexd	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to A (k) x^{k} \in V$
125	118 122 123 124	fvmptd	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to G (x) (k) = A (k) x^{k}$
126	37	adantlr	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
127		simplr	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to x \in ℂ$
128	127 123	expcld	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to x^{k} \in ℂ$
129	126 128	mulcld	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to A (k) x^{k} \in ℂ$
130	125 129	eqeltrd	$⊢ ((φ \land x \in ℂ) \land k \in ℕ_{0}) \to G (x) (k) \in ℂ$
131	113 130	sylanl2	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in ℕ_{0}) \to G (x) (k) \in ℂ$
132	131	adantlr	$⊢ (((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \land k \in ℕ_{0}) \to G (x) (k) \in ℂ$
133	36	adantlr	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to k \in ℕ_{0}$
134	133 125	syldan	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to G (x) (k) = A (k) x^{k}$
135	113 134	sylanl2	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to G (x) (k) = A (k) x^{k}$
136	38	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to A (k) \in ℂ$
137	113	adantl	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to x \in ℂ$
138	137	adantr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x \in ℂ$
139	36	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k \in ℕ_{0}$
140	138 139	expcld	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{k} \in ℂ$
141	7	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to A (k) \neq 0$
142		eldifsni	$⊢ x \in (ℂ ∖ \{0\}) \to x \neq 0$
143	142	ad2antlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x \neq 0$
144	139	nn0zd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k \in ℤ$
145	138 143 144	expne0d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{k} \neq 0$
146	136 140 141 145	mulne0d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to A (k) x^{k} \neq 0$
147	135 146	eqnetrd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to G (x) (k) \neq 0$
148	147	adantlr	$⊢ (((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \land k \in Z) \to G (x) (k) \neq 0$
149		fvoveq1	$⊢ n = k \to G (x) (n + 1) = G (x) (k + 1)$
150		fveq2	$⊢ n = k \to G (x) (n) = G (x) (k)$
151	149 150	oveq12d	$⊢ n = k \to \frac{G (x) (n + 1)}{G (x) (n)} = \frac{G (x) (k + 1)}{G (x) (k)}$
152	151	fveq2d	$⊢ n = k \to \|\frac{G (x) (n + 1)}{G (x) (n)}\| = \|\frac{G (x) (k + 1)}{G (x) (k)}\|$
153	152	cbvmptv	$⊢ (n \in Z ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) = (k \in Z ⟼ \|\frac{G (x) (k + 1)}{G (x) (k)}\|)$
154	5	reseq2i	$⊢ {(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{Z} = {(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{ℤ_{\geq M}}$
155	26	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to Z \subseteq ℕ_{0}$
156	155	resmptd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{Z} = (n \in Z ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|)$
157	154 156	eqtr3id	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to {(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{ℤ_{\geq M}} = (n \in Z ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|)$
158	12	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to M \in ℤ$
159	8	adantr	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to D ⇝ L$
160	137	abscld	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \in ℝ$
161	160	recnd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to \|x\| \in ℂ$
162	14	mptex	$⊢ (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) \in V$
163	162	a1i	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) \in V$
164	73	recnd	$⊢ (φ \land k \in Z) \to D (k) \in ℂ$
165	164	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to D (k) \in ℂ$
166		eqidd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) = (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|)$
167	152	adantl	$⊢ (((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \land n = k) \to \|\frac{G (x) (n + 1)}{G (x) (n)}\| = \|\frac{G (x) (k + 1)}{G (x) (k)}\|$
168		fvexd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|\frac{G (x) (k + 1)}{G (x) (k)}\| \in V$
169	166 167 139 168	fvmptd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) (k) = \|\frac{G (x) (k + 1)}{G (x) (k)}\|$
170	117	adantr	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to G (x) = (n \in ℕ_{0} ⟼ A (n) x^{n})$
171		simpr	$⊢ (((φ \land x \in ℂ) \land k \in Z) \land n = k + 1) \to n = k + 1$
172	171	fveq2d	$⊢ (((φ \land x \in ℂ) \land k \in Z) \land n = k + 1) \to A (n) = A (k + 1)$
173	171	oveq2d	$⊢ (((φ \land x \in ℂ) \land k \in Z) \land n = k + 1) \to x^{n} = x^{k + 1}$
174	172 173	oveq12d	$⊢ (((φ \land x \in ℂ) \land k \in Z) \land n = k + 1) \to A (n) x^{n} = A (k + 1) x^{k + 1}$
175		1nn0	$⊢ 1 \in ℕ_{0}$
176	175	a1i	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to 1 \in ℕ_{0}$
177	133 176	nn0addcld	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to k + 1 \in ℕ_{0}$
178		ovexd	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to A (k + 1) x^{k + 1} \in V$
179	170 174 177 178	fvmptd	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to G (x) (k + 1) = A (k + 1) x^{k + 1}$
180	121	adantl	$⊢ (((φ \land x \in ℂ) \land k \in Z) \land n = k) \to A (n) x^{n} = A (k) x^{k}$
181		ovexd	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to A (k) x^{k} \in V$
182	170 180 133 181	fvmptd	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to G (x) (k) = A (k) x^{k}$
183	179 182	oveq12d	$⊢ ((φ \land x \in ℂ) \land k \in Z) \to \frac{G (x) (k + 1)}{G (x) (k)} = \frac{A (k + 1) x^{k + 1}}{A (k) x^{k}}$
184	113 183	sylanl2	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \frac{G (x) (k + 1)}{G (x) (k)} = \frac{A (k + 1) x^{k + 1}}{A (k) x^{k}}$
185	35	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to A (k + 1) \in ℂ$
186	113 177	sylanl2	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k + 1 \in ℕ_{0}$
187	138 186	expcld	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{k + 1} \in ℂ$
188	185 136 187 140 141 145	divmuldivd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (\frac{A (k + 1)}{A (k)}) (\frac{x^{k + 1}}{x^{k}}) = \frac{A (k + 1) x^{k + 1}}{A (k) x^{k}}$
189	139	nn0cnd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k \in ℂ$
190		1cnd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to 1 \in ℂ$
191	189 190	pncan2d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k + 1 - k = 1$
192	191	oveq2d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{k + 1 - k} = x^{1}$
193	186	nn0zd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to k + 1 \in ℤ$
194	138 143 144 193	expsubd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{k + 1 - k} = \frac{x^{k + 1}}{x^{k}}$
195	138	exp1d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to x^{1} = x$
196	192 194 195	3eqtr3d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \frac{x^{k + 1}}{x^{k}} = x$
197	196	oveq2d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (\frac{A (k + 1)}{A (k)}) (\frac{x^{k + 1}}{x^{k}}) = (\frac{A (k + 1)}{A (k)}) x$
198	184 188 197	3eqtr2d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \frac{G (x) (k + 1)}{G (x) (k)} = (\frac{A (k + 1)}{A (k)}) x$
199	198	fveq2d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|\frac{G (x) (k + 1)}{G (x) (k)}\| = \|(\frac{A (k + 1)}{A (k)}) x\|$
200	39	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \frac{A (k + 1)}{A (k)} \in ℂ$
201	200 138	absmuld	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|(\frac{A (k + 1)}{A (k)}) x\| = \|\frac{A (k + 1)}{A (k)}\| \|x\|$
202	169 199 201	3eqtrd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) (k) = \|\frac{A (k + 1)}{A (k)}\| \|x\|$
203	72 30	eqtr3d	$⊢ (φ \land k \in Z) \to D (k) = \|\frac{A (k + 1)}{A (k)}\|$
204	203	adantlr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to D (k) = \|\frac{A (k + 1)}{A (k)}\|$
205	204	eqcomd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|\frac{A (k + 1)}{A (k)}\| = D (k)$
206	205	oveq1d	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|\frac{A (k + 1)}{A (k)}\| \|x\| = D (k) \|x\|$
207	161	adantr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to \|x\| \in ℂ$
208	165 207	mulcomd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to D (k) \|x\| = \|x\| D (k)$
209	202 206 208	3eqtrd	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land k \in Z) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) (k) = \|x\| D (k)$
210	5 158 159 161 163 165 209	climmulc2	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ⇝ \|x\| L$
211		climres	$⊢ (M \in ℤ \land (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) \in V) \to (({(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{ℤ_{\geq M}}) ⇝ \|x\| L \leftrightarrow (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ⇝ \|x\| L)$
212	158 162 211	sylancl	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to (({(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{ℤ_{\geq M}}) ⇝ \|x\| L \leftrightarrow (n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ⇝ \|x\| L)$
213	210 212	mpbird	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to ({(n \in ℕ_{0} ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ↾}_{ℤ_{\geq M}}) ⇝ \|x\| L$
214	157 213	eqbrtrrd	$⊢ (φ \land x \in (ℂ ∖ \{0\})) \to (n \in Z ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ⇝ \|x\| L$
215	214	adantr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \to (n \in Z ⟼ \|\frac{G (x) (n + 1)}{G (x) (n)}\|) ⇝ \|x\| L$
216		simpr	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \to \|x\| L \neq 1$
217	110 5 111 112 132 148 153 215 216	cvgdvgrat	$⊢ ((φ \land x \in (ℂ ∖ \{0\})) \land \|x\| L \neq 1) \to (\|x\| L < 1 \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
218	109 217	sylanl2	$⊢ ((φ \land x \in (ℝ ∖ \{0\})) \land \|x\| L \neq 1) \to (\|x\| L < 1 \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
219		eldifi	$⊢ x \in (ℝ ∖ \{0\}) \to x \in ℝ$
220		fveq2	$⊢ r = x \to G (r) = G (x)$
221	220	seqeq3d	$⊢ r = x \to seq 0 (+ G (r)) = seq 0 (+ G (x))$
222	221	eleq1d	$⊢ r = x \to (seq 0 (+ G (r)) \in dom ⇝ \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
223	222	elrab3	$⊢ x \in ℝ \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
224	219 223	syl	$⊢ x \in (ℝ ∖ \{0\}) \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
225	224	ad2antlr	$⊢ ((φ \land x \in (ℝ ∖ \{0\})) \land \|x\| L \neq 1) \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \leftrightarrow seq 0 (+ G (x)) \in dom ⇝)$
226	218 225	bitr4d	$⊢ ((φ \land x \in (ℝ ∖ \{0\})) \land \|x\| L \neq 1) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
227	226	an32s	$⊢ ((φ \land \|x\| L \neq 1) \land x \in (ℝ ∖ \{0\})) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
228	105 227	jaodan	$⊢ ((φ \land \|x\| L \neq 1) \land (x \in (ℝ \cap \{0\}) \lor x \in (ℝ ∖ \{0\}))) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
229	86 228	sylan2br	$⊢ ((φ \land \|x\| L \neq 1) \land x \in ℝ) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
230	229	an32s	$⊢ ((φ \land x \in ℝ) \land \|x\| L \neq 1) \to (\|x\| L < 1 \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
231	82 230	bitr3d	$⊢ ((φ \land x \in ℝ) \land \|x\| L \neq 1) \to (\|x\| < \frac{1}{L} \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
232	69 231	syldan	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\|x\| < \frac{1}{L} \leftrightarrow x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
233	232	notbid	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\neg \|x\| < \frac{1}{L} \leftrightarrow \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
234	58 233	bitrd	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} < \|x\| \leftrightarrow \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
235	234	biimpd	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\frac{1}{L} < \|x\| \to \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
236	235	impancom	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < \|x\|) \to (\|x\| \neq \frac{1}{L} \to \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
237	52 236	mpd	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < \|x\|) \to \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
238	237	ex	$⊢ (φ \land x \in ℝ) \to (\frac{1}{L} < \|x\| \to \neg x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
239	238	con2d	$⊢ (φ \land x \in ℝ) \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \to \neg \frac{1}{L} < \|x\|)$
240	47	adantr	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to \frac{1}{L} \in ℝ$
241		simplr	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to x \in ℝ$
242	50	adantr	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to \|x\| \in ℝ$
243		simpr	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to \frac{1}{L} < x$
244	241	leabsd	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to x \leq \|x\|$
245	240 241 242 243 244	ltletrd	$⊢ ((φ \land x \in ℝ) \land \frac{1}{L} < x) \to \frac{1}{L} < \|x\|$
246	245	ex	$⊢ (φ \land x \in ℝ) \to (\frac{1}{L} < x \to \frac{1}{L} < \|x\|)$
247	239 246	nsyld	$⊢ (φ \land x \in ℝ) \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \to \neg \frac{1}{L} < x)$
248	46 247	sylan2	$⊢ (φ \land x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}) \to (x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \to \neg \frac{1}{L} < x)$
249	45 248	mpd	$⊢ (φ \land x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}) \to \neg \frac{1}{L} < x$
250	43	renegcld	$⊢ φ \to - \frac{1}{L} \in ℝ$
251	250	rexrd	$⊢ φ \to - \frac{1}{L} \in ℝ^{*}$
252		iooss1	$⊢ (- \frac{1}{L} \in ℝ^{*} \land - \frac{1}{L} \leq x) \to (x, \frac{1}{L}) \subseteq (- \frac{1}{L}, \frac{1}{L})$
253	251 252	sylan	$⊢ (φ \land - \frac{1}{L} \leq x) \to (x, \frac{1}{L}) \subseteq (- \frac{1}{L}, \frac{1}{L})$
254	253	adantlr	$⊢ ((φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \land - \frac{1}{L} \leq x) \to (x, \frac{1}{L}) \subseteq (- \frac{1}{L}, \frac{1}{L})$
255		eliooord	$⊢ k \in (x, \frac{1}{L}) \to (x < k \land k < \frac{1}{L})$
256	255	simpld	$⊢ k \in (x, \frac{1}{L}) \to x < k$
257	256	rgen	$⊢ \forall k \in (x, \frac{1}{L}) x < k$
258		ioon0	$⊢ (x \in ℝ^{} \land \frac{1}{L} \in ℝ^{}) \to ((x, \frac{1}{L}) \neq \emptyset \leftrightarrow x < \frac{1}{L})$
259	44 258	sylan2	$⊢ (x \in ℝ^{*} \land φ) \to ((x, \frac{1}{L}) \neq \emptyset \leftrightarrow x < \frac{1}{L})$
260	259	ancoms	$⊢ (φ \land x \in ℝ^{*}) \to ((x, \frac{1}{L}) \neq \emptyset \leftrightarrow x < \frac{1}{L})$
261	260	biimpar	$⊢ ((φ \land x \in ℝ^{*}) \land x < \frac{1}{L}) \to (x, \frac{1}{L}) \neq \emptyset$
262		r19.2zb	$⊢ (x, \frac{1}{L}) \neq \emptyset \leftrightarrow (\forall k \in (x, \frac{1}{L}) x < k \to \exists k \in (x, \frac{1}{L}) x < k)$
263	261 262	sylib	$⊢ ((φ \land x \in ℝ^{*}) \land x < \frac{1}{L}) \to (\forall k \in (x, \frac{1}{L}) x < k \to \exists k \in (x, \frac{1}{L}) x < k)$
264	257 263	mpi	$⊢ ((φ \land x \in ℝ^{*}) \land x < \frac{1}{L}) \to \exists k \in (x, \frac{1}{L}) x < k$
265	264	anasss	$⊢ (φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \to \exists k \in (x, \frac{1}{L}) x < k$
266	265	adantr	$⊢ ((φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \land - \frac{1}{L} \leq x) \to \exists k \in (x, \frac{1}{L}) x < k$
267		ssrexv	$⊢ (x, \frac{1}{L}) \subseteq (- \frac{1}{L}, \frac{1}{L}) \to (\exists k \in (x, \frac{1}{L}) x < k \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k)$
268	254 266 267	sylc	$⊢ ((φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \land - \frac{1}{L} \leq x) \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k$
269		simplr	$⊢ ((φ \land x \in ℝ^{}) \land \neg - \frac{1}{L} \leq x) \to x \in ℝ^{}$
270		xrltnle	$⊢ (x \in ℝ^{} \land - \frac{1}{L} \in ℝ^{}) \to (x < - \frac{1}{L} \leftrightarrow \neg - \frac{1}{L} \leq x)$
271		xrltle	$⊢ (x \in ℝ^{} \land - \frac{1}{L} \in ℝ^{}) \to (x < - \frac{1}{L} \to x \leq - \frac{1}{L})$
272	270 271	sylbird	$⊢ (x \in ℝ^{} \land - \frac{1}{L} \in ℝ^{}) \to (\neg - \frac{1}{L} \leq x \to x \leq - \frac{1}{L})$
273	251 272	sylan2	$⊢ (x \in ℝ^{*} \land φ) \to (\neg - \frac{1}{L} \leq x \to x \leq - \frac{1}{L})$
274	273	ancoms	$⊢ (φ \land x \in ℝ^{*}) \to (\neg - \frac{1}{L} \leq x \to x \leq - \frac{1}{L})$
275	274	imp	$⊢ ((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \to x \leq - \frac{1}{L}$
276		iooss1	$⊢ (x \in ℝ^{*} \land x \leq - \frac{1}{L}) \to (- \frac{1}{L}, \frac{1}{L}) \subseteq (x, \frac{1}{L})$
277	269 275 276	syl2anc	$⊢ ((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \to (- \frac{1}{L}, \frac{1}{L}) \subseteq (x, \frac{1}{L})$
278	277	sselda	$⊢ (((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \land k \in (- \frac{1}{L}, \frac{1}{L})) \to k \in (x, \frac{1}{L})$
279	278 256	syl	$⊢ (((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \land k \in (- \frac{1}{L}, \frac{1}{L})) \to x < k$
280	279	ralrimiva	$⊢ ((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \to \forall k \in (- \frac{1}{L}, \frac{1}{L}) x < k$
281	42 78	recgt0d	$⊢ φ \to 0 < \frac{1}{L}$
282	43 43 281 281	addgt0d	$⊢ φ \to 0 < (\frac{1}{L}) + (\frac{1}{L})$
283	43	recnd	$⊢ φ \to \frac{1}{L} \in ℂ$
284	283 283	subnegd	$⊢ φ \to (\frac{1}{L}) - (- \frac{1}{L}) = (\frac{1}{L}) + (\frac{1}{L})$
285	282 284	breqtrrd	$⊢ φ \to 0 < (\frac{1}{L}) - (- \frac{1}{L})$
286	250 43	posdifd	$⊢ φ \to (- \frac{1}{L} < \frac{1}{L} \leftrightarrow 0 < (\frac{1}{L}) - (- \frac{1}{L}))$
287	285 286	mpbird	$⊢ φ \to - \frac{1}{L} < \frac{1}{L}$
288		ioon0	$⊢ (- \frac{1}{L} \in ℝ^{} \land \frac{1}{L} \in ℝ^{}) \to ((- \frac{1}{L}, \frac{1}{L}) \neq \emptyset \leftrightarrow - \frac{1}{L} < \frac{1}{L})$
289	251 44 288	syl2anc	$⊢ φ \to ((- \frac{1}{L}, \frac{1}{L}) \neq \emptyset \leftrightarrow - \frac{1}{L} < \frac{1}{L})$
290	287 289	mpbird	$⊢ φ \to (- \frac{1}{L}, \frac{1}{L}) \neq \emptyset$
291		r19.2zb	$⊢ (- \frac{1}{L}, \frac{1}{L}) \neq \emptyset \leftrightarrow (\forall k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k)$
292	290 291	sylib	$⊢ φ \to (\forall k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k)$
293	292	ad2antrr	$⊢ ((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \to (\forall k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k)$
294	280 293	mpd	$⊢ ((φ \land x \in ℝ^{*}) \land \neg - \frac{1}{L} \leq x) \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k$
295	294	adantlrr	$⊢ ((φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \land \neg - \frac{1}{L} \leq x) \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k$
296	268 295	pm2.61dan	$⊢ (φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \to \exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k$
297		elioo2	$⊢ (- \frac{1}{L} \in ℝ^{} \land \frac{1}{L} \in ℝ^{}) \to (x \in (- \frac{1}{L}, \frac{1}{L}) \leftrightarrow (x \in ℝ \land - \frac{1}{L} < x \land x < \frac{1}{L}))$
298	251 44 297	syl2anc	$⊢ φ \to (x \in (- \frac{1}{L}, \frac{1}{L}) \leftrightarrow (x \in ℝ \land - \frac{1}{L} < x \land x < \frac{1}{L}))$
299	298	biimpa	$⊢ (φ \land x \in (- \frac{1}{L}, \frac{1}{L})) \to (x \in ℝ \land - \frac{1}{L} < x \land x < \frac{1}{L})$
300		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
301	300 47	absltd	$⊢ (φ \land x \in ℝ) \to (\|x\| < \frac{1}{L} \leftrightarrow (- \frac{1}{L} < x \land x < \frac{1}{L}))$
302	50	adantr	$⊢ ((φ \land x \in ℝ) \land \|x\| < \frac{1}{L}) \to \|x\| \in ℝ$
303		simpr	$⊢ ((φ \land x \in ℝ) \land \|x\| < \frac{1}{L}) \to \|x\| < \frac{1}{L}$
304	302 303	ltned	$⊢ ((φ \land x \in ℝ) \land \|x\| < \frac{1}{L}) \to \|x\| \neq \frac{1}{L}$
305	232	biimpd	$⊢ ((φ \land x \in ℝ) \land \|x\| \neq \frac{1}{L}) \to (\|x\| < \frac{1}{L} \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
306	305	impancom	$⊢ ((φ \land x \in ℝ) \land \|x\| < \frac{1}{L}) \to (\|x\| \neq \frac{1}{L} \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
307	304 306	mpd	$⊢ ((φ \land x \in ℝ) \land \|x\| < \frac{1}{L}) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
308	307	ex	$⊢ (φ \land x \in ℝ) \to (\|x\| < \frac{1}{L} \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
309	301 308	sylbird	$⊢ (φ \land x \in ℝ) \to ((- \frac{1}{L} < x \land x < \frac{1}{L}) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
310	309	impr	$⊢ (φ \land (x \in ℝ \land (- \frac{1}{L} < x \land x < \frac{1}{L}))) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
311	310	expcom	$⊢ (x \in ℝ \land (- \frac{1}{L} < x \land x < \frac{1}{L})) \to (φ \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
312	311	3impb	$⊢ (x \in ℝ \land - \frac{1}{L} < x \land x < \frac{1}{L}) \to (φ \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
313	312	impcom	$⊢ (φ \land (x \in ℝ \land - \frac{1}{L} < x \land x < \frac{1}{L})) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
314	299 313	syldan	$⊢ (φ \land x \in (- \frac{1}{L}, \frac{1}{L})) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
315	314	ex	$⊢ φ \to (x \in (- \frac{1}{L}, \frac{1}{L}) \to x \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\})$
316	315	ssrdv	$⊢ φ \to (- \frac{1}{L}, \frac{1}{L}) \subseteq \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\}$
317		ssrexv	$⊢ (- \frac{1}{L}, \frac{1}{L}) \subseteq \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \to (\exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} x < k)$
318	316 317	syl	$⊢ φ \to (\exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} x < k)$
319	318	adantr	$⊢ (φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \to (\exists k \in (- \frac{1}{L}, \frac{1}{L}) x < k \to \exists k \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} x < k)$
320	296 319	mpd	$⊢ (φ \land (x \in ℝ^{*} \land x < \frac{1}{L})) \to \exists k \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} x < k$
321	11 44 249 320	eqsupd	$⊢ φ \to sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <) = \frac{1}{L}$
322	3 321	eqtrid	$⊢ φ \to R = \frac{1}{L}$

Metamath Proof Explorer

Theorem radcnvrat

Proof