Theorem iseraltlem2 15031

Description: Lemma for iseralt 15033. 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 7143	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2		2t0e0 11794	. . . . . . . . . 10 ⊢ (2 · 0) = 0
3	1, 2	eqtrdi 2849	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
4	3	oveq2d 7151	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
5	4	fveq2d 6649	. . . . . . 7 ⊢ (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
6	5	oveq2d 7151	. . . . . 6 ⊢ (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
7	6	breq1d 5040	. . . . 5 ⊢ (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
8	7	imbi2d 344	. . . 4 ⊢ (𝑥 = 0 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
9		oveq2 7143	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
10	9	oveq2d 7151	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
11	10	fveq2d 6649	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
12	11	oveq2d 7151	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
13	12	breq1d 5040	. . . . 5 ⊢ (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
14	13	imbi2d 344	. . . 4 ⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
15		oveq2 7143	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
16	15	oveq2d 7151	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
17	16	fveq2d 6649	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
18	17	oveq2d 7151	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
19	18	breq1d 5040	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
20	19	imbi2d 344	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
21		oveq2 7143	. . . . . . . . 9 ⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
22	21	oveq2d 7151	. . . . . . . 8 ⊢ (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
23	22	fveq2d 6649	. . . . . . 7 ⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
24	23	oveq2d 7151	. . . . . 6 ⊢ (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
25	24	breq1d 5040	. . . . 5 ⊢ (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
26	25	imbi2d 344	. . . 4 ⊢ (𝑥 = 𝐾 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
27		iseralt.1	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ≥‘𝑀)
28		uzssz 12252	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
29	27, 28	eqsstri 3949	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ ℤ
30	29	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℤ)
31	30	sselda 3915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℤ)
32	31	zcnd 12076	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℂ)
33	32	addid1d 10829	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝑁 + 0) = 𝑁)
34	33	fveq2d 6649	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
35	34	oveq2d 7151	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36		neg1rr 11740	. . . . . . . 8 ⊢ -1 ∈ ℝ
37		neg1ne0 11741	. . . . . . . 8 ⊢ -1 ≠ 0
38		reexpclz 13445	. . . . . . . 8 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
39	36, 37, 31, 38	mp3an12i 1462	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (-1↑𝑁) ∈ ℝ)
40		iseralt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41		iseralt.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
42	30	sselda 3915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
43		reexpclz 13445	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
44	36, 37, 42, 43	mp3an12i 1462	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ)
45		iseralt.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
46	45	ffvelrnda 6828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)
47	44, 46	remulcld 10660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ)
48	41, 47	eqeltrd 2890	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
49	27, 40, 48	serfre 13395	. . . . . . . 8 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
50	49	ffvelrnda 6828	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
51	39, 50	remulcld 10660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
52	51	leidd 11195	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
53	35, 52	eqbrtrd 5052	. . . 4 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
54	45	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55		ax-1cn 10584	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
56	55	2timesi 11763	. . . . . . . . . . . . . . 15 ⊢ (2 · 1) = (1 + 1)
57	56	oveq2i 7146	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ 𝑍)
59	58, 27	eleqtrdi 2900	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ (ℤ≥‘𝑀))
60	59	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ≥‘𝑀))
61		eluzelz 12241	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
62	60, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
63	62	zcnd 12076	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64		2cn 11700	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
65		nn0cn 11895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ)
66	65	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67		mulcl 10610	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
68	64, 66, 67	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
69	64, 55	mulcli 10637	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
71	63, 68, 70	addassd 10652	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
72	57, 71	syl5eqr 2847	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73		2nn0 11902	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
74		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75		nn0mulcl 11921	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
76	73, 74, 75	sylancr 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77		uzaddcl 12292	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
78	60, 76, 77	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
79	28, 78	sseldi 3913	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
80	79	zcnd 12076	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81		1cnd 10625	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
82	80, 81, 81	addassd 10652	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83		2cnd 11703	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
84	83, 66, 81	adddid 10654	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
85	84	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
86	72, 82, 85	3eqtr4d 2843	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87		peano2nn0 11925	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
88	87	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89		nn0mulcl 11921	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
90	73, 88, 89	sylancr 590	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91		uzaddcl 12292	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
92	60, 90, 91	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
93	92, 27	eleqtrrdi 2901	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
94	86, 93	eqeltrd 2890	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
95	54, 94	ffvelrnd 6829	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96		peano2uz 12289	. . . . . . . . . . . . 13 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
97	78, 96	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
98	97, 27	eleqtrrdi 2901	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
99	54, 98	ffvelrnd 6829	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
100	95, 99	resubcld 11057	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101		0red 10633	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
102	39	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
103	49	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
104	78, 27	eleqtrrdi 2901	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105	103, 104	ffvelrnd 6829	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106	102, 105	remulcld 10660	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107		fvoveq1 7158	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109	107, 108	breq12d 5043	. . . . . . . . . . 11 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110		iseralt.4	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
111	110	ralrimiva 3149	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
112	111	ad2antrr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
113	109, 112, 98	rspcdva 3573	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
114	95, 99	suble0d 11220	. . . . . . . . . 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 11244	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117		seqp1 13379	. . . . . . . . . . . . 13 ⊢ (((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
118	97, 117	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
119		seqp1 13379	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
120	78, 119	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))))
121	120	oveq1d 7150	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122	118, 121	eqtrd 2833	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
123	86	fveq2d 6649	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124	105	recnd 10658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126		oveq2 7143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
127	126, 108	oveq12d 7153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128	125, 127	eqeq12d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
129	41	ralrimiva 3149	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
130	129	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
131	128, 130, 98	rspcdva 3573	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132		neg1cn 11739	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
133	132	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
134	37	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135	133, 134, 79	expp1zd 13515	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
136	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137	136, 134, 79	reexpclzd 13606	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138	137	recnd 10658	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139		mulcom 10612	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
140	138, 132, 139	sylancl 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
141	138	mulm1d 11081	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
142	135, 140, 141	3eqtrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
143	142	oveq1d 7150	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
144	99	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145		mulneg12 11067	. . . . . . . . . . . . . . . 16 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
146	138, 144, 145	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
147	131, 143, 146	3eqtrd 2837	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
148	99	renegcld 11056	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149	137, 148	remulcld 10660	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150	147, 149	eqeltrd 2890	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151	150	recnd 10658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹‘𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153		oveq2 7143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154		fveq2 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺‘𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155	153, 154	oveq12d 7153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156	152, 155	eqeq12d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157	156, 130, 94	rspcdva 3573	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
158	79	peano2zd 12078	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159	133, 134, 158	expp1zd 13515	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160	142	oveq1d 7150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
161		mul2neg 11068	. . . . . . . . . . . . . . . . . . 19 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
162	138, 55, 161	sylancl 589	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
163	138	mulid1d 10647	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
164	162, 163	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
165	159, 160, 164	3eqtrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
166	165	oveq1d 7150	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167	157, 166	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168	137, 95	remulcld 10660	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169	167, 168	eqeltrd 2890	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170	169	recnd 10658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171	124, 151, 170	addassd 10652	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172	122, 123, 171	3eqtr3d 2841	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173	172	oveq2d 7151	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174	102	recnd 10658	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
175	150, 169	readdcld 10659	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176	175	recnd 10658	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177	174, 124, 176	adddid 10654	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178	174, 151, 170	adddid 10654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179	147	oveq2d 7151	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180	148	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181	174, 138, 180	mulassd 10653	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182	179, 181	eqtr4d 2836	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
183	83, 63, 66	adddid 10654	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184	63	2timesd 11868	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185	184	oveq1d 7150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
186	63, 63, 68	addassd 10652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187	183, 185, 186	3eqtrrd 2838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188	187	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
189		expaddz 13469	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
190	133, 134, 62, 79, 189	syl22anc 837	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
191		2z 12002	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℤ
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193		nn0z 11993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
194		zaddcl 12010	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
195	31, 193, 194	syl2an 598	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196		expmulz 13471	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
197	133, 134, 192, 195, 196	syl22anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
198		neg1sqe1 13555	. . . . . . . . . . . . . . . . . 18 ⊢ (-1↑2) = 1
199	198	oveq1i 7145	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200		1exp 13454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201	195, 200	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202	199, 201	syl5eq 2845	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
203	197, 202	eqtrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
204	188, 190, 203	3eqtr3d 2841	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
205	204	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206	180	mulid2d 10648	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207	182, 205, 206	3eqtrd 2837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208	167	oveq2d 7151	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
209	95	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210	174, 138, 209	mulassd 10653	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211	208, 210	eqtr4d 2836	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212	204	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213	209	mulid2d 10648	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214	211, 212, 213	3eqtrd 2837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215	207, 214	oveq12d 7153	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216	144	negcld 10973	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217	216, 209	addcomd 10831	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218	209, 144	negsubd 10992	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219	217, 218	eqtrd 2833	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220	178, 215, 219	3eqtrd 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221	220	oveq2d 7151	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222	173, 177, 221	3eqtrrd 2838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223	106	recnd 10658	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224	223	addid1d 10829	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225	116, 222, 224	3brtr3d 5061	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226	103, 93	ffvelrnd 6829	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227	102, 226	remulcld 10660	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
228	51	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229		letr 10723	. . . . . . . 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 1368	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
231	225, 230	mpand 694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
232	231	expcom 417	. . . . 5 ⊢ (𝑛 ∈ ℕ0 → ((𝜑 ∧ 𝑁 ∈ 𝑍) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
233	232	a2d 29	. . . 4 ⊢ (𝑛 ∈ ℕ0 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
234	8, 14, 20, 26, 53, 233	nn0ind 12065	. . 3 ⊢ (𝐾 ∈ ℕ0 → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
235	234	com12 32	. 2 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
236	235	3impia 1114	1 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106   ⊆ wss 3881   class class class wbr 5030  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   ≤ cle 10665   − cmin 10859  -cneg 10860  2c2 11680  ℕ₀cn0 11885  ℤcz 11969  ℤ_≥cuz 12231  seqcseq 13364  ↑cexp 13425   ⇝ cli 14833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-seq 13365  df-exp 13426

This theorem is referenced by:  iseraltlem3  15032