geomcau

Description: If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	lmclim2.2	$⊢ φ \to D \in Met (X)$
	lmclim2.3	$⊢ φ \to F : ℕ ⟶ X$
	geomcau.4	$⊢ φ \to A \in ℝ$
	geomcau.5	$⊢ φ \to B \in ℝ^{+}$
	geomcau.6	$⊢ φ \to B < 1$
	geomcau.7	$⊢ (φ \land k \in ℕ) \to F (k) D F (k + 1) \leq A B^{k}$
Assertion	geomcau	$⊢ φ \to F \in Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		lmclim2.2	$⊢ φ \to D \in Met (X)$
2		lmclim2.3	$⊢ φ \to F : ℕ ⟶ X$
3		geomcau.4	$⊢ φ \to A \in ℝ$
4		geomcau.5	$⊢ φ \to B \in ℝ^{+}$
5		geomcau.6	$⊢ φ \to B < 1$
6		geomcau.7	$⊢ (φ \land k \in ℕ) \to F (k) D F (k + 1) \leq A B^{k}$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8		1zzd	$⊢ φ \to 1 \in ℤ$
9	4	rpcnd	$⊢ φ \to B \in ℂ$
10	4	rpred	$⊢ φ \to B \in ℝ$
11	4	rpge0d	$⊢ φ \to 0 \leq B$
12	10 11	absidd	$⊢ φ \to \|B\| = B$
13	12 5	eqbrtrd	$⊢ φ \to \|B\| < 1$
14	9 13	expcnv	$⊢ φ \to (m \in ℕ_{0} ⟼ B^{m}) ⇝ 0$
15		1re	$⊢ 1 \in ℝ$
16		resubcl	$⊢ (1 \in ℝ \land B \in ℝ) \to 1 - B \in ℝ$
17	15 10 16	sylancr	$⊢ φ \to 1 - B \in ℝ$
18		posdif	$⊢ (B \in ℝ \land 1 \in ℝ) \to (B < 1 \leftrightarrow 0 < 1 - B)$
19	10 15 18	sylancl	$⊢ φ \to (B < 1 \leftrightarrow 0 < 1 - B)$
20	5 19	mpbid	$⊢ φ \to 0 < 1 - B$
21	17 20	elrpd	$⊢ φ \to 1 - B \in ℝ^{+}$
22	3 21	rerpdivcld	$⊢ φ \to \frac{A}{1 - B} \in ℝ$
23	22	recnd	$⊢ φ \to \frac{A}{1 - B} \in ℂ$
24		nnex	$⊢ ℕ \in V$
25	24	mptex	$⊢ (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) \in V$
26	25	a1i	$⊢ φ \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) \in V$
27		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
28	27	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
29		oveq2	$⊢ m = n \to B^{m} = B^{n}$
30		eqid	$⊢ (m \in ℕ_{0} ⟼ B^{m}) = (m \in ℕ_{0} ⟼ B^{m})$
31		ovex	$⊢ B^{n} \in V$
32	29 30 31	fvmpt	$⊢ n \in ℕ_{0} \to (m \in ℕ_{0} ⟼ B^{m}) (n) = B^{n}$
33	28 32	syl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ_{0} ⟼ B^{m}) (n) = B^{n}$
34		nnz	$⊢ n \in ℕ \to n \in ℤ$
35		rpexpcl	$⊢ (B \in ℝ^{+} \land n \in ℤ) \to B^{n} \in ℝ^{+}$
36	4 34 35	syl2an	$⊢ (φ \land n \in ℕ) \to B^{n} \in ℝ^{+}$
37	36	rpcnd	$⊢ (φ \land n \in ℕ) \to B^{n} \in ℂ$
38	33 37	eqeltrd	$⊢ (φ \land n \in ℕ) \to (m \in ℕ_{0} ⟼ B^{m}) (n) \in ℂ$
39	23	adantr	$⊢ (φ \land n \in ℕ) \to \frac{A}{1 - B} \in ℂ$
40	37 39	mulcomd	$⊢ (φ \land n \in ℕ) \to B^{n} (\frac{A}{1 - B}) = (\frac{A}{1 - B}) B^{n}$
41	29	oveq1d	$⊢ m = n \to B^{m} (\frac{A}{1 - B}) = B^{n} (\frac{A}{1 - B})$
42		eqid	$⊢ (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) = (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B}))$
43		ovex	$⊢ B^{n} (\frac{A}{1 - B}) \in V$
44	41 42 43	fvmpt	$⊢ n \in ℕ \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) (n) = B^{n} (\frac{A}{1 - B})$
45	44	adantl	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) (n) = B^{n} (\frac{A}{1 - B})$
46	33	oveq2d	$⊢ (φ \land n \in ℕ) \to (\frac{A}{1 - B}) (m \in ℕ_{0} ⟼ B^{m}) (n) = (\frac{A}{1 - B}) B^{n}$
47	40 45 46	3eqtr4d	$⊢ (φ \land n \in ℕ) \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) (n) = (\frac{A}{1 - B}) (m \in ℕ_{0} ⟼ B^{m}) (n)$
48	7 8 14 23 26 38 47	climmulc2	$⊢ φ \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) ⇝ (\frac{A}{1 - B}) \cdot 0$
49	23	mul01d	$⊢ φ \to (\frac{A}{1 - B}) \cdot 0 = 0$
50	48 49	breqtrd	$⊢ φ \to (m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) ⇝ 0$
51	36	rpred	$⊢ (φ \land n \in ℕ) \to B^{n} \in ℝ$
52	22	adantr	$⊢ (φ \land n \in ℕ) \to \frac{A}{1 - B} \in ℝ$
53	51 52	remulcld	$⊢ (φ \land n \in ℕ) \to B^{n} (\frac{A}{1 - B}) \in ℝ$
54	53	recnd	$⊢ (φ \land n \in ℕ) \to B^{n} (\frac{A}{1 - B}) \in ℂ$
55	7 8 26 45 54	clim0c	$⊢ φ \to ((m \in ℕ ⟼ B^{m} (\frac{A}{1 - B})) ⇝ 0 \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x)$
56	50 55	mpbid	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x$
57		nnz	$⊢ j \in ℕ \to j \in ℤ$
58	57	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to j \in ℤ$
59		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
60		oveq2	$⊢ n = j \to B^{n} = B^{j}$
61	60	fvoveq1d	$⊢ n = j \to \|B^{n} (\frac{A}{1 - B})\| = \|B^{j} (\frac{A}{1 - B})\|$
62	61	breq1d	$⊢ n = j \to (\|B^{n} (\frac{A}{1 - B})\| < x \leftrightarrow \|B^{j} (\frac{A}{1 - B})\| < x)$
63	62	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x \to \|B^{j} (\frac{A}{1 - B})\| < x)$
64	58 59 63	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x \to \|B^{j} (\frac{A}{1 - B})\| < x)$
65	1	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to D \in Met (X)$
66		simpl	$⊢ (j \in ℕ \land n \in ℤ_{\geq j}) \to j \in ℕ$
67		ffvelcdm	$⊢ (F : ℕ ⟶ X \land j \in ℕ) \to F (j) \in X$
68	2 66 67	syl2an	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) \in X$
69		eluznn	$⊢ (j \in ℕ \land n \in ℤ_{\geq j}) \to n \in ℕ$
70		ffvelcdm	$⊢ (F : ℕ ⟶ X \land n \in ℕ) \to F (n) \in X$
71	2 69 70	syl2an	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (n) \in X$
72		metcl	$⊢ (D \in Met (X) \land F (j) \in X \land F (n) \in X) \to F (j) D F (n) \in ℝ$
73	65 68 71 72	syl3anc	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \in ℝ$
74		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
75		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
76	75	ad2antrl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to j \in ℕ_{0}$
77	76	nn0zd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to j \in ℤ$
78		oveq2	$⊢ m = k \to B^{m} = B^{k}$
79	78	oveq2d	$⊢ m = k \to A B^{m} = A B^{k}$
80		eqid	$⊢ (m \in ℤ_{\geq j} ⟼ A B^{m}) = (m \in ℤ_{\geq j} ⟼ A B^{m})$
81		ovex	$⊢ A B^{k} \in V$
82	79 80 81	fvmpt	$⊢ k \in ℤ_{\geq j} \to (m \in ℤ_{\geq j} ⟼ A B^{m}) (k) = A B^{k}$
83	82	adantl	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq j} ⟼ A B^{m}) (k) = A B^{k}$
84	3	ad2antrr	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to A \in ℝ$
85	10	ad2antrr	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to B \in ℝ$
86		eluznn0	$⊢ (j \in ℕ_{0} \land k \in ℤ_{\geq j}) \to k \in ℕ_{0}$
87	76 86	sylan	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to k \in ℕ_{0}$
88	85 87	reexpcld	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to B^{k} \in ℝ$
89	84 88	remulcld	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to A B^{k} \in ℝ$
90	89	recnd	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to A B^{k} \in ℂ$
91	3	recnd	$⊢ φ \to A \in ℂ$
92	91	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to A \in ℂ$
93	9	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B \in ℂ$
94	13	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \|B\| < 1$
95		eqid	$⊢ (m \in ℤ_{\geq j} ⟼ B^{m}) = (m \in ℤ_{\geq j} ⟼ B^{m})$
96		ovex	$⊢ B^{k} \in V$
97	78 95 96	fvmpt	$⊢ k \in ℤ_{\geq j} \to (m \in ℤ_{\geq j} ⟼ B^{m}) (k) = B^{k}$
98	97	adantl	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq j} ⟼ B^{m}) (k) = B^{k}$
99	93 94 76 98	geolim2	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to seq j (+ (m \in ℤ_{\geq j} ⟼ B^{m})) ⇝ (\frac{B^{j}}{1 - B})$
100	88	recnd	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to B^{k} \in ℂ$
101	98 100	eqeltrd	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq j} ⟼ B^{m}) (k) \in ℂ$
102	98	oveq2d	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to A (m \in ℤ_{\geq j} ⟼ B^{m}) (k) = A B^{k}$
103	83 102	eqtr4d	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to (m \in ℤ_{\geq j} ⟼ A B^{m}) (k) = A (m \in ℤ_{\geq j} ⟼ B^{m}) (k)$
104	74 77 92 99 101 103	isermulc2	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) ⇝ A (\frac{B^{j}}{1 - B})$
105	4	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B \in ℝ^{+}$
106	105 77	rpexpcld	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B^{j} \in ℝ^{+}$
107	106	rpcnd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B^{j} \in ℂ$
108	17	recnd	$⊢ φ \to 1 - B \in ℂ$
109	108	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to 1 - B \in ℂ$
110	21	rpne0d	$⊢ φ \to 1 - B \neq 0$
111	110	adantr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to 1 - B \neq 0$
112	92 107 109 111	div12d	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to A (\frac{B^{j}}{1 - B}) = B^{j} (\frac{A}{1 - B})$
113	104 112	breqtrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) ⇝ B^{j} (\frac{A}{1 - B})$
114	74 77 83 90 113	isumclim	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k \in ℤ_{\geq j}} A B^{k} = B^{j} (\frac{A}{1 - B})$
115		seqex	$⊢ seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) \in V$
116		ovex	$⊢ A (\frac{B^{j}}{1 - B}) \in V$
117	115 116	breldm	$⊢ seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) ⇝ A (\frac{B^{j}}{1 - B}) \to seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) \in dom ⇝$
118	104 117	syl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to seq j (+ (m \in ℤ_{\geq j} ⟼ A B^{m})) \in dom ⇝$
119	74 77 83 89 118	isumrecl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k \in ℤ_{\geq j}} A B^{k} \in ℝ$
120	114 119	eqeltrrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B^{j} (\frac{A}{1 - B}) \in ℝ$
121	120	recnd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B^{j} (\frac{A}{1 - B}) \in ℂ$
122	121	abscld	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \|B^{j} (\frac{A}{1 - B})\| \in ℝ$
123		fzfid	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to (j \dots n - 1) \in Fin$
124		simpll	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n - 1)) \to φ$
125		elfzuz	$⊢ k \in (j \dots n - 1) \to k \in ℤ_{\geq j}$
126		simprl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to j \in ℕ$
127		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
128	126 127	sylan	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to k \in ℕ$
129	125 128	sylan2	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n - 1)) \to k \in ℕ$
130	1	adantr	$⊢ (φ \land k \in ℕ) \to D \in Met (X)$
131	2	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to F (k) \in X$
132		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
133		ffvelcdm	$⊢ (F : ℕ ⟶ X \land k + 1 \in ℕ) \to F (k + 1) \in X$
134	2 132 133	syl2an	$⊢ (φ \land k \in ℕ) \to F (k + 1) \in X$
135		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land F (k + 1) \in X) \to F (k) D F (k + 1) \in ℝ$
136	130 131 134 135	syl3anc	$⊢ (φ \land k \in ℕ) \to F (k) D F (k + 1) \in ℝ$
137	124 129 136	syl2anc	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n - 1)) \to F (k) D F (k + 1) \in ℝ$
138	123 137	fsumrecl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k = j}^{n - 1} (F (k) D F (k + 1)) \in ℝ$
139		simprr	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to n \in ℤ_{\geq j}$
140		elfzuz	$⊢ k \in (j \dots n) \to k \in ℤ_{\geq j}$
141		simpll	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to φ$
142	141 128 131	syl2anc	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to F (k) \in X$
143	140 142	sylan2	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n)) \to F (k) \in X$
144	65 139 143	mettrifi	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \leq \sum_{k = j}^{n - 1} (F (k) D F (k + 1))$
145	125 89	sylan2	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n - 1)) \to A B^{k} \in ℝ$
146	123 145	fsumrecl	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k = j}^{n - 1} A B^{k} \in ℝ$
147	124 129 6	syl2anc	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in (j \dots n - 1)) \to F (k) D F (k + 1) \leq A B^{k}$
148	123 137 145 147	fsumle	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k = j}^{n - 1} (F (k) D F (k + 1)) \leq \sum_{k = j}^{n - 1} A B^{k}$
149		fzssuz	$⊢ (j \dots n - 1) \subseteq ℤ_{\geq j}$
150	149	a1i	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to (j \dots n - 1) \subseteq ℤ_{\geq j}$
151		0red	$⊢ (φ \land k \in ℕ) \to 0 \in ℝ$
152		nnz	$⊢ k \in ℕ \to k \in ℤ$
153		rpexpcl	$⊢ (B \in ℝ^{+} \land k \in ℤ) \to B^{k} \in ℝ^{+}$
154	4 152 153	syl2an	$⊢ (φ \land k \in ℕ) \to B^{k} \in ℝ^{+}$
155	136 154	rerpdivcld	$⊢ (φ \land k \in ℕ) \to \frac{F (k) D F (k + 1)}{B^{k}} \in ℝ$
156	3	adantr	$⊢ (φ \land k \in ℕ) \to A \in ℝ$
157		metge0	$⊢ (D \in Met (X) \land F (k) \in X \land F (k + 1) \in X) \to 0 \leq F (k) D F (k + 1)$
158	130 131 134 157	syl3anc	$⊢ (φ \land k \in ℕ) \to 0 \leq F (k) D F (k + 1)$
159	136 154 158	divge0d	$⊢ (φ \land k \in ℕ) \to 0 \leq \frac{F (k) D F (k + 1)}{B^{k}}$
160	136 156 154	ledivmul2d	$⊢ (φ \land k \in ℕ) \to (\frac{F (k) D F (k + 1)}{B^{k}} \leq A \leftrightarrow F (k) D F (k + 1) \leq A B^{k})$
161	6 160	mpbird	$⊢ (φ \land k \in ℕ) \to \frac{F (k) D F (k + 1)}{B^{k}} \leq A$
162	151 155 156 159 161	letrd	$⊢ (φ \land k \in ℕ) \to 0 \leq A$
163	141 128 162	syl2anc	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to 0 \leq A$
164	141 128 154	syl2anc	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to B^{k} \in ℝ^{+}$
165	164	rpge0d	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to 0 \leq B^{k}$
166	84 88 163 165	mulge0d	$⊢ ((φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \land k \in ℤ_{\geq j}) \to 0 \leq A B^{k}$
167	74 77 123 150 83 89 166 118	isumless	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k = j}^{n - 1} A B^{k} \leq \sum_{k \in ℤ_{\geq j}} A B^{k}$
168	138 146 119 148 167	letrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \sum_{k = j}^{n - 1} (F (k) D F (k + 1)) \leq \sum_{k \in ℤ_{\geq j}} A B^{k}$
169	73 138 119 144 168	letrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \leq \sum_{k \in ℤ_{\geq j}} A B^{k}$
170	169 114	breqtrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \leq B^{j} (\frac{A}{1 - B})$
171	120	leabsd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to B^{j} (\frac{A}{1 - B}) \leq \|B^{j} (\frac{A}{1 - B})\|$
172	73 120 122 170 171	letrd	$⊢ (φ \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \leq \|B^{j} (\frac{A}{1 - B})\|$
173	172	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \leq \|B^{j} (\frac{A}{1 - B})\|$
174	73	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to F (j) D F (n) \in ℝ$
175	122	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to \|B^{j} (\frac{A}{1 - B})\| \in ℝ$
176		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
177	176	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to x \in ℝ$
178		lelttr	$⊢ (F (j) D F (n) \in ℝ \land \|B^{j} (\frac{A}{1 - B})\| \in ℝ \land x \in ℝ) \to ((F (j) D F (n) \leq \|B^{j} (\frac{A}{1 - B})\| \land \|B^{j} (\frac{A}{1 - B})\| < x) \to F (j) D F (n) < x)$
179	174 175 177 178	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to ((F (j) D F (n) \leq \|B^{j} (\frac{A}{1 - B})\| \land \|B^{j} (\frac{A}{1 - B})\| < x) \to F (j) D F (n) < x)$
180	173 179	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in ℕ \land n \in ℤ_{\geq j})) \to (\|B^{j} (\frac{A}{1 - B})\| < x \to F (j) D F (n) < x)$
181	180	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℕ) \land n \in ℤ_{\geq j}) \to (\|B^{j} (\frac{A}{1 - B})\| < x \to F (j) D F (n) < x)$
182	181	ralrimdva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\|B^{j} (\frac{A}{1 - B})\| < x \to \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
183	64 182	syld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x \to \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
184	183	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in ℕ \forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x \to \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
185	184	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} \|B^{n} (\frac{A}{1 - B})\| < x \to \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
186	56 185	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x$
187		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
188	1 187	syl	$⊢ φ \to D \in ∞Met (X)$
189		eqidd	$⊢ (φ \land n \in ℕ) \to F (n) = F (n)$
190		eqidd	$⊢ (φ \land j \in ℕ) \to F (j) = F (j)$
191	7 188 8 189 190 2	iscauf	$⊢ φ \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
192	186 191	mpbird	$⊢ φ \to F \in Cau (D)$

Metamath Proof Explorer

Theorem geomcau

Proof