iseralt

Description: The alternating series test. If G ( k ) is a decreasing sequence that converges to 0 , then sum_ k e. Z ( -u 1 ^ k ) x. G ( k ) is a convergent series. (Note that the first term is positive if M is even, and negative if M is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -u 1 using isermulc2 .) (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 9-Jul-2022)

	Ref	Expression
Hypotheses	iseralt.1	$⊢ Z = ℤ_{\geq M}$
	iseralt.2	$⊢ φ \to M \in ℤ$
	iseralt.3	$⊢ φ \to G : Z ⟶ ℝ$
	iseralt.4	$⊢ (φ \land k \in Z) \to G (k + 1) \leq G (k)$
	iseralt.5	$⊢ φ \to G ⇝ 0$
	iseralt.6	$⊢ (φ \land k \in Z) \to F (k) = {(- 1)}^{k} G (k)$
Assertion	iseralt	$⊢ φ \to seq M (+ F) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		iseralt.1	$⊢ Z = ℤ_{\geq M}$
2		iseralt.2	$⊢ φ \to M \in ℤ$
3		iseralt.3	$⊢ φ \to G : Z ⟶ ℝ$
4		iseralt.4	$⊢ (φ \land k \in Z) \to G (k + 1) \leq G (k)$
5		iseralt.5	$⊢ φ \to G ⇝ 0$
6		iseralt.6	$⊢ (φ \land k \in Z) \to F (k) = {(- 1)}^{k} G (k)$
7		seqex	$⊢ seq M (+ F) \in V$
8	7	a1i	$⊢ φ \to seq M (+ F) \in V$
9		climrel	$⊢ Rel ⇝$
10	9	brrelex1i	$⊢ G ⇝ 0 \to G \in V$
11	5 10	syl	$⊢ φ \to G \in V$
12		eqidd	$⊢ (φ \land n \in Z) \to G (n) = G (n)$
13	3	ffvelrnda	$⊢ (φ \land n \in Z) \to G (n) \in ℝ$
14	13	recnd	$⊢ (φ \land n \in Z) \to G (n) \in ℂ$
15	1 2 11 12 14	clim0c	$⊢ φ \to (G ⇝ 0 \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|G (n)\| < x)$
16	5 15	mpbid	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|G (n)\| < x$
17		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to j \in Z$
18	17 1	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to j \in ℤ_{\geq M}$
19		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
20		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
21	18 19 20	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to j \in ℤ_{\geq j}$
22		peano2uz	$⊢ j \in ℤ_{\geq j} \to j + 1 \in ℤ_{\geq j}$
23		2fveq3	$⊢ n = j + 1 \to \|G (n)\| = \|G (j + 1)\|$
24	23	breq1d	$⊢ n = j + 1 \to (\|G (n)\| < x \leftrightarrow \|G (j + 1)\| < x)$
25	24	rspcv	$⊢ j + 1 \in ℤ_{\geq j} \to (\forall n \in ℤ_{\geq j} \|G (n)\| < x \to \|G (j + 1)\| < x)$
26	21 22 25	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall n \in ℤ_{\geq j} \|G (n)\| < x \to \|G (j + 1)\| < x)$
27		eluzelz	$⊢ n \in ℤ_{\geq j} \to n \in ℤ$
28	27	ad2antll	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n \in ℤ$
29	28	zcnd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n \in ℂ$
30	19 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
31	30	ad2antrl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j \in ℤ$
32	31	zcnd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j \in ℂ$
33	29 32	subcld	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j \in ℂ$
34		2cnd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 \in ℂ$
35		2ne0	$⊢ 2 \neq 0$
36	35	a1i	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 \neq 0$
37	33 34 36	divcan2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 (\frac{n - j}{2}) = n - j$
38	37	oveq2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + 2 (\frac{n - j}{2}) = j + n - j$
39	32 29	pncan3d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + n - j = n$
40	38 39	eqtr2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n = j + 2 (\frac{n - j}{2})$
41	40	adantr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to n = j + 2 (\frac{n - j}{2})$
42	41	fveq2d	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to seq M (+ F) (n) = seq M (+ F) (j + 2 (\frac{n - j}{2}))$
43	42	fvoveq1d	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| = \|seq M (+ F) (j + 2 (\frac{n - j}{2})) - seq M (+ F) (j)\|$
44		simpll	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to φ$
45		simpl	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to j \in Z$
46	45	ad2antlr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to j \in Z$
47		simpr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to \frac{n - j}{2} \in ℤ$
48	28 31	zsubcld	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j \in ℤ$
49	48	zred	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j \in ℝ$
50		2rp	$⊢ 2 \in ℝ^{+}$
51	50	a1i	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 \in ℝ^{+}$
52		eluzle	$⊢ n \in ℤ_{\geq j} \to j \leq n$
53	52	ad2antll	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j \leq n$
54	28	zred	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n \in ℝ$
55	31	zred	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j \in ℝ$
56	54 55	subge0d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (0 \leq n - j \leftrightarrow j \leq n)$
57	53 56	mpbird	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \leq n - j$
58	49 51 57	divge0d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \leq \frac{n - j}{2}$
59	58	adantr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to 0 \leq \frac{n - j}{2}$
60		elnn0z	$⊢ \frac{n - j}{2} \in ℕ_{0} \leftrightarrow (\frac{n - j}{2} \in ℤ \land 0 \leq \frac{n - j}{2})$
61	47 59 60	sylanbrc	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to \frac{n - j}{2} \in ℕ_{0}$
62	1 2 3 4 5 6	iseraltlem3	$⊢ (φ \land j \in Z \land \frac{n - j}{2} \in ℕ_{0}) \to (\|seq M (+ F) (j + 2 (\frac{n - j}{2})) - seq M (+ F) (j)\| \leq G (j + 1) \land \|seq M (+ F) (j + 2 (\frac{n - j}{2}) + 1) - seq M (+ F) (j)\| \leq G (j + 1))$
63	62	simpld	$⊢ (φ \land j \in Z \land \frac{n - j}{2} \in ℕ_{0}) \to \|seq M (+ F) (j + 2 (\frac{n - j}{2})) - seq M (+ F) (j)\| \leq G (j + 1)$
64	44 46 61 63	syl3anc	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to \|seq M (+ F) (j + 2 (\frac{n - j}{2})) - seq M (+ F) (j)\| \leq G (j + 1)$
65	43 64	eqbrtrd	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j}{2} \in ℤ) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \leq G (j + 1)$
66		2div2e1	$⊢ \frac{2}{2} = 1$
67	66	oveq2i	$⊢ (\frac{n - j + 1}{2}) - (\frac{2}{2}) = (\frac{n - j + 1}{2}) - 1$
68		peano2cn	$⊢ n - j \in ℂ \to n - j + 1 \in ℂ$
69	33 68	syl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j + 1 \in ℂ$
70	69 34 34 36	divsubdird	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \frac{(n - j) + 1 - 2}{2} = (\frac{n - j + 1}{2}) - (\frac{2}{2})$
71		df-2	$⊢ 2 = 1 + 1$
72	71	oveq2i	$⊢ (n - j) + 1 - 2 = (n - j) + 1 - (1 + 1)$
73		ax-1cn	$⊢ 1 \in ℂ$
74	73	a1i	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 1 \in ℂ$
75	33 74 74	pnpcan2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (n - j) + 1 - (1 + 1) = n - j - 1$
76	72 75	eqtrid	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (n - j) + 1 - 2 = n - j - 1$
77	76	oveq1d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \frac{(n - j) + 1 - 2}{2} = \frac{n - j - 1}{2}$
78	70 77	eqtr3d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (\frac{n - j + 1}{2}) - (\frac{2}{2}) = \frac{n - j - 1}{2}$
79	67 78	eqtr3id	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (\frac{n - j + 1}{2}) - 1 = \frac{n - j - 1}{2}$
80	79	oveq2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 ((\frac{n - j + 1}{2}) - 1) = 2 (\frac{n - j - 1}{2})$
81		subcl	$⊢ (n - j \in ℂ \land 1 \in ℂ) \to n - j - 1 \in ℂ$
82	33 73 81	sylancl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j - 1 \in ℂ$
83	82 34 36	divcan2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 (\frac{n - j - 1}{2}) = n - j - 1$
84	29 32 74	sub32d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j - 1 = n - 1 - j$
85	80 83 84	3eqtrd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 2 ((\frac{n - j + 1}{2}) - 1) = n - 1 - j$
86	85	oveq2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + 2 ((\frac{n - j + 1}{2}) - 1) = j + (n - 1) - j$
87		subcl	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 \in ℂ$
88	29 73 87	sylancl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - 1 \in ℂ$
89	32 88	pncan3d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + (n - 1) - j = n - 1$
90	86 89	eqtrd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + 2 ((\frac{n - j + 1}{2}) - 1) = n - 1$
91	90	oveq1d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to j + 2 ((\frac{n - j + 1}{2}) - 1) + 1 = n - 1 + 1$
92		npcan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 + 1 = n$
93	29 73 92	sylancl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - 1 + 1 = n$
94	91 93	eqtr2d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n = j + 2 ((\frac{n - j + 1}{2}) - 1) + 1$
95	94	adantr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to n = j + 2 ((\frac{n - j + 1}{2}) - 1) + 1$
96	95	fveq2d	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to seq M (+ F) (n) = seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1) + 1)$
97	96	fvoveq1d	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| = \|seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1) + 1) - seq M (+ F) (j)\|$
98		simpll	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to φ$
99	45	ad2antlr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to j \in Z$
100		simpr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to \frac{n - j + 1}{2} \in ℤ$
101		uznn0sub	$⊢ n \in ℤ_{\geq j} \to n - j \in ℕ_{0}$
102	101	ad2antll	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j \in ℕ_{0}$
103		nn0p1nn	$⊢ n - j \in ℕ_{0} \to n - j + 1 \in ℕ$
104	102 103	syl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j + 1 \in ℕ$
105	104	nnrpd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to n - j + 1 \in ℝ^{+}$
106	105	rphalfcld	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \frac{n - j + 1}{2} \in ℝ^{+}$
107	106	rpgt0d	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 < \frac{n - j + 1}{2}$
108	107	adantr	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to 0 < \frac{n - j + 1}{2}$
109		elnnz	$⊢ \frac{n - j + 1}{2} \in ℕ \leftrightarrow (\frac{n - j + 1}{2} \in ℤ \land 0 < \frac{n - j + 1}{2})$
110	100 108 109	sylanbrc	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to \frac{n - j + 1}{2} \in ℕ$
111		nnm1nn0	$⊢ \frac{n - j + 1}{2} \in ℕ \to (\frac{n - j + 1}{2}) - 1 \in ℕ_{0}$
112	110 111	syl	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to (\frac{n - j + 1}{2}) - 1 \in ℕ_{0}$
113	1 2 3 4 5 6	iseraltlem3	$⊢ (φ \land j \in Z \land (\frac{n - j + 1}{2}) - 1 \in ℕ_{0}) \to (\|seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1)) - seq M (+ F) (j)\| \leq G (j + 1) \land \|seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1) + 1) - seq M (+ F) (j)\| \leq G (j + 1))$
114	113	simprd	$⊢ (φ \land j \in Z \land (\frac{n - j + 1}{2}) - 1 \in ℕ_{0}) \to \|seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1) + 1) - seq M (+ F) (j)\| \leq G (j + 1)$
115	98 99 112 114	syl3anc	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to \|seq M (+ F) (j + 2 ((\frac{n - j + 1}{2}) - 1) + 1) - seq M (+ F) (j)\| \leq G (j + 1)$
116	97 115	eqbrtrd	$⊢ ((φ \land (j \in Z \land n \in ℤ_{\geq j})) \land \frac{n - j + 1}{2} \in ℤ) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \leq G (j + 1)$
117		zeo	$⊢ n - j \in ℤ \to (\frac{n - j}{2} \in ℤ \lor \frac{n - j + 1}{2} \in ℤ)$
118	48 117	syl	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to (\frac{n - j}{2} \in ℤ \lor \frac{n - j + 1}{2} \in ℤ)$
119	65 116 118	mpjaodan	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \leq G (j + 1)$
120	1	peano2uzs	$⊢ j \in Z \to j + 1 \in Z$
121	120	adantr	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to j + 1 \in Z$
122		ffvelrn	$⊢ (G : Z ⟶ ℝ \land j + 1 \in Z) \to G (j + 1) \in ℝ$
123	3 121 122	syl2an	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to G (j + 1) \in ℝ$
124	1 2 3 4 5	iseraltlem1	$⊢ (φ \land j + 1 \in Z) \to 0 \leq G (j + 1)$
125	121 124	sylan2	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \leq G (j + 1)$
126	123 125	absidd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \|G (j + 1)\| = G (j + 1)$
127	119 126	breqtrrd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \leq \|G (j + 1)\|$
128	127	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \leq \|G (j + 1)\|$
129		neg1rr	$⊢ - 1 \in ℝ$
130	129	a1i	$⊢ (φ \land k \in Z) \to - 1 \in ℝ$
131		neg1ne0	$⊢ - 1 \neq 0$
132	131	a1i	$⊢ (φ \land k \in Z) \to - 1 \neq 0$
133		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
134	133 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
135	134	adantl	$⊢ (φ \land k \in Z) \to k \in ℤ$
136	130 132 135	reexpclzd	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} \in ℝ$
137	3	ffvelrnda	$⊢ (φ \land k \in Z) \to G (k) \in ℝ$
138	136 137	remulcld	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} G (k) \in ℝ$
139	6 138	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
140	1 2 139	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
141	1	uztrn2	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to n \in Z$
142		ffvelrn	$⊢ (seq M (+ F) : Z ⟶ ℝ \land n \in Z) \to seq M (+ F) (n) \in ℝ$
143	140 141 142	syl2an	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ F) (n) \in ℝ$
144		ffvelrn	$⊢ (seq M (+ F) : Z ⟶ ℝ \land j \in Z) \to seq M (+ F) (j) \in ℝ$
145	140 45 144	syl2an	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ F) (j) \in ℝ$
146	143 145	resubcld	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ F) (n) - seq M (+ F) (j) \in ℝ$
147	146	recnd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ F) (n) - seq M (+ F) (j) \in ℂ$
148	147	abscld	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \in ℝ$
149	148	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| \in ℝ$
150	126 123	eqeltrd	$⊢ (φ \land (j \in Z \land n \in ℤ_{\geq j})) \to \|G (j + 1)\| \in ℝ$
151	150	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|G (j + 1)\| \in ℝ$
152		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
153	152	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to x \in ℝ$
154		lelttr	$⊢ (\|seq M (+ F) (n) - seq M (+ F) (j)\| \in ℝ \land \|G (j + 1)\| \in ℝ \land x \in ℝ) \to ((\|seq M (+ F) (n) - seq M (+ F) (j)\| \leq \|G (j + 1)\| \land \|G (j + 1)\| < x) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| < x)$
155	149 151 153 154	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to ((\|seq M (+ F) (n) - seq M (+ F) (j)\| \leq \|G (j + 1)\| \land \|G (j + 1)\| < x) \to \|seq M (+ F) (n) - seq M (+ F) (j)\| < x)$
156	128 155	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (\|G (j + 1)\| < x \to \|seq M (+ F) (n) - seq M (+ F) (j)\| < x)$
157	140	adantr	$⊢ (φ \land x \in ℝ^{+}) \to seq M (+ F) : Z ⟶ ℝ$
158	157 141 142	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ F) (n) \in ℝ$
159	156 158	jctild	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (\|G (j + 1)\| < x \to (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
160	159	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land n \in ℤ_{\geq j}) \to (\|G (j + 1)\| < x \to (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
161	160	ralrimdva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\|G (j + 1)\| < x \to \forall n \in ℤ_{\geq j} (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
162	26 161	syld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall n \in ℤ_{\geq j} \|G (n)\| < x \to \forall n \in ℤ_{\geq j} (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
163	162	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall n \in ℤ_{\geq j} \|G (n)\| < x \to \exists j \in Z \forall n \in ℤ_{\geq j} (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
164	163	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|G (n)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x))$
165	16 164	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} (seq M (+ F) (n) \in ℝ \land \|seq M (+ F) (n) - seq M (+ F) (j)\| < x)$
166	1 8 165	caurcvg2	$⊢ φ \to seq M (+ F) \in dom ⇝$

Metamath Proof Explorer

Theorem iseralt

Proof