iseralt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > iseralt		Structured version Visualization version GIF version

Theorem iseralt 14415

Description: The alternating series test. If 𝐺(𝑘) is a decreasing sequence that converges to 0, then Σ𝑘 ∈ 𝑍(-1↑𝑘) · 𝐺(𝑘) is a convergent series. (Note that the first term is positive if 𝑀 is even, and negative if 𝑀 is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -1 using isermulc2 14388.) (Contributed by Mario Carneiro, 7-Apr-2015.)

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

**Assertion**
Ref	Expression
iseralt	⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )

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

Proof of Theorem iseralt Dummy variables 𝑗 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseralt.1	. 2 ⊢ 𝑍 = (ℤ_≥‘𝑀)
2		seqex 12803	. . 3 ⊢ seq𝑀( + , 𝐹) ∈ V
3	2	a1i 11	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V)
4		iseralt.5	. . . 4 ⊢ (𝜑 → 𝐺 ⇝ 0)
5		iseralt.2	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
6		climrel 14223	. . . . . . 7 ⊢ Rel ⇝
7	6	brrelexi 5158	. . . . . 6 ⊢ (𝐺 ⇝ 0 → 𝐺 ∈ V)
8	4, 7	syl 17	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ V)
9		eqidd 2623	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = (𝐺‘𝑛))
10		iseralt.3	. . . . . . 7 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
11	10	ffvelrnda 6359	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ ℝ)
12	11	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ ℂ)
13	1, 5, 8, 9, 12	clim0c 14238	. . . 4 ⊢ (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥))
14	4, 13	mpbid 222	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥)
15		simpr 477	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍)
16	15, 1	syl6eleq 2711	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ_≥‘𝑀))
17		eluzelz 11697	. . . . . . . 8 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) → 𝑗 ∈ ℤ)
18		uzid 11702	. . . . . . . 8 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ_≥‘𝑗))
19	16, 17, 18	3syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ_≥‘𝑗))
20		peano2uz 11741	. . . . . . 7 ⊢ (𝑗 ∈ (ℤ_≥‘𝑗) → (𝑗 + 1) ∈ (ℤ_≥‘𝑗))
21		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1)))
22	21	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑛 = (𝑗 + 1) → (abs‘(𝐺‘𝑛)) = (abs‘(𝐺‘(𝑗 + 1))))
23	22	breq1d 4663	. . . . . . . 8 ⊢ (𝑛 = (𝑗 + 1) → ((abs‘(𝐺‘𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
24	23	rspcv 3305	. . . . . . 7 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘𝑗) → (∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
25	19, 20, 24	3syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → (∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥))
26		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (ℤ_≥‘𝑗) → 𝑛 ∈ ℤ)
27	26	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑛 ∈ ℤ)
28	27	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑛 ∈ ℂ)
29	17, 1	eleq2s 2719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ)
30	29	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ ℤ)
31	30	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ ℂ)
32	28, 31	subcld 10392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℂ)
33		2cnd 11093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 2 ∈ ℂ)
34		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 2 ≠ 0)
36	32, 33, 35	divcan2d 10803	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (2 · ((𝑛 − 𝑗) / 2)) = (𝑛 − 𝑗))
37	36	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑗 + (2 · ((𝑛 − 𝑗) / 2))) = (𝑗 + (𝑛 − 𝑗)))
38	31, 28	pncan3d 10395	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑗 + (𝑛 − 𝑗)) = 𝑛)
39	37, 38	eqtr2d 2657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛 − 𝑗) / 2))))
40	39	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛 − 𝑗) / 2))))
41	40	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))))
42	41	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗)))
43	42	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))))
44		simpll 790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝜑)
45		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗)) → 𝑗 ∈ 𝑍)
46	45	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝑗 ∈ 𝑍)
47		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → ((𝑛 − 𝑗) / 2) ∈ ℤ)
48	27, 30	zsubcld 11487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℤ)
49	48	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℝ)
50		eluzle 11700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘𝑗) → 𝑗 ≤ 𝑛)
51	50	ad2antll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑗 ≤ 𝑛)
52	27	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑛 ∈ ℝ)
53	30	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ ℝ)
54	52, 53	subge0d 10617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (0 ≤ (𝑛 − 𝑗) ↔ 𝑗 ≤ 𝑛))
55	51, 54	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 0 ≤ (𝑛 − 𝑗))
56		2re 11090	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 2 ∈ ℝ)
58		2pos 11112	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 2
59	58	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 0 < 2)
60		divge0 10892	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑛 − 𝑗) ∈ ℝ ∧ 0 ≤ (𝑛 − 𝑗)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑛 − 𝑗) / 2))
61	49, 55, 57, 59, 60	syl22anc 1327	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 0 ≤ ((𝑛 − 𝑗) / 2))
62	61	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛 − 𝑗) / 2))
63		elnn0z 11390	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 − 𝑗) / 2) ∈ ℕ₀ ↔ (((𝑛 − 𝑗) / 2) ∈ ℤ ∧ 0 ≤ ((𝑛 − 𝑗) / 2)))
64	47, 62, 63	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → ((𝑛 − 𝑗) / 2) ∈ ℕ₀)
65		iseralt.4	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘))
66		iseralt.6	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)))
67	1, 5, 10, 65, 4, 66	iseraltlem3 14414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((𝑛 − 𝑗) / 2) ∈ ℕ₀) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛 − 𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
68	67	simpld 475	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((𝑛 − 𝑗) / 2) ∈ ℕ₀) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
69	44, 46, 64, 68	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
70	43, 69	eqbrtrd 4675	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
71		2div2e1 11150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 / 2) = 1
72	71	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑛 − 𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛 − 𝑗) + 1) / 2) − 1)
73		peano2cn 10208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑛 − 𝑗) ∈ ℂ → ((𝑛 − 𝑗) + 1) ∈ ℂ)
74	32, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈ ℂ)
75	74, 33, 33, 35	divsubdird 10840	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) − 2) / 2) = ((((𝑛 − 𝑗) + 1) / 2) − (2 / 2)))
76		df-2 11079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 2 = (1 + 1)
77	76	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 − 𝑗) + 1) − 2) = (((𝑛 − 𝑗) + 1) − (1 + 1))
78		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ ℂ
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 1 ∈ ℂ)
80	32, 79, 79	pnpcan2d 10430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (((𝑛 − 𝑗) + 1) − (1 + 1)) = ((𝑛 − 𝑗) − 1))
81	77, 80	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (((𝑛 − 𝑗) + 1) − 2) = ((𝑛 − 𝑗) − 1))
82	81	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) − 2) / 2) = (((𝑛 − 𝑗) − 1) / 2))
83	75, 82	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) / 2) − (2 / 2)) = (((𝑛 − 𝑗) − 1) / 2))
84	72, 83	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) / 2) − 1) = (((𝑛 − 𝑗) − 1) / 2))
85	84	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)) = (2 · (((𝑛 − 𝑗) − 1) / 2)))
86		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 − 𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 𝑗) − 1) ∈ ℂ)
87	32, 78, 86	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 𝑗) − 1) ∈ ℂ)
88	87, 33, 35	divcan2d 10803	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (2 · (((𝑛 − 𝑗) − 1) / 2)) = ((𝑛 − 𝑗) − 1))
89	28, 31, 79	sub32d 10424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 𝑗) − 1) = ((𝑛 − 1) − 𝑗))
90	85, 88, 89	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗))
91	90	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗)))
92		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑛 − 1) ∈ ℂ)
93	28, 78, 92	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑛 − 1) ∈ ℂ)
94	31, 93	pncan3d 10395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1))
95	91, 94	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) = (𝑛 − 1))
96	95	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) + 1))
97		npcan 10290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
98	28, 78, 97	sylancl 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 1) + 1) = 𝑛)
99	96, 98	eqtr2d 2657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1))
100	99	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1))
101	100	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)))
102	101	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗)))
103	102	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))))
104		simpll 790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝜑)
105	45	ad2antlr 763	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝑗 ∈ 𝑍)
106		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ)
107		uznn0sub 11719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (ℤ_≥‘𝑗) → (𝑛 − 𝑗) ∈ ℕ₀)
108	107	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℕ₀)
109		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 − 𝑗) ∈ ℕ₀ → ((𝑛 − 𝑗) + 1) ∈ ℕ)
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈ ℕ)
111	110	nnrpd 11870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈ ℝ⁺)
112	111	rphalfcld 11884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (((𝑛 − 𝑗) + 1) / 2) ∈ ℝ⁺)
113	112	rpgt0d 11875	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 0 < (((𝑛 − 𝑗) + 1) / 2))
114	113	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 0 < (((𝑛 − 𝑗) + 1) / 2))
115		elnnz 11387	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℤ ∧ 0 < (((𝑛 − 𝑗) + 1) / 2)))
116	106, 114, 115	sylanbrc 698	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (((𝑛 − 𝑗) + 1) / 2) ∈ ℕ)
117		nnm1nn0 11334	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℕ → ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈ ℕ₀)
118	116, 117	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈ ℕ₀)
119	1, 5, 10, 65, 4, 66	iseraltlem3 14414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈ ℕ₀) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))))
120	119	simprd 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈ ℕ₀) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
121	104, 105, 118, 120	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
122	103, 121	eqbrtrd 4675	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
123		zeo 11463	. . . . . . . . . . . . . 14 ⊢ ((𝑛 − 𝑗) ∈ ℤ → (((𝑛 − 𝑗) / 2) ∈ ℤ ∨ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ))
124	48, 123	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (((𝑛 − 𝑗) / 2) ∈ ℤ ∨ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ))
125	70, 122, 124	mpjaodan 827	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))
126	1	peano2uzs 11742	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ 𝑍 → (𝑗 + 1) ∈ 𝑍)
127	126	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗)) → (𝑗 + 1) ∈ 𝑍)
128		ffvelrn 6357	. . . . . . . . . . . . . 14 ⊢ ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
129	10, 127, 128	syl2an 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ)
130	1, 5, 10, 65, 4	iseraltlem1 14412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1)))
131	127, 130	sylan2 491	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1)))
132	129, 131	absidd 14161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1)))
133	125, 132	breqtrrd 4681	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
134	133	adantlr 751	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))))
135		neg1rr 11125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 ∈ ℝ
136	135	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ∈ ℝ)
137		neg1ne0 11126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 ≠ 0
138	137	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ≠ 0)
139		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ (ℤ_≥‘𝑀) → 𝑘 ∈ ℤ)
140	139, 1	eleq2s 2719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ)
141	140	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ)
142	136, 138, 141	reexpclzd 13034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ)
143	10	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ)
144	142, 143	remulcld 10070	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ)
145	66, 144	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
146	1, 5, 145	serfre 12830	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
147	1	uztrn2 11705	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗)) → 𝑛 ∈ 𝑍)
148		ffvelrn 6357	. . . . . . . . . . . . . . . 16 ⊢ ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
149	146, 147, 148	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
150		ffvelrn 6357	. . . . . . . . . . . . . . . 16 ⊢ ((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
151	146, 45, 150	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
152	149, 151	resubcld 10458	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ)
153	152	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ)
154	153	abscld 14175	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
155	154	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ)
156	132, 129	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
157	156	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ)
158		rpre 11839	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
159	158	ad2antlr 763	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → 𝑥 ∈ ℝ)
160		lelttr 10128	. . . . . . . . . . 11 ⊢ (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
161	155, 157, 159, 160	syl3anc 1326	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
162	134, 161	mpand 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
163	146	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
164	163, 147, 148	syl2an 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
165	162, 164	jctild 566	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ_≥‘𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
166	165	anassrs 680	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ_≥‘𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
167	166	ralrimdva 2969	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ_≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
168	25, 167	syld 47	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → (∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ_≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
169	168	reximdva 3017	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
170	169	ralimdva 2962	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)))
171	14, 170	mpd 15	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ_≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))
172	1, 3, 171	caurcvg2 14408	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 class class class wbr 4653 dom cdm 5114 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 seqcseq 12801 ↑cexp 12860 abscabs 13974 ⇝ cli 14215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fl 12593 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220

This theorem is referenced by: leibpi 24669

W3C validator