cvgdvgrat

Description: Ratio test for convergence and divergence of a complex infinite series. If the ratio R of the absolute values of successive terms in an infinite sequence F converges to less than one, then the infinite sum of the terms of F converges to a complex number; and if R convergesgreater then the sum diverges. This combined form of cvgrat and dvgrat directly uses the limit of the ratio.

	Ref	Expression
Hypotheses	cvgdvgrat.z	$⊢ Z = ℤ_{\geq M}$
	cvgdvgrat.w	$⊢ W = ℤ_{\geq N}$
	cvgdvgrat.n	$⊢ φ \to N \in Z$
	cvgdvgrat.f	$⊢ φ \to F \in V$
	cvgdvgrat.c	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	cvgdvgrat.n0	$⊢ (φ \land k \in W) \to F (k) \neq 0$
	cvgdvgrat.r	$⊢ R = (k \in W ⟼ \|\frac{F (k + 1)}{F (k)}\|)$
	cvgdvgrat.cvg	$⊢ φ \to R ⇝ L$
	cvgdvgrat.n1	$⊢ φ \to L \neq 1$
Assertion	cvgdvgrat	$⊢ φ \to (L < 1 \leftrightarrow seq M (+ F) \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		cvgdvgrat.z	$⊢ Z = ℤ_{\geq M}$
2		cvgdvgrat.w	$⊢ W = ℤ_{\geq N}$
3		cvgdvgrat.n	$⊢ φ \to N \in Z$
4		cvgdvgrat.f	$⊢ φ \to F \in V$
5		cvgdvgrat.c	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
6		cvgdvgrat.n0	$⊢ (φ \land k \in W) \to F (k) \neq 0$
7		cvgdvgrat.r	$⊢ R = (k \in W ⟼ \|\frac{F (k + 1)}{F (k)}\|)$
8		cvgdvgrat.cvg	$⊢ φ \to R ⇝ L$
9		cvgdvgrat.n1	$⊢ φ \to L \neq 1$
10		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
11		elioore	$⊢ r \in (L, 1) \to r \in ℝ$
12	11	ad3antlr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \to r \in ℝ$
13	3 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
14		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
15	13 14	syl	$⊢ φ \to N \in ℤ$
16	7	a1i	$⊢ φ \to R = (k \in W ⟼ \|\frac{F (k + 1)}{F (k)}\|)$
17	2	peano2uzs	$⊢ k \in W \to k + 1 \in W$
18		ovex	$⊢ k + 1 \in V$
19		eleq1	$⊢ i = k + 1 \to (i \in W \leftrightarrow k + 1 \in W)$
20	19	anbi2d	$⊢ i = k + 1 \to ((φ \land i \in W) \leftrightarrow (φ \land k + 1 \in W))$
21		fveq2	$⊢ i = k + 1 \to F (i) = F (k + 1)$
22	21	eleq1d	$⊢ i = k + 1 \to (F (i) \in ℂ \leftrightarrow F (k + 1) \in ℂ)$
23	20 22	imbi12d	$⊢ i = k + 1 \to (((φ \land i \in W) \to F (i) \in ℂ) \leftrightarrow ((φ \land k + 1 \in W) \to F (k + 1) \in ℂ))$
24		eleq1	$⊢ k = i \to (k \in W \leftrightarrow i \in W)$
25	24	anbi2d	$⊢ k = i \to ((φ \land k \in W) \leftrightarrow (φ \land i \in W))$
26		fveq2	$⊢ k = i \to F (k) = F (i)$
27	26	eleq1d	$⊢ k = i \to (F (k) \in ℂ \leftrightarrow F (i) \in ℂ)$
28	25 27	imbi12d	$⊢ k = i \to (((φ \land k \in W) \to F (k) \in ℂ) \leftrightarrow ((φ \land i \in W) \to F (i) \in ℂ))$
29	2	eleq2i	$⊢ k \in W \leftrightarrow k \in ℤ_{\geq N}$
30	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
31	3 30	sylan	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in Z$
32	29 31	sylan2b	$⊢ (φ \land k \in W) \to k \in Z$
33	32 5	syldan	$⊢ (φ \land k \in W) \to F (k) \in ℂ$
34	28 33	chvarvv	$⊢ (φ \land i \in W) \to F (i) \in ℂ$
35	18 23 34	vtocl	$⊢ (φ \land k + 1 \in W) \to F (k + 1) \in ℂ$
36	17 35	sylan2	$⊢ (φ \land k \in W) \to F (k + 1) \in ℂ$
37	36 33 6	divcld	$⊢ (φ \land k \in W) \to \frac{F (k + 1)}{F (k)} \in ℂ$
38	37	abscld	$⊢ (φ \land k \in W) \to \|\frac{F (k + 1)}{F (k)}\| \in ℝ$
39	16 38	fvmpt2d	$⊢ (φ \land k \in W) \to R (k) = \|\frac{F (k + 1)}{F (k)}\|$
40	39 38	eqeltrd	$⊢ (φ \land k \in W) \to R (k) \in ℝ$
41	2 15 8 40	climrecl	$⊢ φ \to L \in ℝ$
42	41	rexrd	$⊢ φ \to L \in ℝ^{*}$
43		1xr	$⊢ 1 \in ℝ^{*}$
44		elioo2	$⊢ (L \in ℝ^{} \land 1 \in ℝ^{}) \to (r \in (L, 1) \leftrightarrow (r \in ℝ \land L < r \land r < 1))$
45	42 43 44	sylancl	$⊢ φ \to (r \in (L, 1) \leftrightarrow (r \in ℝ \land L < r \land r < 1))$
46	45	biimpa	$⊢ (φ \land r \in (L, 1)) \to (r \in ℝ \land L < r \land r < 1)$
47	46	simp3d	$⊢ (φ \land r \in (L, 1)) \to r < 1$
48	47	ad2antrr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \to r < 1$
49		simplr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \to n \in W$
50	34	ex	$⊢ φ \to (i \in W \to F (i) \in ℂ)$
51	50	ad3antrrr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \to (i \in W \to F (i) \in ℂ)$
52	51	imp	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \land i \in W) \to F (i) \in ℂ$
53		fvoveq1	$⊢ k = i \to F (k + 1) = F (i + 1)$
54	53	fveq2d	$⊢ k = i \to \|F (k + 1)\| = \|F (i + 1)\|$
55	26	fveq2d	$⊢ k = i \to \|F (k)\| = \|F (i)\|$
56	55	oveq2d	$⊢ k = i \to r \|F (k)\| = r \|F (i)\|$
57	54 56	breq12d	$⊢ k = i \to (\|F (k + 1)\| \leq r \|F (k)\| \leftrightarrow \|F (i + 1)\| \leq r \|F (i)\|)$
58	57	rspccva	$⊢ (\forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\| \land i \in ℤ_{\geq n}) \to \|F (i + 1)\| \leq r \|F (i)\|$
59	58	adantll	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \land i \in ℤ_{\geq n}) \to \|F (i + 1)\| \leq r \|F (i)\|$
60	2 10 12 48 49 52 59	cvgrat	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|) \to seq N (+ F) \in dom ⇝$
61	15	adantr	$⊢ (φ \land r \in (L, 1)) \to N \in ℤ$
62	46	simp2d	$⊢ (φ \land r \in (L, 1)) \to L < r$
63		difrp	$⊢ (L \in ℝ \land r \in ℝ) \to (L < r \leftrightarrow r - L \in ℝ^{+})$
64	41 11 63	syl2an	$⊢ (φ \land r \in (L, 1)) \to (L < r \leftrightarrow r - L \in ℝ^{+})$
65	62 64	mpbid	$⊢ (φ \land r \in (L, 1)) \to r - L \in ℝ^{+}$
66	39	adantlr	$⊢ ((φ \land r \in (L, 1)) \land k \in W) \to R (k) = \|\frac{F (k + 1)}{F (k)}\|$
67	8	adantr	$⊢ (φ \land r \in (L, 1)) \to R ⇝ L$
68	2 61 65 66 67	climi2	$⊢ (φ \land r \in (L, 1)) \to \exists n \in W \forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L$
69	2	uztrn2	$⊢ (n \in W \land k \in ℤ_{\geq n}) \to k \in W$
70	69 36	sylan2	$⊢ (φ \land (n \in W \land k \in ℤ_{\geq n})) \to F (k + 1) \in ℂ$
71	70	anassrs	$⊢ ((φ \land n \in W) \land k \in ℤ_{\geq n}) \to F (k + 1) \in ℂ$
72	71	adantllr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k + 1) \in ℂ$
73	72	adantr	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to F (k + 1) \in ℂ$
74	73	abscld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k + 1)\| \in ℝ$
75	11	ad4antlr	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to r \in ℝ$
76	69 33	sylan2	$⊢ (φ \land (n \in W \land k \in ℤ_{\geq n})) \to F (k) \in ℂ$
77	76	anassrs	$⊢ ((φ \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \in ℂ$
78	77	adantllr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \in ℂ$
79	78	adantr	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to F (k) \in ℂ$
80	79	abscld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k)\| \in ℝ$
81	75 80	remulcld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to r \|F (k)\| \in ℝ$
82	69 6	sylan2	$⊢ (φ \land (n \in W \land k \in ℤ_{\geq n})) \to F (k) \neq 0$
83	82	anassrs	$⊢ ((φ \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \neq 0$
84	83	adantllr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \neq 0$
85	84	adantr	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to F (k) \neq 0$
86	73 79 85	absdivd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|\frac{F (k + 1)}{F (k)}\| = \frac{\|F (k + 1)\|}{\|F (k)\|}$
87	72 78 84	divcld	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to \frac{F (k + 1)}{F (k)} \in ℂ$
88	87	abscld	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to \|\frac{F (k + 1)}{F (k)}\| \in ℝ$
89	41	ad3antrrr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to L \in ℝ$
90	88 89	resubcld	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to \|\frac{F (k + 1)}{F (k)}\| - L \in ℝ$
91	11	ad3antlr	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to r \in ℝ$
92	91 89	resubcld	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to r - L \in ℝ$
93	90 92	absltd	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to (\|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L \leftrightarrow (- (r - L) < \|\frac{F (k + 1)}{F (k)}\| - L \land \|\frac{F (k + 1)}{F (k)}\| - L < r - L))$
94	93	simplbda	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|\frac{F (k + 1)}{F (k)}\| - L < r - L$
95	73 79 85	divcld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \frac{F (k + 1)}{F (k)} \in ℂ$
96	95	abscld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|\frac{F (k + 1)}{F (k)}\| \in ℝ$
97	41	ad4antr	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to L \in ℝ$
98	96 75 97	ltsub1d	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to (\|\frac{F (k + 1)}{F (k)}\| < r \leftrightarrow \|\frac{F (k + 1)}{F (k)}\| - L < r - L)$
99	94 98	mpbird	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|\frac{F (k + 1)}{F (k)}\| < r$
100	86 99	eqbrtrrd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \frac{\|F (k + 1)\|}{\|F (k)\|} < r$
101	79 85	absrpcld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k)\| \in ℝ^{+}$
102	74 75 101	ltdivmuld	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to (\frac{\|F (k + 1)\|}{\|F (k)\|} < r \leftrightarrow \|F (k + 1)\| < \|F (k)\| r)$
103	100 102	mpbid	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k + 1)\| < \|F (k)\| r$
104	101	rpcnd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k)\| \in ℂ$
105	75	recnd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to r \in ℂ$
106	104 105	mulcomd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k)\| r = r \|F (k)\|$
107	103 106	breqtrd	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k + 1)\| < r \|F (k)\|$
108	74 81 107	ltled	$⊢ ((((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L) \to \|F (k + 1)\| \leq r \|F (k)\|$
109	108	ex	$⊢ (((φ \land r \in (L, 1)) \land n \in W) \land k \in ℤ_{\geq n}) \to (\|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L \to \|F (k + 1)\| \leq r \|F (k)\|)$
110	109	ralimdva	$⊢ ((φ \land r \in (L, 1)) \land n \in W) \to (\forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L \to \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|)$
111	110	reximdva	$⊢ (φ \land r \in (L, 1)) \to (\exists n \in W \forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < r - L \to \exists n \in W \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|)$
112	68 111	mpd	$⊢ (φ \land r \in (L, 1)) \to \exists n \in W \forall k \in ℤ_{\geq n} \|F (k + 1)\| \leq r \|F (k)\|$
113	60 112	r19.29a	$⊢ (φ \land r \in (L, 1)) \to seq N (+ F) \in dom ⇝$
114	113	ralrimiva	$⊢ φ \to \forall r \in (L, 1) seq N (+ F) \in dom ⇝$
115	114	adantr	$⊢ (φ \land L < 1) \to \forall r \in (L, 1) seq N (+ F) \in dom ⇝$
116		ioon0	$⊢ (L \in ℝ^{} \land 1 \in ℝ^{}) \to ((L, 1) \neq \emptyset \leftrightarrow L < 1)$
117	42 43 116	sylancl	$⊢ φ \to ((L, 1) \neq \emptyset \leftrightarrow L < 1)$
118	117	biimpar	$⊢ (φ \land L < 1) \to (L, 1) \neq \emptyset$
119		r19.3rzv	$⊢ (L, 1) \neq \emptyset \to (seq N (+ F) \in dom ⇝ \leftrightarrow \forall r \in (L, 1) seq N (+ F) \in dom ⇝)$
120	118 119	syl	$⊢ (φ \land L < 1) \to (seq N (+ F) \in dom ⇝ \leftrightarrow \forall r \in (L, 1) seq N (+ F) \in dom ⇝)$
121	115 120	mpbird	$⊢ (φ \land L < 1) \to seq N (+ F) \in dom ⇝$
122	1 3 5	iserex	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
123	122	adantr	$⊢ (φ \land L < 1) \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
124	121 123	mpbird	$⊢ (φ \land L < 1) \to seq M (+ F) \in dom ⇝$
125	124	ex	$⊢ φ \to (L < 1 \to seq M (+ F) \in dom ⇝)$
126		1red	$⊢ φ \to 1 \in ℝ$
127	41 126	lttri2d	$⊢ φ \to (L \neq 1 \leftrightarrow (L < 1 \lor 1 < L))$
128	9 127	mpbid	$⊢ φ \to (L < 1 \lor 1 < L)$
129	128	orcanai	$⊢ (φ \land \neg L < 1) \to 1 < L$
130		simplr	$⊢ (((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \to n \in W$
131	4	ad3antrrr	$⊢ (((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \to F \in V$
132	50	ad3antrrr	$⊢ (((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \to (i \in W \to F (i) \in ℂ)$
133	132	imp	$⊢ ((((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \land i \in W) \to F (i) \in ℂ$
134	2	uztrn2	$⊢ (n \in W \land i \in ℤ_{\geq n}) \to i \in W$
135	26	neeq1d	$⊢ k = i \to (F (k) \neq 0 \leftrightarrow F (i) \neq 0)$
136	25 135	imbi12d	$⊢ k = i \to (((φ \land k \in W) \to F (k) \neq 0) \leftrightarrow ((φ \land i \in W) \to F (i) \neq 0))$
137	136 6	chvarvv	$⊢ (φ \land i \in W) \to F (i) \neq 0$
138	134 137	sylan2	$⊢ (φ \land (n \in W \land i \in ℤ_{\geq n})) \to F (i) \neq 0$
139	138	anassrs	$⊢ ((φ \land n \in W) \land i \in ℤ_{\geq n}) \to F (i) \neq 0$
140	139	adantllr	$⊢ (((φ \land 1 < L) \land n \in W) \land i \in ℤ_{\geq n}) \to F (i) \neq 0$
141	140	adantlr	$⊢ ((((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \land i \in ℤ_{\geq n}) \to F (i) \neq 0$
142	55 54	breq12d	$⊢ k = i \to (\|F (k)\| \leq \|F (k + 1)\| \leftrightarrow \|F (i)\| \leq \|F (i + 1)\|)$
143	142	rspccva	$⊢ (\forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\| \land i \in ℤ_{\geq n}) \to \|F (i)\| \leq \|F (i + 1)\|$
144	143	adantll	$⊢ ((((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \land i \in ℤ_{\geq n}) \to \|F (i)\| \leq \|F (i + 1)\|$
145	2 10 130 131 133 141 144	dvgrat	$⊢ (((φ \land 1 < L) \land n \in W) \land \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|) \to seq N (+ F) \notin dom ⇝$
146	15	adantr	$⊢ (φ \land 1 < L) \to N \in ℤ$
147		1re	$⊢ 1 \in ℝ$
148		difrp	$⊢ (1 \in ℝ \land L \in ℝ) \to (1 < L \leftrightarrow L - 1 \in ℝ^{+})$
149	147 41 148	sylancr	$⊢ φ \to (1 < L \leftrightarrow L - 1 \in ℝ^{+})$
150	149	biimpa	$⊢ (φ \land 1 < L) \to L - 1 \in ℝ^{+}$
151	39	adantlr	$⊢ ((φ \land 1 < L) \land k \in W) \to R (k) = \|\frac{F (k + 1)}{F (k)}\|$
152	8	adantr	$⊢ (φ \land 1 < L) \to R ⇝ L$
153	2 146 150 151 152	climi2	$⊢ (φ \land 1 < L) \to \exists n \in W \forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1$
154	77	adantllr	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \in ℂ$
155	154	adantr	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to F (k) \in ℂ$
156	155	abscld	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k)\| \in ℝ$
157	71	adantllr	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k + 1) \in ℂ$
158	157	adantr	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to F (k + 1) \in ℂ$
159	158	abscld	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k + 1)\| \in ℝ$
160	83	adantllr	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to F (k) \neq 0$
161	160	adantr	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to F (k) \neq 0$
162	155 161	absrpcld	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k)\| \in ℝ^{+}$
163	162	rpcnd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k)\| \in ℂ$
164	163	mullidd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 \|F (k)\| = \|F (k)\|$
165	41	ad4antr	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to L \in ℝ$
166	165	recnd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to L \in ℂ$
167		1cnd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 \in ℂ$
168	166 167	negsubdi2d	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to - (L - 1) = 1 - L$
169	157 154 160	divcld	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to \frac{F (k + 1)}{F (k)} \in ℂ$
170	169	abscld	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to \|\frac{F (k + 1)}{F (k)}\| \in ℝ$
171	41	ad3antrrr	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to L \in ℝ$
172	170 171	resubcld	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to \|\frac{F (k + 1)}{F (k)}\| - L \in ℝ$
173		1red	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to 1 \in ℝ$
174	171 173	resubcld	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to L - 1 \in ℝ$
175	172 174	absltd	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to (\|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1 \leftrightarrow (- (L - 1) < \|\frac{F (k + 1)}{F (k)}\| - L \land \|\frac{F (k + 1)}{F (k)}\| - L < L - 1))$
176	175	simprbda	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to - (L - 1) < \|\frac{F (k + 1)}{F (k)}\| - L$
177	168 176	eqbrtrrd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 - L < \|\frac{F (k + 1)}{F (k)}\| - L$
178		1red	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 \in ℝ$
179	158 155 161	divcld	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \frac{F (k + 1)}{F (k)} \in ℂ$
180	179	abscld	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|\frac{F (k + 1)}{F (k)}\| \in ℝ$
181	178 180 165	ltsub1d	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to (1 < \|\frac{F (k + 1)}{F (k)}\| \leftrightarrow 1 - L < \|\frac{F (k + 1)}{F (k)}\| - L)$
182	177 181	mpbird	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 < \|\frac{F (k + 1)}{F (k)}\|$
183	158 155 161	absdivd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|\frac{F (k + 1)}{F (k)}\| = \frac{\|F (k + 1)\|}{\|F (k)\|}$
184	182 183	breqtrd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 < \frac{\|F (k + 1)\|}{\|F (k)\|}$
185	178 159 162	ltmuldivd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to (1 \|F (k)\| < \|F (k + 1)\| \leftrightarrow 1 < \frac{\|F (k + 1)\|}{\|F (k)\|})$
186	184 185	mpbird	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to 1 \|F (k)\| < \|F (k + 1)\|$
187	164 186	eqbrtrrd	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k)\| < \|F (k + 1)\|$
188	156 159 187	ltled	$⊢ ((((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \land \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1) \to \|F (k)\| \leq \|F (k + 1)\|$
189	188	ex	$⊢ (((φ \land 1 < L) \land n \in W) \land k \in ℤ_{\geq n}) \to (\|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1 \to \|F (k)\| \leq \|F (k + 1)\|)$
190	189	ralimdva	$⊢ ((φ \land 1 < L) \land n \in W) \to (\forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1 \to \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|)$
191	190	reximdva	$⊢ (φ \land 1 < L) \to (\exists n \in W \forall k \in ℤ_{\geq n} \|\|\frac{F (k + 1)}{F (k)}\| - L\| < L - 1 \to \exists n \in W \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|)$
192	153 191	mpd	$⊢ (φ \land 1 < L) \to \exists n \in W \forall k \in ℤ_{\geq n} \|F (k)\| \leq \|F (k + 1)\|$
193	145 192	r19.29a	$⊢ (φ \land 1 < L) \to seq N (+ F) \notin dom ⇝$
194		df-nel	$⊢ seq N (+ F) \notin dom ⇝ \leftrightarrow \neg seq N (+ F) \in dom ⇝$
195	193 194	sylib	$⊢ (φ \land 1 < L) \to \neg seq N (+ F) \in dom ⇝$
196	122	adantr	$⊢ (φ \land 1 < L) \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
197	195 196	mtbird	$⊢ (φ \land 1 < L) \to \neg seq M (+ F) \in dom ⇝$
198	129 197	syldan	$⊢ (φ \land \neg L < 1) \to \neg seq M (+ F) \in dom ⇝$
199	198	ex	$⊢ φ \to (\neg L < 1 \to \neg seq M (+ F) \in dom ⇝)$
200	125 199	impcon4bid	$⊢ φ \to (L < 1 \leftrightarrow seq M (+ F) \in dom ⇝)$

Metamath Proof Explorer

Theorem cvgdvgrat

Proof