iseraltlem2

Description: Lemma for iseralt . The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S ( 1 ) <_ S ( 3 ) <_ S ( 5 ) <_ ... and ... <_ S ( 4 ) <_ S ( 2 ) <_ S ( 0 ) (assuming M = 0 so that these terms are defined). (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	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)$

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		oveq2	$⊢ x = 0 \to 2 x = 2 \cdot 0$
8		2t0e0	$⊢ 2 \cdot 0 = 0$
9	7 8	eqtrdi	$⊢ x = 0 \to 2 x = 0$
10	9	oveq2d	$⊢ x = 0 \to N + 2 x = N + 0$
11	10	fveq2d	$⊢ x = 0 \to seq M (+ F) (N + 2 x) = seq M (+ F) (N + 0)$
12	11	oveq2d	$⊢ x = 0 \to {(- 1)}^{N} seq M (+ F) (N + 2 x) = {(- 1)}^{N} seq M (+ F) (N + 0)$
13	12	breq1d	$⊢ x = 0 \to ({(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N + 0) \leq {(- 1)}^{N} seq M (+ F) (N))$
14	13	imbi2d	$⊢ x = 0 \to (((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N)) \leftrightarrow ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 0) \leq {(- 1)}^{N} seq M (+ F) (N)))$
15		oveq2	$⊢ x = n \to 2 x = 2 n$
16	15	oveq2d	$⊢ x = n \to N + 2 x = N + 2 n$
17	16	fveq2d	$⊢ x = n \to seq M (+ F) (N + 2 x) = seq M (+ F) (N + 2 n)$
18	17	oveq2d	$⊢ x = n \to {(- 1)}^{N} seq M (+ F) (N + 2 x) = {(- 1)}^{N} seq M (+ F) (N + 2 n)$
19	18	breq1d	$⊢ x = n \to ({(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N))$
20	19	imbi2d	$⊢ x = n \to (((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N)) \leftrightarrow ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N)))$
21		oveq2	$⊢ x = n + 1 \to 2 x = 2 (n + 1)$
22	21	oveq2d	$⊢ x = n + 1 \to N + 2 x = N + 2 (n + 1)$
23	22	fveq2d	$⊢ x = n + 1 \to seq M (+ F) (N + 2 x) = seq M (+ F) (N + 2 (n + 1))$
24	23	oveq2d	$⊢ x = n + 1 \to {(- 1)}^{N} seq M (+ F) (N + 2 x) = {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1))$
25	24	breq1d	$⊢ x = n + 1 \to ({(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N))$
26	25	imbi2d	$⊢ x = n + 1 \to (((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N)) \leftrightarrow ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N)))$
27		oveq2	$⊢ x = K \to 2 x = 2 K$
28	27	oveq2d	$⊢ x = K \to N + 2 x = N + 2 K$
29	28	fveq2d	$⊢ x = K \to seq M (+ F) (N + 2 x) = seq M (+ F) (N + 2 K)$
30	29	oveq2d	$⊢ x = K \to {(- 1)}^{N} seq M (+ F) (N + 2 x) = {(- 1)}^{N} seq M (+ F) (N + 2 K)$
31	30	breq1d	$⊢ x = K \to ({(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N) \leftrightarrow {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N))$
32	31	imbi2d	$⊢ x = K \to (((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 x) \leq {(- 1)}^{N} seq M (+ F) (N)) \leftrightarrow ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N)))$
33		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
34	1 33	eqsstri	$⊢ Z \subseteq ℤ$
35	34	a1i	$⊢ φ \to Z \subseteq ℤ$
36	35	sselda	$⊢ (φ \land N \in Z) \to N \in ℤ$
37	36	zcnd	$⊢ (φ \land N \in Z) \to N \in ℂ$
38	37	addridd	$⊢ (φ \land N \in Z) \to N + 0 = N$
39	38	fveq2d	$⊢ (φ \land N \in Z) \to seq M (+ F) (N + 0) = seq M (+ F) (N)$
40	39	oveq2d	$⊢ (φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 0) = {(- 1)}^{N} seq M (+ F) (N)$
41		neg1rr	$⊢ - 1 \in ℝ$
42		neg1ne0	$⊢ - 1 \neq 0$
43		reexpclz	$⊢ (- 1 \in ℝ \land - 1 \neq 0 \land N \in ℤ) \to {(- 1)}^{N} \in ℝ$
44	41 42 36 43	mp3an12i	$⊢ (φ \land N \in Z) \to {(- 1)}^{N} \in ℝ$
45	35	sselda	$⊢ (φ \land k \in Z) \to k \in ℤ$
46		reexpclz	$⊢ (- 1 \in ℝ \land - 1 \neq 0 \land k \in ℤ) \to {(- 1)}^{k} \in ℝ$
47	41 42 45 46	mp3an12i	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} \in ℝ$
48	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to G (k) \in ℝ$
49	47 48	remulcld	$⊢ (φ \land k \in Z) \to {(- 1)}^{k} G (k) \in ℝ$
50	6 49	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
51	1 2 50	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
52	51	ffvelcdmda	$⊢ (φ \land N \in Z) \to seq M (+ F) (N) \in ℝ$
53	44 52	remulcld	$⊢ (φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N) \in ℝ$
54	53	leidd	$⊢ (φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N) \leq {(- 1)}^{N} seq M (+ F) (N)$
55	40 54	eqbrtrd	$⊢ (φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 0) \leq {(- 1)}^{N} seq M (+ F) (N)$
56	3	ad2antrr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G : Z ⟶ ℝ$
57		ax-1cn	$⊢ 1 \in ℂ$
58	57	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
59	58	oveq2i	$⊢ N + 2 n + 2 \cdot 1 = N + 2 n + 1 + 1$
60		simpr	$⊢ (φ \land N \in Z) \to N \in Z$
61	60 1	eleqtrdi	$⊢ (φ \land N \in Z) \to N \in ℤ_{\geq M}$
62	61	adantr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N \in ℤ_{\geq M}$
63		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
64	62 63	syl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N \in ℤ$
65	64	zcnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N \in ℂ$
66		2cn	$⊢ 2 \in ℂ$
67		nn0cn	$⊢ n \in ℕ_{0} \to n \in ℂ$
68	67	adantl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to n \in ℂ$
69		mulcl	$⊢ (2 \in ℂ \land n \in ℂ) \to 2 n \in ℂ$
70	66 68 69	sylancr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 n \in ℂ$
71	66 57	mulcli	$⊢ 2 \cdot 1 \in ℂ$
72	71	a1i	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 \cdot 1 \in ℂ$
73	65 70 72	addassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n + 2 \cdot 1 = N + 2 n + 2 \cdot 1$
74	59 73	eqtr3id	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n + 1 + 1 = N + 2 n + 2 \cdot 1$
75		2nn0	$⊢ 2 \in ℕ_{0}$
76		simpr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
77		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
78	75 76 77	sylancr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
79		uzaddcl	$⊢ (N \in ℤ_{\geq M} \land 2 n \in ℕ_{0}) \to N + 2 n \in ℤ_{\geq M}$
80	62 78 79	syl2anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n \in ℤ_{\geq M}$
81	33 80	sselid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n \in ℤ$
82	81	zcnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n \in ℂ$
83		1cnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 1 \in ℂ$
84	82 83 83	addassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (N + 2 n) + 1 + 1 = N + 2 n + 1 + 1$
85		2cnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 \in ℂ$
86	85 68 83	adddid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 (n + 1) = 2 n + 2 \cdot 1$
87	86	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 (n + 1) = N + 2 n + 2 \cdot 1$
88	74 84 87	3eqtr4d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (N + 2 n) + 1 + 1 = N + 2 (n + 1)$
89		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
90	89	adantl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to n + 1 \in ℕ_{0}$
91		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n + 1 \in ℕ_{0}) \to 2 (n + 1) \in ℕ_{0}$
92	75 90 91	sylancr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 (n + 1) \in ℕ_{0}$
93		uzaddcl	$⊢ (N \in ℤ_{\geq M} \land 2 (n + 1) \in ℕ_{0}) \to N + 2 (n + 1) \in ℤ_{\geq M}$
94	62 92 93	syl2anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 (n + 1) \in ℤ_{\geq M}$
95	94 1	eleqtrrdi	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 (n + 1) \in Z$
96	88 95	eqeltrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (N + 2 n) + 1 + 1 \in Z$
97	56 96	ffvelcdmd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) \in ℝ$
98		peano2uz	$⊢ N + 2 n \in ℤ_{\geq M} \to N + 2 n + 1 \in ℤ_{\geq M}$
99	80 98	syl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n + 1 \in ℤ_{\geq M}$
100	99 1	eleqtrrdi	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n + 1 \in Z$
101	56 100	ffvelcdmd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G (N + 2 n + 1) \in ℝ$
102	97 101	resubcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1) \in ℝ$
103		0red	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 0 \in ℝ$
104	44	adantr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} \in ℝ$
105	51	ad2antrr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) : Z ⟶ ℝ$
106	80 1	eleqtrrdi	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n \in Z$
107	105 106	ffvelcdmd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 n) \in ℝ$
108	104 107	remulcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) \in ℝ$
109		fvoveq1	$⊢ k = N + 2 n + 1 \to G (k + 1) = G ((N + 2 n) + 1 + 1)$
110		fveq2	$⊢ k = N + 2 n + 1 \to G (k) = G (N + 2 n + 1)$
111	109 110	breq12d	$⊢ k = N + 2 n + 1 \to (G (k + 1) \leq G (k) \leftrightarrow G ((N + 2 n) + 1 + 1) \leq G (N + 2 n + 1))$
112	4	ralrimiva	$⊢ φ \to \forall k \in Z G (k + 1) \leq G (k)$
113	112	ad2antrr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to \forall k \in Z G (k + 1) \leq G (k)$
114	111 113 100	rspcdva	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) \leq G (N + 2 n + 1)$
115	97 101	suble0d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1) \leq 0 \leftrightarrow G ((N + 2 n) + 1 + 1) \leq G (N + 2 n + 1))$
116	114 115	mpbird	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1) \leq 0$
117	102 103 108 116	leadd2dd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) + G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1) \leq {(- 1)}^{N} seq M (+ F) (N + 2 n) + 0$
118		seqp1	$⊢ N + 2 n + 1 \in ℤ_{\geq M} \to seq M (+ F) ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
119	99 118	syl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
120		seqp1	$⊢ N + 2 n \in ℤ_{\geq M} \to seq M (+ F) (N + 2 n + 1) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1)$
121	80 120	syl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 n + 1) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1)$
122	121	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 n + 1) + F ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
123	119 122	eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
124	88	fveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 (n + 1))$
125	107	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 n) \in ℂ$
126		fveq2	$⊢ k = N + 2 n + 1 \to F (k) = F (N + 2 n + 1)$
127		oveq2	$⊢ k = N + 2 n + 1 \to {(- 1)}^{k} = {(- 1)}^{N + 2 n + 1}$
128	127 110	oveq12d	$⊢ k = N + 2 n + 1 \to {(- 1)}^{k} G (k) = {(- 1)}^{N + 2 n + 1} G (N + 2 n + 1)$
129	126 128	eqeq12d	$⊢ k = N + 2 n + 1 \to (F (k) = {(- 1)}^{k} G (k) \leftrightarrow F (N + 2 n + 1) = {(- 1)}^{N + 2 n + 1} G (N + 2 n + 1))$
130	6	ralrimiva	$⊢ φ \to \forall k \in Z F (k) = {(- 1)}^{k} G (k)$
131	130	ad2antrr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to \forall k \in Z F (k) = {(- 1)}^{k} G (k)$
132	129 131 100	rspcdva	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) = {(- 1)}^{N + 2 n + 1} G (N + 2 n + 1)$
133		neg1cn	$⊢ - 1 \in ℂ$
134	133	a1i	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - 1 \in ℂ$
135	42	a1i	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - 1 \neq 0$
136	134 135 81	expp1zd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n + 1} = {(- 1)}^{N + 2 n} -1$
137	41	a1i	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - 1 \in ℝ$
138	137 135 81	reexpclzd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} \in ℝ$
139	138	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} \in ℂ$
140		mulcom	$⊢ ({(- 1)}^{N + 2 n} \in ℂ \land - 1 \in ℂ) \to {(- 1)}^{N + 2 n} -1 = -1 {(- 1)}^{N + 2 n}$
141	139 133 140	sylancl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} -1 = -1 {(- 1)}^{N + 2 n}$
142	139	mulm1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to -1 {(- 1)}^{N + 2 n} = - {(- 1)}^{N + 2 n}$
143	136 141 142	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n + 1} = - {(- 1)}^{N + 2 n}$
144	143	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n + 1} G (N + 2 n + 1) = (- {(- 1)}^{N + 2 n}) G (N + 2 n + 1)$
145	101	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G (N + 2 n + 1) \in ℂ$
146		mulneg12	$⊢ ({(- 1)}^{N + 2 n} \in ℂ \land G (N + 2 n + 1) \in ℂ) \to (- {(- 1)}^{N + 2 n}) G (N + 2 n + 1) = {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
147	139 145 146	syl2anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (- {(- 1)}^{N + 2 n}) G (N + 2 n + 1) = {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
148	132 144 147	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) = {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
149	101	renegcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - G (N + 2 n + 1) \in ℝ$
150	138 149	remulcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} (- G (N + 2 n + 1)) \in ℝ$
151	148 150	eqeltrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) \in ℝ$
152	151	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) \in ℂ$
153		fveq2	$⊢ k = (N + 2 n) + 1 + 1 \to F (k) = F ((N + 2 n) + 1 + 1)$
154		oveq2	$⊢ k = (N + 2 n) + 1 + 1 \to {(- 1)}^{k} = {(- 1)}^{(N + 2 n) + 1 + 1}$
155		fveq2	$⊢ k = (N + 2 n) + 1 + 1 \to G (k) = G ((N + 2 n) + 1 + 1)$
156	154 155	oveq12d	$⊢ k = (N + 2 n) + 1 + 1 \to {(- 1)}^{k} G (k) = {(- 1)}^{(N + 2 n) + 1 + 1} G ((N + 2 n) + 1 + 1)$
157	153 156	eqeq12d	$⊢ k = (N + 2 n) + 1 + 1 \to (F (k) = {(- 1)}^{k} G (k) \leftrightarrow F ((N + 2 n) + 1 + 1) = {(- 1)}^{(N + 2 n) + 1 + 1} G ((N + 2 n) + 1 + 1))$
158	157 131 96	rspcdva	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F ((N + 2 n) + 1 + 1) = {(- 1)}^{(N + 2 n) + 1 + 1} G ((N + 2 n) + 1 + 1)$
159	81	peano2zd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + 2 n + 1 \in ℤ$
160	134 135 159	expp1zd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{(N + 2 n) + 1 + 1} = {(- 1)}^{N + 2 n + 1} -1$
161	143	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n + 1} -1 = (- {(- 1)}^{N + 2 n}) -1$
162		mul2neg	$⊢ ({(- 1)}^{N + 2 n} \in ℂ \land 1 \in ℂ) \to (- {(- 1)}^{N + 2 n}) -1 = {(- 1)}^{N + 2 n} \cdot 1$
163	139 57 162	sylancl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (- {(- 1)}^{N + 2 n}) -1 = {(- 1)}^{N + 2 n} \cdot 1$
164	139	mulridd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} \cdot 1 = {(- 1)}^{N + 2 n}$
165	163 164	eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (- {(- 1)}^{N + 2 n}) -1 = {(- 1)}^{N + 2 n}$
166	160 161 165	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{(N + 2 n) + 1 + 1} = {(- 1)}^{N + 2 n}$
167	166	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{(N + 2 n) + 1 + 1} G ((N + 2 n) + 1 + 1) = {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1)$
168	158 167	eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F ((N + 2 n) + 1 + 1) = {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1)$
169	138 97	remulcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1) \in ℝ$
170	168 169	eqeltrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F ((N + 2 n) + 1 + 1) \in ℝ$
171	170	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F ((N + 2 n) + 1 + 1) \in ℂ$
172	125 152 171	addassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
173	123 124 172	3eqtr3d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 (n + 1)) = seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)$
174	173	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) = {(- 1)}^{N} (seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1))$
175	104	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} \in ℂ$
176	151 170	readdcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1) \in ℝ$
177	176	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1) \in ℂ$
178	175 125 177	adddid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} (seq M (+ F) (N + 2 n) + F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)) = {(- 1)}^{N} seq M (+ F) (N + 2 n) + {(- 1)}^{N} (F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1))$
179	175 152 171	adddid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} (F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)) = {(- 1)}^{N} F (N + 2 n + 1) + {(- 1)}^{N} F ((N + 2 n) + 1 + 1)$
180	148	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F (N + 2 n + 1) = {(- 1)}^{N} {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
181	149	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - G (N + 2 n + 1) \in ℂ$
182	175 139 181	mulassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N + 2 n} (- G (N + 2 n + 1)) = {(- 1)}^{N} {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
183	180 182	eqtr4d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F (N + 2 n + 1) = {(- 1)}^{N} {(- 1)}^{N + 2 n} (- G (N + 2 n + 1))$
184	85 65 68	adddid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 (N + n) = 2 \cdot N + 2 n$
185	65	2timesd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 \cdot N = N + N$
186	185	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 \cdot N + 2 n = N + N + 2 n$
187	65 65 70	addassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + N + 2 n = N + N + 2 n$
188	184 186 187	3eqtrrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + N + 2 n = 2 (N + n)$
189	188	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + N + 2 n} = {(- 1)}^{2 (N + n)}$
190		expaddz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (N \in ℤ \land N + 2 n \in ℤ)) \to {(- 1)}^{N + N + 2 n} = {(- 1)}^{N} {(- 1)}^{N + 2 n}$
191	134 135 64 81 190	syl22anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N + N + 2 n} = {(- 1)}^{N} {(- 1)}^{N + 2 n}$
192		2z	$⊢ 2 \in ℤ$
193	192	a1i	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 2 \in ℤ$
194		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
195		zaddcl	$⊢ (N \in ℤ \land n \in ℤ) \to N + n \in ℤ$
196	36 194 195	syl2an	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to N + n \in ℤ$
197		expmulz	$⊢ ((- 1 \in ℂ \land - 1 \neq 0) \land (2 \in ℤ \land N + n \in ℤ)) \to {(- 1)}^{2 (N + n)} = {({-1}^{2})}^{N + n}$
198	134 135 193 196 197	syl22anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{2 (N + n)} = {({-1}^{2})}^{N + n}$
199		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
200	199	oveq1i	$⊢ {({-1}^{2})}^{N + n} = 1^{N + n}$
201		1exp	$⊢ N + n \in ℤ \to 1^{N + n} = 1$
202	196 201	syl	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 1^{N + n} = 1$
203	200 202	eqtrid	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {({-1}^{2})}^{N + n} = 1$
204	198 203	eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{2 (N + n)} = 1$
205	189 191 204	3eqtr3d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N + 2 n} = 1$
206	205	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N + 2 n} (- G (N + 2 n + 1)) = 1 (- G (N + 2 n + 1))$
207	181	mullidd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 1 (- G (N + 2 n + 1)) = - G (N + 2 n + 1)$
208	183 206 207	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F (N + 2 n + 1) = - G (N + 2 n + 1)$
209	168	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F ((N + 2 n) + 1 + 1) = {(- 1)}^{N} {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1)$
210	97	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) \in ℂ$
211	175 139 210	mulassd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1) = {(- 1)}^{N} {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1)$
212	209 211	eqtr4d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F ((N + 2 n) + 1 + 1) = {(- 1)}^{N} {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1)$
213	205	oveq1d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N + 2 n} G ((N + 2 n) + 1 + 1) = 1 G ((N + 2 n) + 1 + 1)$
214	210	mullidd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to 1 G ((N + 2 n) + 1 + 1) = G ((N + 2 n) + 1 + 1)$
215	212 213 214	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F ((N + 2 n) + 1 + 1) = G ((N + 2 n) + 1 + 1)$
216	208 215	oveq12d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} F (N + 2 n + 1) + {(- 1)}^{N} F ((N + 2 n) + 1 + 1) = - G (N + 2 n + 1) + G ((N + 2 n) + 1 + 1)$
217	145	negcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - G (N + 2 n + 1) \in ℂ$
218	217 210	addcomd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - G (N + 2 n + 1) + G ((N + 2 n) + 1 + 1) = G ((N + 2 n) + 1 + 1) + (- G (N + 2 n + 1))$
219	210 145	negsubd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to G ((N + 2 n) + 1 + 1) + (- G (N + 2 n + 1)) = G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1)$
220	218 219	eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to - G (N + 2 n + 1) + G ((N + 2 n) + 1 + 1) = G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1)$
221	179 216 220	3eqtrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} (F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)) = G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1)$
222	221	oveq2d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) + {(- 1)}^{N} (F (N + 2 n + 1) + F ((N + 2 n) + 1 + 1)) = {(- 1)}^{N} seq M (+ F) (N + 2 n) + G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1)$
223	174 178 222	3eqtrrd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) + G ((N + 2 n) + 1 + 1) - G (N + 2 n + 1) = {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1))$
224	108	recnd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) \in ℂ$
225	224	addridd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) + 0 = {(- 1)}^{N} seq M (+ F) (N + 2 n)$
226	117 223 225	3brtr3d	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N + 2 n)$
227	105 95	ffvelcdmd	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to seq M (+ F) (N + 2 (n + 1)) \in ℝ$
228	104 227	remulcld	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \in ℝ$
229	53	adantr	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N) \in ℝ$
230		letr	$⊢ ({(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \in ℝ \land {(- 1)}^{N} seq M (+ F) (N + 2 n) \in ℝ \land {(- 1)}^{N} seq M (+ F) (N) \in ℝ) \to (({(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N + 2 n) \land {(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N)) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N))$
231	228 108 229 230	syl3anc	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to (({(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N + 2 n) \land {(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N)) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N))$
232	226 231	mpand	$⊢ ((φ \land N \in Z) \land n \in ℕ_{0}) \to ({(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N))$
233	232	expcom	$⊢ n \in ℕ_{0} \to ((φ \land N \in Z) \to ({(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N)))$
234	233	a2d	$⊢ n \in ℕ_{0} \to (((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 n) \leq {(- 1)}^{N} seq M (+ F) (N)) \to ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 (n + 1)) \leq {(- 1)}^{N} seq M (+ F) (N)))$
235	14 20 26 32 55 234	nn0ind	$⊢ K \in ℕ_{0} \to ((φ \land N \in Z) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N))$
236	235	com12	$⊢ (φ \land N \in Z) \to (K \in ℕ_{0} \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N))$
237	236	3impia	$⊢ (φ \land N \in Z \land K \in ℕ_{0}) \to {(- 1)}^{N} seq M (+ F) (N + 2 K) \leq {(- 1)}^{N} seq M (+ F) (N)$

Metamath Proof Explorer

Theorem iseraltlem2

Proof