Theorem iseraltlem2 15760

Description: Lemma for iseralt 15762. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example 𝑆(1) ≤ 𝑆(3) ≤ 𝑆(5) ≤ ... and ... ≤ 𝑆(4) ≤ 𝑆(2) ≤ 𝑆(0) (assuming 𝑀 = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.)

Hypotheses

Ref	Expression
iseralt.1	⊢ 𝑍 = (ℤ≥‘𝑀)
iseralt.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
iseralt.3	⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
iseralt.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
iseralt.5	⊢ (𝜑 → 𝐺 ⇝ 0)
iseralt.6	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))

Assertion

Ref	Expression
iseraltlem2	⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))

Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀   𝜑,𝑘   𝑘,𝐾   𝑘,𝑁   𝑘,𝑍

Proof of Theorem iseraltlem2

Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7431	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2		2t0e0 12429	. . . . . . . . . 10 ⊢ (2 · 0) = 0
3	1, 2	eqtrdi 2817	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
4	3	oveq2d 7439	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
5	4	fveq2d 6892	. . . . . . 7 ⊢ (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
6	5	oveq2d 7439	. . . . . 6 ⊢ (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
7	6	breq1d 5124	. . . . 5 ⊢ (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
8	7	imbi2d 343	. . . 4 ⊢ (𝑥 = 0 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9		oveq2 7431	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
10	9	oveq2d 7439	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
11	10	fveq2d 6892	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
12	11	oveq2d 7439	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
13	12	breq1d 5124	. . . . 5 ⊢ (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
14	13	imbi2d 343	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15		oveq2 7431	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
16	15	oveq2d 7439	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
17	16	fveq2d 6892	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
18	17	oveq2d 7439	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
19	18	breq1d 5124	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
20	19	imbi2d 343	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21		oveq2 7431	. . . . . . . . 9 ⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
22	21	oveq2d 7439	. . . . . . . 8 ⊢ (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
23	22	fveq2d 6892	. . . . . . 7 ⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
24	23	oveq2d 7439	. . . . . 6 ⊢ (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
25	24	breq1d 5124	. . . . 5 ⊢ (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
26	25	imbi2d 343	. . . 4 ⊢ (𝑥 = 𝐾 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27		iseralt.1	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ≥‘𝑀)
28		uzssz 12901	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
29	27, 28	eqsstri 3986	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ ℤ
30	29	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℤ)
31	30	sselda 3940	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℤ)
32	31	zcnd 12719	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℂ)
33	32	addridd 11428	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝑁 + 0) = 𝑁)
34	33	fveq2d 6892	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
35	34	oveq2d 7439	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36		neg1rr 12222	. . . . . . . 8 ⊢ -1 ∈ ℝ
37		neg1ne0 12223	. . . . . . . 8 ⊢ -1 ≠ 0
38		reexpclz 14138	. . . . . . . 8 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
39	36, 37, 31, 38	mp3an12i 1494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (-1↑𝑁) ∈ ℝ)
40		iseralt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41		iseralt.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
42	30	sselda 3940	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
43		reexpclz 14138	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
44	36, 37, 42, 43	mp3an12i 1494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ)
45		iseralt.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
46	45	ffvelcdmda 7086	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)
47	44, 46	remulcld 11257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ)
48	41, 47	eqeltrd 2866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
49	27, 40, 48	serfre 14087	. . . . . . . 8 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
50	49	ffvelcdmda 7086	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
51	39, 50	remulcld 11257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
52	51	leidd 11798	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
53	35, 52	eqbrtrd 5138	. . . 4 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
54	45	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55		ax-1cn 11176	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
56	55	2timesi 12396	. . . . . . . . . . . . . . 15 ⊢ (2 · 1) = (1 + 1)
57	56	oveq2i 7434	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ 𝑍)
59	58, 27	eleqtrdi 2876	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ (ℤ≥‘𝑀))
60	59	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ≥‘𝑀))
61		eluzelz 12890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
62	60, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
63	62	zcnd 12719	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64		2cn 12334	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
65		nn0cn 12532	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ)
66	65	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67		mulcl 11202	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
68	64, 66, 67	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
69	64, 55	mulcli 11234	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
71	63, 68, 70	addassd 11249	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
72	57, 71	eqtr3id 2815	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73		2nn0 12539	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
74		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75		nn0mulcl 12558	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
76	73, 74, 75	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77		uzaddcl 12946	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
78	60, 76, 77	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
79	28, 78	sselid 3938	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
80	79	zcnd 12719	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81		1cnd 11220	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
82	80, 81, 81	addassd 11249	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83		2cnd 12337	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
84	83, 66, 81	adddid 11251	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
85	84	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
86	72, 82, 85	3eqtr4d 2811	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87		peano2nn0 12562	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
88	87	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89		nn0mulcl 12558	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
90	73, 88, 89	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91		uzaddcl 12946	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
92	60, 90, 91	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
93	92, 27	eleqtrrdi 2877	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
94	86, 93	eqeltrd 2866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
95	54, 94	ffvelcdmd 7087	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96		peano2uz 12943	. . . . . . . . . . . . 13 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
97	78, 96	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
98	97, 27	eleqtrrdi 2877	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
99	54, 98	ffvelcdmd 7087	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
100	95, 99	resubcld 11660	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101		0red 11229	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
102	39	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
103	49	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
104	78, 27	eleqtrrdi 2877	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105	103, 104	ffvelcdmd 7087	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106	102, 105	remulcld 11257	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107		fvoveq1 7446	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109	107, 108	breq12d 5127	. . . . . . . . . . 11 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110		iseralt.4	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
111	110	ralrimiva 3160	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
112	111	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
113	109, 112, 98	rspcdva 3585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
114	95, 99	suble0d 11823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
115	113, 114	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0)
116	100, 101, 106, 115	leadd2dd 11847	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117		seqp1 14072	. . . . . . . . . . . . 13 ⊢ (((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
118	97, 117	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
119		seqp1 14072	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
120	78, 119	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
121	120	oveq1d 7438	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122	118, 121	eqtrd 2801	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
123	86	fveq2d 6892	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124	105	recnd 11255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125		fveq2 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126		oveq2 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
127	126, 108	oveq12d 7441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128	125, 127	eqeq12d 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
129	41	ralrimiva 3160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
130	129	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
131	128, 130, 98	rspcdva 3585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132		neg1cn 12221	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
133	132	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
134	37	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135	133, 134, 79	expp1zd 14211	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
136	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137	136, 134, 79	reexpclzd 14305	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138	137	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139		mulcom 11204	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
140	138, 132, 139	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
141	138	mulm1d 11684	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
142	135, 140, 141	3eqtrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
143	142	oveq1d 7438	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
144	99	recnd 11255	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145		mulneg12 11670	. . . . . . . . . . . . . . . 16 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
146	138, 144, 145	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
147	131, 143, 146	3eqtrd 2805	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
148	99	renegcld 11659	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149	137, 148	remulcld 11257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150	147, 149	eqeltrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151	150	recnd 11255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152		fveq2 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹‘𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153		oveq2 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154		fveq2 6888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺‘𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155	153, 154	oveq12d 7441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156	152, 155	eqeq12d 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157	156, 130, 94	rspcdva 3585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
158	79	peano2zd 12721	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159	133, 134, 158	expp1zd 14211	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160	142	oveq1d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
161		mul2neg 11671	. . . . . . . . . . . . . . . . . . 19 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
162	138, 55, 161	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
163	138	mulridd 11244	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
164	162, 163	eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
165	159, 160, 164	3eqtrd 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
166	165	oveq1d 7438	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167	157, 166	eqtrd 2801	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168	137, 95	remulcld 11257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169	167, 168	eqeltrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170	169	recnd 11255	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171	124, 151, 170	addassd 11249	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172	122, 123, 171	3eqtr3d 2809	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173	172	oveq2d 7439	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174	102	recnd 11255	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
175	150, 169	readdcld 11256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176	175	recnd 11255	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177	174, 124, 176	adddid 11251	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178	174, 151, 170	adddid 11251	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179	147	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180	148	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181	174, 138, 180	mulassd 11250	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182	179, 181	eqtr4d 2804	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
183	83, 63, 66	adddid 11251	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184	63	2timesd 12505	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185	184	oveq1d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
186	63, 63, 68	addassd 11249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187	183, 185, 186	3eqtrrd 2806	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188	187	oveq2d 7439	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
189		expaddz 14162	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
190	133, 134, 62, 79, 189	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
191		2z 12644	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℤ
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193		nn0z 12633	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
194		zaddcl 12652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
195	31, 193, 194	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196		expmulz 14164	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
197	133, 134, 192, 195, 196	syl22anc 852	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
198		neg1sqe1 14252	. . . . . . . . . . . . . . . . . 18 ⊢ (-1↑2) = 1
199	198	oveq1i 7433	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200		1exp 14147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201	195, 200	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202	199, 201	eqtrid 2813	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
203	197, 202	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
204	188, 190, 203	3eqtr3d 2809	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
205	204	oveq1d 7438	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206	180	mullidd 11245	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207	182, 205, 206	3eqtrd 2805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208	167	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
209	95	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210	174, 138, 209	mulassd 11250	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211	208, 210	eqtr4d 2804	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212	204	oveq1d 7438	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213	209	mullidd 11245	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214	211, 212, 213	3eqtrd 2805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215	207, 214	oveq12d 7441	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216	144	negcld 11574	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217	216, 209	addcomd 11430	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218	209, 144	negsubd 11593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219	217, 218	eqtrd 2801	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220	178, 215, 219	3eqtrd 2805	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221	220	oveq2d 7439	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222	173, 177, 221	3eqtrrd 2806	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223	106	recnd 11255	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224	223	addridd 11428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225	116, 222, 224	3brtr3d 5147	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226	103, 93	ffvelcdmd 7087	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227	102, 226	remulcld 11257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
228	51	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229		letr 11322	. . . . . . . 8 ⊢ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
230	227, 106, 228, 229	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
231	225, 230	mpand 708	. . . . . 6 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
232	231	expcom 419	. . . . 5 ⊢ (𝑛 ∈ ℕ0 → ((𝜑 ∧ 𝑁 ∈ 𝑍) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
233	232	a2d 30	. . . 4 ⊢ (𝑛 ∈ ℕ0 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
234	8, 14, 20, 26, 53, 233	nn0ind 12709	. . 3 ⊢ (𝐾 ∈ ℕ0 → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
235	234	com12 33	. 2 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
236	235	3impia 1135	1 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2961  ∀wral 3082   ⊆ wss 3908   class class class wbr 5114  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423  ℂcc 11116  ℝcr 11117  0cc0 11118  1c1 11119   + caddc 11121   · cmul 11123   ≤ cle 11262   − cmin 11459  -cneg 11460  2c2 12313  ℕ₀cn0 12522  ℤcz 12609  ℤ_≥cuz 12880  seqcseq 14057  ↑cexp 14117   ⇝ cli 15561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-n0 12523  df-z 12610  df-uz 12881  df-fz 13554  df-seq 14058  df-exp 14118

This theorem is used by:  iseraltlem3  15761