Theorem iseraltlem2 15041

Description: Lemma for iseralt 15043. 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 7166	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2		2t0e0 11809	. . . . . . . . . 10 ⊢ (2 · 0) = 0
3	1, 2	syl6eq 2874	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
4	3	oveq2d 7174	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
5	4	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
6	5	oveq2d 7174	. . . . . 6 ⊢ (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
7	6	breq1d 5078	. . . . 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 7166	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
10	9	oveq2d 7174	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
11	10	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
12	11	oveq2d 7174	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
13	12	breq1d 5078	. . . . 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 7166	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
16	15	oveq2d 7174	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
17	16	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
18	17	oveq2d 7174	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
19	18	breq1d 5078	. . . . 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 7166	. . . . . . . . 9 ⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
22	21	oveq2d 7174	. . . . . . . 8 ⊢ (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
23	22	fveq2d 6676	. . . . . . 7 ⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
24	23	oveq2d 7174	. . . . . 6 ⊢ (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
25	24	breq1d 5078	. . . . 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 12267	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
29	27, 28	eqsstri 4003	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ ℤ
30	29	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℤ)
31	30	sselda 3969	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℤ)
32	31	zcnd 12091	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℂ)
33	32	addid1d 10842	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝑁 + 0) = 𝑁)
34	33	fveq2d 6676	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
35	34	oveq2d 7174	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36		neg1rr 11755	. . . . . . . 8 ⊢ -1 ∈ ℝ
37		neg1ne0 11756	. . . . . . . 8 ⊢ -1 ≠ 0
38		reexpclz 13452	. . . . . . . 8 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈ ℝ)
39	36, 37, 31, 38	mp3an12i 1461	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (-1↑𝑁) ∈ ℝ)
40		iseralt.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41		iseralt.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
42	30	sselda 3969	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
43		reexpclz 13452	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈ ℝ)
44	36, 37, 42, 43	mp3an12i 1461	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ)
45		iseralt.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
46	45	ffvelrnda 6853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)
47	44, 46	remulcld 10673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ)
48	41, 47	eqeltrd 2915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
49	27, 40, 48	serfre 13402	. . . . . . . 8 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
50	49	ffvelrnda 6853	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
51	39, 50	remulcld 10673	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
52	51	leidd 11208	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
53	35, 52	eqbrtrd 5090	. . . 4 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
54	45	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55		ax-1cn 10597	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
56	55	2timesi 11778	. . . . . . . . . . . . . . 15 ⊢ (2 · 1) = (1 + 1)
57	56	oveq2i 7169	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58		simpr 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ 𝑍)
59	58, 27	eleqtrdi 2925	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ (ℤ≥‘𝑀))
60	59	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ≥‘𝑀))
61		eluzelz 12256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
62	60, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
63	62	zcnd 12091	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64		2cn 11715	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
65		nn0cn 11910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ)
66	65	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67		mulcl 10623	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
68	64, 66, 67	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
69	64, 55	mulcli 10650	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
71	63, 68, 70	addassd 10665	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
72	57, 71	syl5eqr 2872	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73		2nn0 11917	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
74		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75		nn0mulcl 11936	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
76	73, 74, 75	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77		uzaddcl 12307	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
78	60, 76, 77	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
79	28, 78	sseldi 3967	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
80	79	zcnd 12091	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81		1cnd 10638	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
82	80, 81, 81	addassd 10665	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83		2cnd 11718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
84	83, 66, 81	adddid 10667	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
85	84	oveq2d 7174	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
86	72, 82, 85	3eqtr4d 2868	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87		peano2nn0 11940	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
88	87	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89		nn0mulcl 11936	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
90	73, 88, 89	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91		uzaddcl 12307	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
92	60, 90, 91	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
93	92, 27	eleqtrrdi 2926	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
94	86, 93	eqeltrd 2915	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
95	54, 94	ffvelrnd 6854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96		peano2uz 12304	. . . . . . . . . . . . 13 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
97	78, 96	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
98	97, 27	eleqtrrdi 2926	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
99	54, 98	ffvelrnd 6854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
100	95, 99	resubcld 11070	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101		0red 10646	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
102	39	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
103	49	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
104	78, 27	eleqtrrdi 2926	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105	103, 104	ffvelrnd 6854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106	102, 105	remulcld 10673	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107		fvoveq1 7181	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109	107, 108	breq12d 5081	. . . . . . . . . . 11 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110		iseralt.4	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
111	110	ralrimiva 3184	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
112	111	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
113	109, 112, 98	rspcdva 3627	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
114	95, 99	suble0d 11233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
115	113, 114	mpbird 259	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0)
116	100, 101, 106, 115	leadd2dd 11257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117		seqp1 13387	. . . . . . . . . . . . 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 13387	. . . . . . . . . . . . . 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 7173	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122	118, 121	eqtrd 2858	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
123	86	fveq2d 6676	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124	105	recnd 10671	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126		oveq2 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1)))
127	126, 108	oveq12d 7176	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128	125, 127	eqeq12d 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
129	41	ralrimiva 3184	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
130	129	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
131	128, 130, 98	rspcdva 3627	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132		neg1cn 11754	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
133	132	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
134	37	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135	133, 134, 79	expp1zd 13522	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -1))
136	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137	136, 134, 79	reexpclzd 13613	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138	137	recnd 10671	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139		mulcom 10625	. . . . . . . . . . . . . . . . . 18 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
140	138, 132, 139	sylancl 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 · (-1↑(𝑁 + (2 · 𝑛)))))
141	138	mulm1d 11094	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1 · (-1↑(𝑁 + (2 · 𝑛)))) = -(-1↑(𝑁 + (2 · 𝑛))))
142	135, 140, 141	3eqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝑛)) + 1)) = -(-1↑(𝑁 + (2 · 𝑛))))
143	142	oveq1d 7173	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
144	99	recnd 10671	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145		mulneg12 11080	. . . . . . . . . . . . . . . 16 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
146	138, 144, 145	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
147	131, 143, 146	3eqtrd 2862	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
148	99	renegcld 11069	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149	137, 148	remulcld 10673	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150	147, 149	eqeltrd 2915	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151	150	recnd 10671	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹‘𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153		oveq2 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154		fveq2 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺‘𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155	153, 154	oveq12d 7176	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156	152, 155	eqeq12d 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157	156, 130, 94	rspcdva 3627	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
158	79	peano2zd 12093	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159	133, 134, 158	expp1zd 13522	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160	142	oveq1d 7173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = (-(-1↑(𝑁 + (2 · 𝑛))) · -1))
161		mul2neg 11081	. . . . . . . . . . . . . . . . . . 19 ⊢ (((-1↑(𝑁 + (2 · 𝑛))) ∈ ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
162	138, 55, 161	sylancl 588	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) · 1))
163	138	mulid1d 10660	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · 1) = (-1↑(𝑁 + (2 · 𝑛))))
164	162, 163	eqtrd 2858	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1↑(𝑁 + (2 · 𝑛))))
165	159, 160, 164	3eqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (-1↑(𝑁 + (2 · 𝑛))))
166	165	oveq1d 7173	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167	157, 166	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168	137, 95	remulcld 10673	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169	167, 168	eqeltrd 2915	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170	169	recnd 10671	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171	124, 151, 170	addassd 10665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172	122, 123, 171	3eqtr3d 2866	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173	172	oveq2d 7174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174	102	recnd 10671	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
175	150, 169	readdcld 10672	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176	175	recnd 10671	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177	174, 124, 176	adddid 10667	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178	174, 151, 170	adddid 10667	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179	147	oveq2d 7174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180	148	recnd 10671	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181	174, 138, 180	mulassd 10666	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182	179, 181	eqtr4d 2861	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
183	83, 63, 66	adddid 10667	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184	63	2timesd 11883	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185	184	oveq1d 7173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
186	63, 63, 68	addassd 10665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187	183, 185, 186	3eqtrrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188	187	oveq2d 7174	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 · (𝑁 + 𝑛))))
189		expaddz 13476	. . . . . . . . . . . . . . . 16 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
190	133, 134, 62, 79, 189	syl22anc 836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))))
191		2z 12017	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℤ
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193		nn0z 12008	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
194		zaddcl 12025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
195	31, 193, 194	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196		expmulz 13478	. . . . . . . . . . . . . . . . 17 ⊢ (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
197	133, 134, 192, 195, 196	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛)))
198		neg1sqe1 13562	. . . . . . . . . . . . . . . . . 18 ⊢ (-1↑2) = 1
199	198	oveq1i 7168	. . . . . . . . . . . . . . . . 17 ⊢ ((-1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200		1exp 13461	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201	195, 200	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202	199, 201	syl5eq 2870	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑2)↑(𝑁 + 𝑛)) = 1)
203	197, 202	eqtrd 2858	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1↑(2 · (𝑁 + 𝑛))) = 1)
204	188, 190, 203	3eqtr3d 2866	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) = 1)
205	204	oveq1d 7173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206	180	mulid2d 10661	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207	182, 205, 206	3eqtrd 2862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208	167	oveq2d 7174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
209	95	recnd 10671	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210	174, 138, 209	mulassd 10666	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211	208, 210	eqtr4d 2861	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212	204	oveq1d 7173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213	209	mulid2d 10661	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214	211, 212, 213	3eqtrd 2862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215	207, 214	oveq12d 7176	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216	144	negcld 10986	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217	216, 209	addcomd 10844	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218	209, 144	negsubd 11005	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219	217, 218	eqtrd 2858	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220	178, 215, 219	3eqtrd 2862	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221	220	oveq2d 7174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222	173, 177, 221	3eqtrrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223	106	recnd 10671	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224	223	addid1d 10842	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225	116, 222, 224	3brtr3d 5099	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226	103, 93	ffvelrnd 6854	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227	102, 226	remulcld 10673	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
228	51	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229		letr 10736	. . . . . . . 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 1367	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
231	225, 230	mpand 693	. . . . . 6 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
232	231	expcom 416	. . . . 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 12080	. . 3 ⊢ (𝐾 ∈ ℕ0 → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
235	234	com12 32	. 2 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝐾 ∈ ℕ0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
236	235	3impia 1113	1 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140   ⊆ wss 3938   class class class wbr 5068  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  ℂcc 10537  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544   ≤ cle 10678   − cmin 10872  -cneg 10873  2c2 11695  ℕ₀cn0 11900  ℤcz 11984  ℤ_≥cuz 12246  seqcseq 13372  ↑cexp 13432   ⇝ cli 14843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-n0 11901  df-z 11985  df-uz 12247  df-fz 12896  df-seq 13373  df-exp 13433

This theorem is referenced by:  iseraltlem3  15042