Theorem iseraltlem2 15855

Description: Lemma for iseralt 15857. 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 7428	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (2 · 𝑥) = (2 · 0))
2		2t0e0 12516	. . . . . . . . . 10 ⊢ (2 · 0) = 0
3	1, 2	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑥 = 0 → (2 · 𝑥) = 0)
4	3	oveq2d 7436	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0))
5	4	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0)))
6	5	oveq2d 7436	. . . . . 6 ⊢ (𝑥 = 0 → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))))
7	6	breq1d 5112	. . . . 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 7428	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛))
10	9	oveq2d 7436	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛)))
11	10	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))
12	11	oveq2d 7436	. . . . . 6 ⊢ (𝑥 = 𝑛 → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
13	12	breq1d 5112	. . . . 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 7428	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1)))
16	15	oveq2d 7436	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1))))
17	16	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
18	17	oveq2d 7436	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
19	18	breq1d 5112	. . . . 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 7428	. . . . . . . . 9 ⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
22	21	oveq2d 7436	. . . . . . . 8 ⊢ (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾)))
23	22	fveq2d 6889	. . . . . . 7 ⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))
24	23	oveq2d 7436	. . . . . 6 ⊢ (𝑥 = 𝐾 → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
25	24	breq1d 5112	. . . . 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 12989	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
29	27, 28	eqsstri 3954	. . . . . . . . . . 11 ⊢ 𝑍 ⊆ ℤ
30	29	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ⊆ ℤ)
31	30	sselda 3908	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℤ)
32	31	zcnd 12807	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℂ)
33	32	addridd 11513	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝑁 + 0) = 𝑁)
34	33	fveq2d 6889	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁))
35	34	oveq2d 7436	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
36		neg1rr 12309	. . . . . . . 8 ⊢ -1 ∈ ℝ
37		neg1ne0 12310	. . . . . . . 8 ⊢ -1 ≠ 0
38		reexpclz 14228	. . . . . . . 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 3908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
43		reexpclz 14228	. . . . . . . . . . . 12 ⊢ (( -1 ∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → ( -1↑𝑘) ∈ ℝ)
44	36, 37, 42, 43	mp3an12i 1494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ( -1↑𝑘) ∈ ℝ)
45		iseralt.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
46	45	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)
47	44, 46	remulcld 11342	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (( -1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ)
48	41, 47	eqeltrd 2860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
49	27, 40, 48	serfre 14177	. . . . . . . 8 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
50	49	ffvelcdmda 7084	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
51	39, 50	remulcld 11342	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
52	51	leidd 11885	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
53	35, 52	eqbrtrd 5126	. . . 4 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
54	45	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
55		ax-1cn 11261	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
56	55	2timesi 12483	. . . . . . . . . . . . . . 15 ⊢ (2 · 1) = (1 + 1)
57	56	oveq2i 7431	. . . . . . . . . . . . . 14 ⊢ ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1))
58		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ 𝑍)
59	58, 27	eleqtrdi 2870	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ (ℤ≥‘𝑀))
60	59	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ (ℤ≥‘𝑀))
61		eluzelz 12978	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
62	60, 61	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℤ)
63	62	zcnd 12807	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ ℂ)
64		2cn 12421	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
65		nn0cn 12619	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ)
66	65	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℂ)
67		mulcl 11287	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
68	64, 66, 67	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℂ)
69	64, 55	mulcli 11319	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) ∈ ℂ
70	69	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 1) ∈ ℂ)
71	63, 68, 70	addassd 11334	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
72	57, 71	eqtr3id 2809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
73		2nn0 12626	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
74		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
75		nn0mulcl 12645	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
76	73, 74, 75	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
77		uzaddcl 13034	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
78	60, 76, 77	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀))
79	28, 78	sselid 3906	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℤ)
80	79	zcnd 12807	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ ℂ)
81		1cnd 11305	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈ ℂ)
82	80, 81, 81	addassd 11334	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1)))
83		2cnd 12424	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℂ)
84	83, 66, 81	adddid 11336	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
85	84	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1))))
86	72, 82, 85	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1))))
87		peano2nn0 12649	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
88	87	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
89		nn0mulcl 12645	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
90	73, 88, 89	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑛 + 1)) ∈ ℕ0)
91		uzaddcl 13034	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
92	60, 90, 91	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ (ℤ≥‘𝑀))
93	92, 27	eleqtrrdi 2871	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍)
94	86, 93	eqeltrd 2860	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍)
95	54, 94	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
96		peano2uz 13031	. . . . . . . . . . . . 13 ⊢ ((𝑁 + (2 · 𝑛)) ∈ (ℤ≥‘𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
97	78, 96	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ (ℤ≥‘𝑀))
98	97, 27	eleqtrrdi 2871	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍)
99	54, 98	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
100	95, 99	resubcld 11747	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
101		0red 11314	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈ ℝ)
102	39	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑𝑁) ∈ ℝ)
103	49	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
104	78, 27	eleqtrrdi 2871	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍)
105	103, 104	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ)
106	102, 105	remulcld 11342	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ)
107		fvoveq1 7443	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
108		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
109	107, 108	breq12d 5115	. . . . . . . . . . 11 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
110		iseralt.4	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
111	110	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
112	111	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
113	109, 112, 98	rspcdva 3577	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
114	95, 99	suble0d 11910	. . . . . . . . . 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 11934	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0))
117		seqp1 14162	. . . . . . . . . . . . 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 14162	. . . . . . . . . . . . . 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 7435	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
122	118, 121	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
123	86	fveq2d 6889	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))
124	105	recnd 11340	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ)
125		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))
126		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ( -1↑𝑘) = ( -1↑((𝑁 + (2 · 𝑛)) + 1)))
127	126, 108	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (( -1↑𝑘) · (𝐺‘𝑘)) = (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
128	125, 127	eqeq12d 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹‘𝑘) = (( -1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
129	41	ralrimiva 3154	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = (( -1↑𝑘) · (𝐺‘𝑘)))
130	129	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = (( -1↑𝑘) · (𝐺‘𝑘)))
131	128, 130, 98	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
132		neg1cn 12308	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℂ
133	132	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℂ)
134	37	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠ 0)
135	133, 134, 79	expp1zd 14301	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑((𝑁 + (2 · 𝑛)) + 1)) = (( -1↑(𝑁 + (2 · 𝑛))) · -1))
136	36	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈ ℝ)
137	136, 134, 79	reexpclzd 14396	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(𝑁 + (2 · 𝑛))) ∈ ℝ)
138	137	recnd 11340	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(𝑁 + (2 · 𝑛))) ∈ ℂ)
139		mulcom 11289	. . . . . . . . . . . . . . . . . 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 11771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1 · ( -1↑(𝑁 + (2 · 𝑛)))) = -( -1↑(𝑁 + (2 · 𝑛))))
142	135, 140, 141	3eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑((𝑁 + (2 · 𝑛)) + 1)) = -( -1↑(𝑁 + (2 · 𝑛))))
143	142	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ( -( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
144	99	recnd 11340	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
145		mulneg12 11757	. . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = (( -1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
148	99	renegcld 11746	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
149	137, 148	remulcld 11342	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ)
150	147, 149	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ)
151	150	recnd 11340	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
152		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹‘𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
153		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ( -1↑𝑘) = ( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)))
154		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺‘𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
155	153, 154	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (( -1↑𝑘) · (𝐺‘𝑘)) = (( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
156	152, 155	eqeq12d 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹‘𝑘) = (( -1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
157	156, 130, 94	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
158	79	peano2zd 12809	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ ℤ)
159	133, 134, 158	expp1zd 14301	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · -1))
160	142	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑((𝑁 + (2 · 𝑛)) + 1)) · -1) = ( -( -1↑(𝑁 + (2 · 𝑛))) · -1))
161		mul2neg 11758	. . . . . . . . . . . . . . . . . . 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 11329	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑(𝑁 + (2 · 𝑛))) · 1) = ( -1↑(𝑁 + (2 · 𝑛))))
164	162, 163	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -( -1↑(𝑁 + (2 · 𝑛))) · -1) = ( -1↑(𝑁 + (2 · 𝑛))))
165	159, 160, 164	3eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ( -1↑(𝑁 + (2 · 𝑛))))
166	165	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
167	157, 166	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
168	137, 95	remulcld 11342	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
169	167, 168	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℝ)
170	169	recnd 11340	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
171	124, 151, 170	addassd 11334	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
172	122, 123, 171	3eqtr3d 2803	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
173	172	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = (( -1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
174	102	recnd 11340	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑𝑁) ∈ ℂ)
175	150, 169	readdcld 11341	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℝ)
176	175	recnd 11340	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈ ℂ)
177	174, 124, 176	adddid 11336	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + (( -1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))))
178	174, 151, 170	adddid 11336	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((( -1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (( -1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
179	147	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (( -1↑𝑁) · (( -1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
180	148	recnd 11340	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
181	174, 138, 180	mulassd 11335	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (( -1↑𝑁) · (( -1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
182	179, 181	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
183	83, 63, 66	adddid 11336	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛)))
184	63	2timesd 12592	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
185	184	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑁) + (2 · 𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛)))
186	63, 63, 68	addassd 11334	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛))))
187	183, 185, 186	3eqtrrd 2800	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛)))
188	187	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ( -1↑(2 · (𝑁 + 𝑛))))
189		expaddz 14252	. . . . . . . . . . . . . . . 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 12731	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℤ
192	191	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈ ℤ)
193		nn0z 12720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
194		zaddcl 12739	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ)
195	31, 193, 194	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ)
196		expmulz 14254	. . . . . . . . . . . . . . . . 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 14342	. . . . . . . . . . . . . . . . . 18 ⊢ ( -1↑2) = 1
199	198	oveq1i 7430	. . . . . . . . . . . . . . . . 17 ⊢ (( -1↑2)↑(𝑁 + 𝑛)) = (1↑(𝑁 + 𝑛))
200		1exp 14237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1)
201	195, 200	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1↑(𝑁 + 𝑛)) = 1)
202	199, 201	eqtrid 2807	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑2)↑(𝑁 + 𝑛)) = 1)
203	197, 202	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -1↑(2 · (𝑁 + 𝑛))) = 1)
204	188, 190, 203	3eqtr3d 2803	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) = 1)
205	204	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
206	180	mullidd 11330	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
207	182, 205, 206	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))
208	167	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (( -1↑𝑁) · (( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
209	95	recnd 11340	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈ ℂ)
210	174, 138, 209	mulassd 11335	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (( -1↑𝑁) · (( -1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))
211	208, 210	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
212	204	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · ( -1↑(𝑁 + (2 · 𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
213	209	mullidd 11330	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
214	211, 212, 213	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))
215	207, 214	oveq12d 7438	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (( -1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ( -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))
216	144	negcld 11659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ)
217	216, 209	addcomd 11515	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
218	209, 144	negsubd 11678	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
219	217, 218	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ( -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
220	178, 215, 219	3eqtrd 2799	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))
221	220	oveq2d 7436	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + (( -1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))))
222	173, 177, 221	3eqtrrd 2800	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))))
223	106	recnd 11340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ)
224	223	addridd 11513	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
225	116, 222, 224	3brtr3d 5135	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))))
226	103, 93	ffvelcdmd 7085	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ)
227	102, 226	remulcld 11342	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ)
228	51	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (( -1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
229		letr 11407	. . . . . . . 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 12797	. . 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 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076   ⊆ wss 3895   class class class wbr 5102  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  ℂcc 11201  ℝcr 11202  0cc0 11203  1c1 11204   + caddc 11206   · cmul 11208   ≤ cle 11347   − cmin 11544   -cneg 11545  2c2 12400  ℕ₀cn0 12609  ℤcz 12696  ℤ_≥cuz 12968  seqcseq 14147  ↑cexp 14207   ⇝ cli 15656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-div 11977  df-nn 12339  df-2 12408  df-n0 12610  df-z 12697  df-uz 12969  df-fz 13643  df-seq 14148  df-exp 14208

This theorem is used by:  iseraltlem3  15856