stoweidlem7

Description: This lemma is used to prove that q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91, (at the top of page 91), is such that q_n < ε on T \ U , and q_n > 1 - ε on V . Here it is proven that, for n large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable A is used to represent (k*δ) in the paper, and B is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem7.1	$⊢ F = (i \in ℕ_{0} ⟼ {(\frac{1}{A})}^{i})$
	stoweidlem7.2	$⊢ G = (i \in ℕ_{0} ⟼ B^{i})$
	stoweidlem7.3	$⊢ φ \to A \in ℝ$
	stoweidlem7.4	$⊢ φ \to 1 < A$
	stoweidlem7.5	$⊢ φ \to B \in ℝ^{+}$
	stoweidlem7.6	$⊢ φ \to B < 1$
	stoweidlem7.7	$⊢ φ \to E \in ℝ^{+}$
Assertion	stoweidlem7	$⊢ φ \to \exists n \in ℕ (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem7.1	$⊢ F = (i \in ℕ_{0} ⟼ {(\frac{1}{A})}^{i})$
2		stoweidlem7.2	$⊢ G = (i \in ℕ_{0} ⟼ B^{i})$
3		stoweidlem7.3	$⊢ φ \to A \in ℝ$
4		stoweidlem7.4	$⊢ φ \to 1 < A$
5		stoweidlem7.5	$⊢ φ \to B \in ℝ^{+}$
6		stoweidlem7.6	$⊢ φ \to B < 1$
7		stoweidlem7.7	$⊢ φ \to E \in ℝ^{+}$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10		oveq2	$⊢ i = k \to B^{i} = B^{k}$
11		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
12	11	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℕ_{0}$
13	5	rpcnd	$⊢ φ \to B \in ℂ$
14	13	adantr	$⊢ (φ \land k \in ℕ) \to B \in ℂ$
15	14 12	expcld	$⊢ (φ \land k \in ℕ) \to B^{k} \in ℂ$
16	2 10 12 15	fvmptd3	$⊢ (φ \land k \in ℕ) \to G (k) = B^{k}$
17		1red	$⊢ φ \to 1 \in ℝ$
18	17	renegcld	$⊢ φ \to - 1 \in ℝ$
19		0red	$⊢ φ \to 0 \in ℝ$
20	5	rpred	$⊢ φ \to B \in ℝ$
21		neg1lt0	$⊢ - 1 < 0$
22	21	a1i	$⊢ φ \to - 1 < 0$
23	5	rpgt0d	$⊢ φ \to 0 < B$
24	18 19 20 22 23	lttrd	$⊢ φ \to - 1 < B$
25	20 17	absltd	$⊢ φ \to (\|B\| < 1 \leftrightarrow (- 1 < B \land B < 1))$
26	24 6 25	mpbir2and	$⊢ φ \to \|B\| < 1$
27	13 26	expcnv	$⊢ φ \to (i \in ℕ_{0} ⟼ B^{i}) ⇝ 0$
28	2 27	eqbrtrid	$⊢ φ \to G ⇝ 0$
29	8 9 7 16 28	climi	$⊢ φ \to \exists n \in ℕ \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)$
30		r19.26	$⊢ \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E) \leftrightarrow (\forall k \in ℤ_{\geq n} B^{k} \in ℂ \land \forall k \in ℤ_{\geq n} \|B^{k} - 0\| < E)$
31	30	simprbi	$⊢ \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E) \to \forall k \in ℤ_{\geq n} \|B^{k} - 0\| < E$
32	31	ad2antlr	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to \forall k \in ℤ_{\geq n} \|B^{k} - 0\| < E$
33		oveq2	$⊢ k = i \to B^{k} = B^{i}$
34	33	oveq1d	$⊢ k = i \to B^{k} - 0 = B^{i} - 0$
35	34	fveq2d	$⊢ k = i \to \|B^{k} - 0\| = \|B^{i} - 0\|$
36	35	breq1d	$⊢ k = i \to (\|B^{k} - 0\| < E \leftrightarrow \|B^{i} - 0\| < E)$
37	36	rspccva	$⊢ (\forall k \in ℤ_{\geq n} \|B^{k} - 0\| < E \land i \in ℤ_{\geq n}) \to \|B^{i} - 0\| < E$
38	32 37	sylancom	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to \|B^{i} - 0\| < E$
39		simplll	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to φ$
40	39 5	syl	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to B \in ℝ^{+}$
41	40	rpred	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to B \in ℝ$
42		simpllr	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to n \in ℕ$
43		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
44	42 43	syl	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to n \in ℕ_{0}$
45		eluznn0	$⊢ (n \in ℕ_{0} \land i \in ℤ_{\geq n}) \to i \in ℕ_{0}$
46	44 45	sylancom	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to i \in ℕ_{0}$
47	41 46	reexpcld	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to B^{i} \in ℝ$
48		rpre	$⊢ E \in ℝ^{+} \to E \in ℝ$
49	39 7 48	3syl	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to E \in ℝ$
50		recn	$⊢ B^{i} \in ℝ \to B^{i} \in ℂ$
51	50	subid1d	$⊢ B^{i} \in ℝ \to B^{i} - 0 = B^{i}$
52	51	adantr	$⊢ (B^{i} \in ℝ \land E \in ℝ) \to B^{i} - 0 = B^{i}$
53	52	fveq2d	$⊢ (B^{i} \in ℝ \land E \in ℝ) \to \|B^{i} - 0\| = \|B^{i}\|$
54	53	breq1d	$⊢ (B^{i} \in ℝ \land E \in ℝ) \to (\|B^{i} - 0\| < E \leftrightarrow \|B^{i}\| < E)$
55		abslt	$⊢ (B^{i} \in ℝ \land E \in ℝ) \to (\|B^{i}\| < E \leftrightarrow (- E < B^{i} \land B^{i} < E))$
56	54 55	bitrd	$⊢ (B^{i} \in ℝ \land E \in ℝ) \to (\|B^{i} - 0\| < E \leftrightarrow (- E < B^{i} \land B^{i} < E))$
57	47 49 56	syl2anc	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to (\|B^{i} - 0\| < E \leftrightarrow (- E < B^{i} \land B^{i} < E))$
58	38 57	mpbid	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to (- E < B^{i} \land B^{i} < E)$
59	58	simprd	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to B^{i} < E$
60		eluznn	$⊢ (n \in ℕ \land i \in ℤ_{\geq n}) \to i \in ℕ$
61	42 60	sylancom	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to i \in ℕ$
62	20	adantr	$⊢ (φ \land i \in ℕ) \to B \in ℝ$
63		nnnn0	$⊢ i \in ℕ \to i \in ℕ_{0}$
64	63	adantl	$⊢ (φ \land i \in ℕ) \to i \in ℕ_{0}$
65	62 64	reexpcld	$⊢ (φ \land i \in ℕ) \to B^{i} \in ℝ$
66	7	rpred	$⊢ φ \to E \in ℝ$
67	66	adantr	$⊢ (φ \land i \in ℕ) \to E \in ℝ$
68		1red	$⊢ (φ \land i \in ℕ) \to 1 \in ℝ$
69	65 67 68	ltsub2d	$⊢ (φ \land i \in ℕ) \to (B^{i} < E \leftrightarrow 1 - E < 1 - B^{i})$
70	39 61 69	syl2anc	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to (B^{i} < E \leftrightarrow 1 - E < 1 - B^{i})$
71	59 70	mpbid	$⊢ (((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \land i \in ℤ_{\geq n}) \to 1 - E < 1 - B^{i}$
72	71	ralrimiva	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \to \forall i \in ℤ_{\geq n} 1 - E < 1 - B^{i}$
73	33	oveq2d	$⊢ k = i \to 1 - B^{k} = 1 - B^{i}$
74	73	breq2d	$⊢ k = i \to (1 - E < 1 - B^{k} \leftrightarrow 1 - E < 1 - B^{i})$
75	74	cbvralvw	$⊢ \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k} \leftrightarrow \forall i \in ℤ_{\geq n} 1 - E < 1 - B^{i}$
76	72 75	sylibr	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E)) \to \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k}$
77	76	ex	$⊢ (φ \land n \in ℕ) \to (\forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E) \to \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k})$
78	77	reximdva	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} (B^{k} \in ℂ \land \|B^{k} - 0\| < E) \to \exists n \in ℕ \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k})$
79	29 78	mpd	$⊢ φ \to \exists n \in ℕ \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k}$
80		oveq2	$⊢ i = k \to {(\frac{1}{A})}^{i} = {(\frac{1}{A})}^{k}$
81	3	recnd	$⊢ φ \to A \in ℂ$
82		0lt1	$⊢ 0 < 1$
83	82	a1i	$⊢ φ \to 0 < 1$
84	19 17 3 83 4	lttrd	$⊢ φ \to 0 < A$
85	84	gt0ne0d	$⊢ φ \to A \neq 0$
86	81 85	reccld	$⊢ φ \to \frac{1}{A} \in ℂ$
87	86	adantr	$⊢ (φ \land k \in ℕ) \to \frac{1}{A} \in ℂ$
88	87 12	expcld	$⊢ (φ \land k \in ℕ) \to {(\frac{1}{A})}^{k} \in ℂ$
89	1 80 12 88	fvmptd3	$⊢ (φ \land k \in ℕ) \to F (k) = {(\frac{1}{A})}^{k}$
90	3 85	rereccld	$⊢ φ \to \frac{1}{A} \in ℝ$
91	3 84	recgt0d	$⊢ φ \to 0 < \frac{1}{A}$
92	18 19 90 22 91	lttrd	$⊢ φ \to - 1 < \frac{1}{A}$
93		ltdiv23	$⊢ (1 \in ℝ \land (A \in ℝ \land 0 < A) \land (1 \in ℝ \land 0 < 1)) \to (\frac{1}{A} < 1 \leftrightarrow \frac{1}{1} < A)$
94	17 3 84 17 83 93	syl122anc	$⊢ φ \to (\frac{1}{A} < 1 \leftrightarrow \frac{1}{1} < A)$
95		1cnd	$⊢ φ \to 1 \in ℂ$
96	95	div1d	$⊢ φ \to \frac{1}{1} = 1$
97	96	breq1d	$⊢ φ \to (\frac{1}{1} < A \leftrightarrow 1 < A)$
98	94 97	bitrd	$⊢ φ \to (\frac{1}{A} < 1 \leftrightarrow 1 < A)$
99	4 98	mpbird	$⊢ φ \to \frac{1}{A} < 1$
100	90 17	absltd	$⊢ φ \to (\|\frac{1}{A}\| < 1 \leftrightarrow (- 1 < \frac{1}{A} \land \frac{1}{A} < 1))$
101	92 99 100	mpbir2and	$⊢ φ \to \|\frac{1}{A}\| < 1$
102	86 101	expcnv	$⊢ φ \to (i \in ℕ_{0} ⟼ {(\frac{1}{A})}^{i}) ⇝ 0$
103	1 102	eqbrtrid	$⊢ φ \to F ⇝ 0$
104	8 9 7 89 103	climi2	$⊢ φ \to \exists n \in ℕ \forall k \in ℤ_{\geq n} \|{(\frac{1}{A})}^{k} - 0\| < E$
105		simpll	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to φ$
106		uznnssnn	$⊢ n \in ℕ \to ℤ_{\geq n} \subseteq ℕ$
107	106	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to ℤ_{\geq n} \subseteq ℕ$
108		simpr	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to k \in ℤ_{\geq n}$
109	107 108	sseldd	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to k \in ℕ$
110	88	subid1d	$⊢ (φ \land k \in ℕ) \to {(\frac{1}{A})}^{k} - 0 = {(\frac{1}{A})}^{k}$
111	110	fveq2d	$⊢ (φ \land k \in ℕ) \to \|{(\frac{1}{A})}^{k} - 0\| = \|{(\frac{1}{A})}^{k}\|$
112	90	adantr	$⊢ (φ \land k \in ℕ) \to \frac{1}{A} \in ℝ$
113	112 12	reexpcld	$⊢ (φ \land k \in ℕ) \to {(\frac{1}{A})}^{k} \in ℝ$
114	19 90 91	ltled	$⊢ φ \to 0 \leq \frac{1}{A}$
115	114	adantr	$⊢ (φ \land k \in ℕ) \to 0 \leq \frac{1}{A}$
116	112 12 115	expge0d	$⊢ (φ \land k \in ℕ) \to 0 \leq {(\frac{1}{A})}^{k}$
117	113 116	absidd	$⊢ (φ \land k \in ℕ) \to \|{(\frac{1}{A})}^{k}\| = {(\frac{1}{A})}^{k}$
118	111 117	eqtrd	$⊢ (φ \land k \in ℕ) \to \|{(\frac{1}{A})}^{k} - 0\| = {(\frac{1}{A})}^{k}$
119	118	breq1d	$⊢ (φ \land k \in ℕ) \to (\|{(\frac{1}{A})}^{k} - 0\| < E \leftrightarrow {(\frac{1}{A})}^{k} < E)$
120	119	biimpd	$⊢ (φ \land k \in ℕ) \to (\|{(\frac{1}{A})}^{k} - 0\| < E \to {(\frac{1}{A})}^{k} < E)$
121	105 109 120	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in ℤ_{\geq n}) \to (\|{(\frac{1}{A})}^{k} - 0\| < E \to {(\frac{1}{A})}^{k} < E)$
122	121	ralimdva	$⊢ (φ \land n \in ℕ) \to (\forall k \in ℤ_{\geq n} \|{(\frac{1}{A})}^{k} - 0\| < E \to \forall k \in ℤ_{\geq n} {(\frac{1}{A})}^{k} < E)$
123	122	reximdva	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} \|{(\frac{1}{A})}^{k} - 0\| < E \to \exists n \in ℕ \forall k \in ℤ_{\geq n} {(\frac{1}{A})}^{k} < E)$
124	104 123	mpd	$⊢ φ \to \exists n \in ℕ \forall k \in ℤ_{\geq n} {(\frac{1}{A})}^{k} < E$
125	8	rexanuz2	$⊢ \exists n \in ℕ \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E) \leftrightarrow (\exists n \in ℕ \forall k \in ℤ_{\geq n} 1 - E < 1 - B^{k} \land \exists n \in ℕ \forall k \in ℤ_{\geq n} {(\frac{1}{A})}^{k} < E)$
126	79 124 125	sylanbrc	$⊢ φ \to \exists n \in ℕ \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)$
127		simpr	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)$
128		nnz	$⊢ n \in ℕ \to n \in ℤ$
129		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
130	128 129	syl	$⊢ n \in ℕ \to n \in ℤ_{\geq n}$
131	130	ad2antlr	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to n \in ℤ_{\geq n}$
132		oveq2	$⊢ k = n \to B^{k} = B^{n}$
133	132	oveq2d	$⊢ k = n \to 1 - B^{k} = 1 - B^{n}$
134	133	breq2d	$⊢ k = n \to (1 - E < 1 - B^{k} \leftrightarrow 1 - E < 1 - B^{n})$
135		oveq2	$⊢ k = n \to {(\frac{1}{A})}^{k} = {(\frac{1}{A})}^{n}$
136	135	breq1d	$⊢ k = n \to ({(\frac{1}{A})}^{k} < E \leftrightarrow {(\frac{1}{A})}^{n} < E)$
137	134 136	anbi12d	$⊢ k = n \to ((1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E) \leftrightarrow (1 - E < 1 - B^{n} \land {(\frac{1}{A})}^{n} < E))$
138	137	rspccva	$⊢ (\forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E) \land n \in ℤ_{\geq n}) \to (1 - E < 1 - B^{n} \land {(\frac{1}{A})}^{n} < E)$
139	127 131 138	syl2anc	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to (1 - E < 1 - B^{n} \land {(\frac{1}{A})}^{n} < E)$
140		1cnd	$⊢ (φ \land n \in ℕ) \to 1 \in ℂ$
141	81 85	jca	$⊢ φ \to (A \in ℂ \land A \neq 0)$
142	141	adantr	$⊢ (φ \land n \in ℕ) \to (A \in ℂ \land A \neq 0)$
143	43	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℕ_{0}$
144		expdiv	$⊢ (1 \in ℂ \land (A \in ℂ \land A \neq 0) \land n \in ℕ_{0}) \to {(\frac{1}{A})}^{n} = \frac{1^{n}}{A^{n}}$
145	140 142 143 144	syl3anc	$⊢ (φ \land n \in ℕ) \to {(\frac{1}{A})}^{n} = \frac{1^{n}}{A^{n}}$
146	128	adantl	$⊢ (φ \land n \in ℕ) \to n \in ℤ$
147		1exp	$⊢ n \in ℤ \to 1^{n} = 1$
148	146 147	syl	$⊢ (φ \land n \in ℕ) \to 1^{n} = 1$
149	148	oveq1d	$⊢ (φ \land n \in ℕ) \to \frac{1^{n}}{A^{n}} = \frac{1}{A^{n}}$
150	145 149	eqtrd	$⊢ (φ \land n \in ℕ) \to {(\frac{1}{A})}^{n} = \frac{1}{A^{n}}$
151	150	breq1d	$⊢ (φ \land n \in ℕ) \to ({(\frac{1}{A})}^{n} < E \leftrightarrow \frac{1}{A^{n}} < E)$
152	151	adantr	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to ({(\frac{1}{A})}^{n} < E \leftrightarrow \frac{1}{A^{n}} < E)$
153	152	anbi2d	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to ((1 - E < 1 - B^{n} \land {(\frac{1}{A})}^{n} < E) \leftrightarrow (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E))$
154	139 153	mpbid	$⊢ ((φ \land n \in ℕ) \land \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E)) \to (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E)$
155	154	ex	$⊢ (φ \land n \in ℕ) \to (\forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E) \to (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E))$
156	155	reximdva	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} (1 - E < 1 - B^{k} \land {(\frac{1}{A})}^{k} < E) \to \exists n \in ℕ (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E))$
157	126 156	mpd	$⊢ φ \to \exists n \in ℕ (1 - E < 1 - B^{n} \land \frac{1}{A^{n}} < E)$

Metamath Proof Explorer

Theorem stoweidlem7

Proof