iseraltlem3

Description: Lemma for iseralt . From iseraltlem2 , we have ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) and ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) , and we also have ( -u 1 ^ n ) x. S ( n + 1 ) = ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) for each n by the definition of the partial sum S , so combining the inequalities we get ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) = ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) = ( -u 1 ^ n ) x. S ( n + 2 k ) - G ( n + 2 k + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) <_ ( -u 1 ^ n ) x. S ( n ) + G ( n + 1 ) , so | ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k + 1 ) - S ( n ) | <_ G ( n + 1 ) and | ( -u 1 ^ n ) x. S ( n + 2 k ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k ) - S ( n ) | <_ G ( n + 1 ) . Thus, both even and odd partial sums are Cauchy if G converges to 0 . (Contributed by Mario Carneiro, 6-Apr-2015)

	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	iseraltlem3	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (\|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| \leq G (N + 1) \land \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| \leq G (N + 1))$

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		neg1rr	$⊢ - 1 \in ℝ$
8	7	a1i	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to - 1 \in ℝ$
9		neg1ne0	$⊢ - 1 \neq 0$
10	9	a1i	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to - 1 \neq 0$
11		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
12	1 11	eqsstri	$⊢ Z \subseteq ℤ$
13		simp2	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N \in Z$
14	12 13	sselid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N \in ℤ$
15	8 10 14	reexpclzd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} \in ℝ$
16	15	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} \in ℂ$
17	7	a1i	$⊢ (φ \land k \in Z) \to - 1 \in ℝ$
18	9	a1i	$⊢ (φ \land k \in Z) \to - 1 \neq 0$
19		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
20	12 19	sselid	$⊢ (φ \land k \in Z) \to k \in ℤ$
21	17 18 20	reexpclzd	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} \in ℝ$
22	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to G (k) \in ℝ$
23	21 22	remulcld	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} G (k) \in ℝ$
24	6 23	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
25	1 2 24	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
26	25	3ad2ant1	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) : Z ⟶ ℝ$
27	13 1	eleqtrdi	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N \in ℤ_{\geq M}$
28		2nn0	$⊢ 2 \in ℕ_{0}$
29		simp3	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to K \in ℕ_{0}$
30		nn0mulcl	$⊢ (2 \in ℕ_{0} \land K \in ℕ_{0}) \to 2 K \in ℕ_{0}$
31	28 29 30	sylancr	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 2 K \in ℕ_{0}$
32		uzaddcl	$⊢ (N \in ℤ_{\geq M} \land 2 K \in ℕ_{0}) \to N + 2 K \in ℤ_{\geq M}$
33	27 31 32	syl2anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 2 K \in ℤ_{\geq M}$
34	33 1	eleqtrrdi	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 2 K \in Z$
35	26 34	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) \in ℝ$
36	35	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) \in ℂ$
37	26 13	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N) \in ℝ$
38	37	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N) \in ℂ$
39	16 36 38	subdid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} (seq M (+ F) (N + 2 K) - seq M (+ F) (N)) = {(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)$
40	39	fveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} (seq M (+ F) (N + 2 K) - seq M (+ F) (N))\| = \|{(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)\|$
41	35 37	resubcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) - seq M (+ F) (N) \in ℝ$
42	41	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) - seq M (+ F) (N) \in ℂ$
43	16 42	absmuld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} (seq M (+ F) (N + 2 K) - seq M (+ F) (N))\| = \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\|$
44	40 43	eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)\| = \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\|$
45	8	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to - 1 \in ℂ$
46		absexpz	$⊢ (- 1 \in ℂ \land - 1 \neq 0 \land N \in ℤ) \to \|{(- 1)}^{N}\| = {\|- 1\|}^{N}$
47	45 10 14 46	syl3anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N}\| = {\|- 1\|}^{N}$
48		ax-1cn	$⊢ 1 \in ℂ$
49	48	absnegi	$⊢ \|- 1\| = \|1\|$
50		abs1	$⊢ \|1\| = 1$
51	49 50	eqtri	$⊢ \|- 1\| = 1$
52	51	oveq1i	$⊢ {\|- 1\|}^{N} = 1^{N}$
53		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
54	14 53	syl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1^{N} = 1$
55	52 54	eqtrid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {\|- 1\|}^{N} = 1$
56	47 55	eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N}\| = 1$
57	56	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| = 1 \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\|$
58	42	abscld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| \in ℝ$
59	58	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| \in ℂ$
60	59	mullidd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1 \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| = \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\|$
61	44 57 60	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)\| = \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\|$
62	15 37	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) \in ℝ$
63	3	3ad2ant1	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to G : Z ⟶ ℝ$
64	1	peano2uzs	$⊢ N \in Z \to N + 1 \in Z$
65	64	3ad2ant2	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 1 \in Z$
66	63 65	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to G (N + 1) \in ℝ$
67	62 66	resubcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) - G (N + 1) \in ℝ$
68	1	peano2uzs	$⊢ N + 2 K \in Z \to N + 2 K + 1 \in Z$
69	34 68	syl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 2 K + 1 \in Z$
70	26 69	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) \in ℝ$
71	15 70	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \in ℝ$
72	15 35	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \in ℝ$
73		seqp1	$⊢ N \in ℤ_{\geq M} \to seq M (+ F) (N + 1) = seq M (+ F) (N) + F (N + 1)$
74	27 73	syl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1) = seq M (+ F) (N) + F (N + 1)$
75		fveq2	$⊢ k = N + 1 \to F (k) = F (N + 1)$
76		oveq2	$⊢ k = N + 1 \to {(- 1)}^{k} = {(- 1)}^{N + 1}$
77		fveq2	$⊢ k = N + 1 \to G (k) = G (N + 1)$
78	76 77	oveq12d	$⊢ k = N + 1 \to {(- 1)}^{k} G (k) = {(- 1)}^{N + 1} G (N + 1)$
79	75 78	eqeq12d	$⊢ k = N + 1 \to (F (k) = {(- 1)}^{k} G (k) \leftrightarrow F (N + 1) = {(- 1)}^{N + 1} G (N + 1))$
80	6	ralrimiva	$⊢ φ \to \forall k \in Z F (k) = {(- 1)}^{k} G (k)$
81	80	3ad2ant1	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \forall k \in Z F (k) = {(- 1)}^{k} G (k)$
82	79 81 65	rspcdva	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to F (N + 1) = {(- 1)}^{N + 1} G (N + 1)$
83	82	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N) + F (N + 1) = seq M (+ F) (N) + {(- 1)}^{N + 1} G (N + 1)$
84	45 10 14	expp1zd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} = {(- 1)}^{N} -1$
85		neg1cn	$⊢ - 1 \in ℂ$
86		mulcom	$⊢ ({(- 1)}^{N} \in ℂ \land - 1 \in ℂ) \to {(- 1)}^{N} -1 = -1 {(- 1)}^{N}$
87	16 85 86	sylancl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} -1 = -1 {(- 1)}^{N}$
88	16	mulm1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to -1 {(- 1)}^{N} = - {(- 1)}^{N}$
89	84 87 88	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} = - {(- 1)}^{N}$
90	89	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} G (N + 1) = (- {(- 1)}^{N}) G (N + 1)$
91	66	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to G (N + 1) \in ℂ$
92	16 91	mulneg1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) G (N + 1) = - {(- 1)}^{N} G (N + 1)$
93	90 92	eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} G (N + 1) = - {(- 1)}^{N} G (N + 1)$
94	93	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N) + {(- 1)}^{N + 1} G (N + 1) = seq M (+ F) (N) + (- {(- 1)}^{N} G (N + 1))$
95	74 83 94	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1) = seq M (+ F) (N) + (- {(- 1)}^{N} G (N + 1))$
96	15 66	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} G (N + 1) \in ℝ$
97	96	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} G (N + 1) \in ℂ$
98	38 97	negsubd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N) + (- {(- 1)}^{N} G (N + 1)) = seq M (+ F) (N) - {(- 1)}^{N} G (N + 1)$
99	95 98	eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1) = seq M (+ F) (N) - {(- 1)}^{N} G (N + 1)$
100	99	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 1) = {(- 1)}^{N} (seq M (+ F) (N) - {(- 1)}^{N} G (N + 1))$
101	16 38 97	subdid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} (seq M (+ F) (N) - {(- 1)}^{N} G (N + 1)) = {(- 1)}^{N} seq M (+ F) (N) - {(- 1)}^{N} {(- 1)}^{N} G (N + 1)$
102	14	zcnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N \in ℂ$
103	102	2timesd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 2 \cdot N = N + N$
104	103	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{2 \cdot N} = {(- 1)}^{N + N}$
105		2z	$⊢ 2 \in ℤ$
106	105	a1i	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 2 \in ℤ$
107		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land N \in ℤ)) \to {(- 1)}^{2 \cdot N} = {({-1}^{2})}^{N}$
108	45 10 106 14 107	syl22anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{2 \cdot N} = {({-1}^{2})}^{N}$
109	104 108	eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + N} = {({-1}^{2})}^{N}$
110		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
111	110	oveq1i	$⊢ {({-1}^{2})}^{N} = 1^{N}$
112	109 111	eqtrdi	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + N} = 1^{N}$
113		expaddz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (N \in ℤ \land N \in ℤ)) \to {(- 1)}^{N + N} = {(- 1)}^{N} {(- 1)}^{N}$
114	45 10 14 14 113	syl22anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + N} = {(- 1)}^{N} {(- 1)}^{N}$
115	112 114 54	3eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} = 1$
116	115	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 1) = 1 G (N + 1)$
117	16 16 91	mulassd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 1) = {(- 1)}^{N} {(- 1)}^{N} G (N + 1)$
118	91	mullidd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1 G (N + 1) = G (N + 1)$
119	116 117 118	3eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 1) = G (N + 1)$
120	119	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) - {(- 1)}^{N} {(- 1)}^{N} G (N + 1) = {(- 1)}^{N} seq M (+ F) (N) - G (N + 1)$
121	100 101 120	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 1) = {(- 1)}^{N} seq M (+ F) (N) - G (N + 1)$
122	1 2 3 4 5 6	iseraltlem2	$⊢ (φ \land N + 1 \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} seq M (+ F) (N + 1 + 2 K) \leq {(- 1)}^{N + 1} seq M (+ F) (N + 1)$
123	64 122	syl3an2	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} seq M (+ F) (N + 1 + 2 K) \leq {(- 1)}^{N + 1} seq M (+ F) (N + 1)$
124		1cnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1 \in ℂ$
125	31	nn0cnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 2 K \in ℂ$
126	102 124 125	add32d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 1 + 2 K = N + 2 K + 1$
127	126	fveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1 + 2 K) = seq M (+ F) (N + 2 K + 1)$
128	89 127	oveq12d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} seq M (+ F) (N + 1 + 2 K) = (- {(- 1)}^{N}) seq M (+ F) (N + 2 K + 1)$
129	89	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} seq M (+ F) (N + 1) = (- {(- 1)}^{N}) seq M (+ F) (N + 1)$
130	123 128 129	3brtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) seq M (+ F) (N + 2 K + 1) \leq (- {(- 1)}^{N}) seq M (+ F) (N + 1)$
131	70	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) \in ℂ$
132	16 131	mulneg1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) seq M (+ F) (N + 2 K + 1) = - {(- 1)}^{N} seq M (+ F) (N + 2 K + 1)$
133	26 65	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1) \in ℝ$
134	133	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 1) \in ℂ$
135	16 134	mulneg1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) seq M (+ F) (N + 1) = - {(- 1)}^{N} seq M (+ F) (N + 1)$
136	130 132 135	3brtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to - {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leq - {(- 1)}^{N} seq M (+ F) (N + 1)$
137	15 133	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 1) \in ℝ$
138	137 71	lenegd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to ({(- 1)}^{N} seq M (+ F) (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leftrightarrow - {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leq - {(- 1)}^{N} seq M (+ F) (N + 1))$
139	136 138	mpbird	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K + 1)$
140	121 139	eqbrtrrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) - G (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K + 1)$
141		seqp1	$⊢ N + 2 K \in ℤ_{\geq M} \to seq M (+ F) (N + 2 K + 1) = seq M (+ F) (N + 2 K) + F (N + 2 K + 1)$
142	33 141	syl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) = seq M (+ F) (N + 2 K) + F (N + 2 K + 1)$
143		fveq2	$⊢ k = N + 2 K + 1 \to F (k) = F (N + 2 K + 1)$
144		oveq2	$⊢ k = N + 2 K + 1 \to {(- 1)}^{k} = {(- 1)}^{N + 2 K + 1}$
145		fveq2	$⊢ k = N + 2 K + 1 \to G (k) = G (N + 2 K + 1)$
146	144 145	oveq12d	$⊢ k = N + 2 K + 1 \to {(- 1)}^{k} G (k) = {(- 1)}^{N + 2 K + 1} G (N + 2 K + 1)$
147	143 146	eqeq12d	$⊢ k = N + 2 K + 1 \to (F (k) = {(- 1)}^{k} G (k) \leftrightarrow F (N + 2 K + 1) = {(- 1)}^{N + 2 K + 1} G (N + 2 K + 1))$
148	147 81 69	rspcdva	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to F (N + 2 K + 1) = {(- 1)}^{N + 2 K + 1} G (N + 2 K + 1)$
149	12 65	sselid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to N + 1 \in ℤ$
150	31	nn0zd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 2 K \in ℤ$
151		expaddz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (N + 1 \in ℤ \land 2 K \in ℤ)) \to {(- 1)}^{N + 1 + 2 K} = {(- 1)}^{N + 1} {(- 1)}^{2 K}$
152	45 10 149 150 151	syl22anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1 + 2 K} = {(- 1)}^{N + 1} {(- 1)}^{2 K}$
153	29	nn0zd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to K \in ℤ$
154		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land K \in ℤ)) \to {(- 1)}^{2 K} = {({-1}^{2})}^{K}$
155	45 10 106 153 154	syl22anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{2 K} = {({-1}^{2})}^{K}$
156	110	oveq1i	$⊢ {({-1}^{2})}^{K} = 1^{K}$
157		1exp	$⊢ K \in ℤ \to 1^{K} = 1$
158	153 157	syl	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1^{K} = 1$
159	156 158	eqtrid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {({-1}^{2})}^{K} = 1$
160	155 159	eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{2 K} = 1$
161	89 160	oveq12d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1} {(- 1)}^{2 K} = (- {(- 1)}^{N}) \cdot 1$
162	152 161	eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1 + 2 K} = (- {(- 1)}^{N}) \cdot 1$
163	126	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 1 + 2 K} = {(- 1)}^{N + 2 K + 1}$
164	16	negcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to - {(- 1)}^{N} \in ℂ$
165	164	mulridd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) \cdot 1 = - {(- 1)}^{N}$
166	162 163 165	3eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 2 K + 1} = - {(- 1)}^{N}$
167	166	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N + 2 K + 1} G (N + 2 K + 1) = (- {(- 1)}^{N}) G (N + 2 K + 1)$
168	63 69	ffvelcdmd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to G (N + 2 K + 1) \in ℝ$
169	168	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to G (N + 2 K + 1) \in ℂ$
170	16 169	mulneg1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (- {(- 1)}^{N}) G (N + 2 K + 1) = - {(- 1)}^{N} G (N + 2 K + 1)$
171	148 167 170	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to F (N + 2 K + 1) = - {(- 1)}^{N} G (N + 2 K + 1)$
172	171	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) + F (N + 2 K + 1) = seq M (+ F) (N + 2 K) + (- {(- 1)}^{N} G (N + 2 K + 1))$
173	15 168	remulcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} G (N + 2 K + 1) \in ℝ$
174	173	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} G (N + 2 K + 1) \in ℂ$
175	36 174	negsubd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K) + (- {(- 1)}^{N} G (N + 2 K + 1)) = seq M (+ F) (N + 2 K) - {(- 1)}^{N} G (N + 2 K + 1)$
176	142 172 175	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) = seq M (+ F) (N + 2 K) - {(- 1)}^{N} G (N + 2 K + 1)$
177	176	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) = {(- 1)}^{N} (seq M (+ F) (N + 2 K) - {(- 1)}^{N} G (N + 2 K + 1))$
178	16 36 174	subdid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} (seq M (+ F) (N + 2 K) - {(- 1)}^{N} G (N + 2 K + 1)) = {(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1)$
179	115	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1) = 1 G (N + 2 K + 1)$
180	16 16 169	mulassd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1) = {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1)$
181	169	mullidd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1 G (N + 2 K + 1) = G (N + 2 K + 1)$
182	179 180 181	3eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1) = G (N + 2 K + 1)$
183	182	oveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} {(- 1)}^{N} G (N + 2 K + 1) = {(- 1)}^{N} seq M (+ F) (N + 2 K) - G (N + 2 K + 1)$
184	177 178 183	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) = {(- 1)}^{N} seq M (+ F) (N + 2 K) - G (N + 2 K + 1)$
185		simp1	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to φ$
186	1 2 3 4 5	iseraltlem1	$⊢ (φ \land N + 2 K + 1 \in Z) \to 0 \leq G (N + 2 K + 1)$
187	185 69 186	syl2anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 0 \leq G (N + 2 K + 1)$
188	72 168	subge02d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (0 \leq G (N + 2 K + 1) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N + 2 K) - G (N + 2 K + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K))$
189	187 188	mpbid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) - G (N + 2 K + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K)$
190	184 189	eqbrtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K)$
191	67 71 72 140 190	letrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) - G (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K)$
192	62 66	readdcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) + G (N + 1) \in ℝ$
193	1 2 3 4 5 6	iseraltlem2	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N)$
194	1 2 3 4 5	iseraltlem1	$⊢ (φ \land N + 1 \in Z) \to 0 \leq G (N + 1)$
195	185 65 194	syl2anc	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 0 \leq G (N + 1)$
196	62 66	addge01d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (0 \leq G (N + 1) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1))$
197	195 196	mpbid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1)$
198	72 62 192 193 197	letrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1)$
199	72 62 66	absdifled	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (\|{(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)\| \leq G (N + 1) \leftrightarrow ({(- 1)}^{N} seq M (+ F) (N) - G (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K) \land {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1)))$
200	191 198 199	mpbir2and	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K) - {(- 1)}^{N} seq M (+ F) (N)\| \leq G (N + 1)$
201	61 200	eqbrtrrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| \leq G (N + 1)$
202	16 131 38	subdid	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} (seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)) = {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)$
203	202	fveq2d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} (seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N))\| = \|{(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)\|$
204	70 37	resubcld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N) \in ℝ$
205	204	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N) \in ℂ$
206	16 205	absmuld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} (seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N))\| = \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\|$
207	203 206	eqtr3d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)\| = \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\|$
208	56	oveq1d	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N}\| \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| = 1 \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\|$
209	205	abscld	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| \in ℝ$
210	209	recnd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| \in ℂ$
211	210	mullidd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to 1 \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| = \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\|$
212	207 208 211	3eqtrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)\| = \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\|$
213	71 72 192 190 198	letrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1)$
214	71 62 66	absdifled	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (\|{(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)\| \leq G (N + 1) \leftrightarrow ({(- 1)}^{N} seq M (+ F) (N) - G (N + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \land {(- 1)}^{N} seq M (+ F) (N + 2 K + 1) \leq {(- 1)}^{N} seq M (+ F) (N) + G (N + 1)))$
215	140 213 214	mpbir2and	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|{(- 1)}^{N} seq M (+ F) (N + 2 K + 1) - {(- 1)}^{N} seq M (+ F) (N)\| \leq G (N + 1)$
216	212 215	eqbrtrrd	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| \leq G (N + 1)$
217	201 216	jca	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to (\|seq M (+ F) (N + 2 K) - seq M (+ F) (N)\| \leq G (N + 1) \land \|seq M (+ F) (N + 2 K + 1) - seq M (+ F) (N)\| \leq G (N + 1))$

Metamath Proof Explorer

Theorem iseraltlem3

Proof