Theorem seq3split 9970

Description: Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.)

Hypotheses

Ref	Expression
seq3split.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
seq3split.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
seq3split.3	⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))
seq3split.4	⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾))
seq3split.5	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆)

Assertion

Ref	Expression
seq3split	⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐹   𝑥,𝐾,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝑁,𝑦,𝑧   𝑥, + ,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem seq3split

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		seq3split.3	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))
2		eluzfz2 9509	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁))
4		eleq1 2151	. . . . . 6 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁)))
5		fveq2 5320	. . . . . . 7 ⊢ (𝑥 = (𝑀 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑀 + 1)))
6		fveq2 5320	. . . . . . . 8 ⊢ (𝑥 = (𝑀 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))
7	6	oveq2d 5684	. . . . . . 7 ⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))
8	5, 7	eqeq12d 2103	. . . . . 6 ⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))
9	4, 8	imbi12d 233	. . . . 5 ⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))))
10	9	imbi2d 229	. . . 4 ⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))))
11		eleq1 2151	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁)))
12		fveq2 5320	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑛))
13		fveq2 5320	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑛))
14	13	oveq2d 5684	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))
15	12, 14	eqeq12d 2103	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))
16	11, 15	imbi12d 233	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))))
17	16	imbi2d 229	. . . 4 ⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))))
18		eleq1 2151	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)))
19		fveq2 5320	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑛 + 1)))
20		fveq2 5320	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))
21	20	oveq2d 5684	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))
22	19, 21	eqeq12d 2103	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))
23	18, 22	imbi12d 233	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))))
24	23	imbi2d 229	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))))
25		eleq1 2151	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁)))
26		fveq2 5320	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑁))
27		fveq2 5320	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑁))
28	27	oveq2d 5684	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))
29	26, 28	eqeq12d 2103	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))
30	25, 29	imbi12d 233	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))))
31	30	imbi2d 229	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))))
32		seq3split.4	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐾))
33		seq3split.5	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆)
34		seq3split.1	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
35	32, 33, 34	seq3p1 9947	. . . . . 6 ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1))))
36		eluzel2 9087	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ∈ ℤ)
37	1, 36	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝑀 + 1) ∈ ℤ)
38		simpl 108	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑)
39		eluzel2 9087	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ≥‘𝐾) → 𝐾 ∈ ℤ)
40	32, 39	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℤ)
41	40	adantr 271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝐾 ∈ ℤ)
42		eluzelz 9091	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
43	42	adantl 272	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
44	41	zred 8931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝐾 ∈ ℝ)
45		eluzelz 9091	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (ℤ≥‘𝐾) → 𝑀 ∈ ℤ)
46	32, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
47	46	zred 8931	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℝ)
48	47	adantr 271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℝ)
49	43	zred 8931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ℝ)
50		eluzle 9094	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑀)
51	32, 50	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≤ 𝑀)
52	51	adantr 271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝐾 ≤ 𝑀)
53		peano2re 7681	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
54	48, 53	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 + 1) ∈ ℝ)
55	48	lep1d 8455	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ≤ (𝑀 + 1))
56		eluzle 9094	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑥)
57	56	adantl 272	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 + 1) ≤ 𝑥)
58	48, 54, 49, 55, 57	letrd 7670	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ≤ 𝑥)
59	44, 48, 49, 52, 58	letrd 7670	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝐾 ≤ 𝑥)
60		eluz2 9088	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ≤ 𝑥))
61	41, 43, 59, 60	syl3anbrc 1128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ≥‘𝐾))
62	38, 61, 33	syl2anc 404	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
63	37, 62, 34	seq3-1 9940	. . . . . . 7 ⊢ (𝜑 → (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1)))
64	63	oveq2d 5684	. . . . . 6 ⊢ (𝜑 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1))))
65	35, 64	eqtr4d 2124	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))
66	65	a1i13 24	. . . 4 ⊢ ((𝑀 + 1) ∈ ℤ → (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))))
67		peano2fzr 9514	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
68	67	adantl 272	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
69	68	expr 368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁)))
70	69	imim1d 75	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))))
71		oveq1 5675	. . . . . 6 ⊢ ((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))))
72		simprl 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘(𝑀 + 1)))
73		peano2uz 9134	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ≥‘𝐾) → (𝑀 + 1) ∈ (ℤ≥‘𝐾))
74	32, 73	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ≥‘𝐾))
75	74	adantr 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈ (ℤ≥‘𝐾))
76		uztrn 9098	. . . . . . . . 9 ⊢ ((𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑀 + 1) ∈ (ℤ≥‘𝐾)) → 𝑛 ∈ (ℤ≥‘𝐾))
77	72, 75, 76	syl2anc 404	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘𝐾))
78	33	adantlr 462	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆)
79	34	adantlr 462	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
80	77, 78, 79	seq3p1 9947	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
81	62	adantlr 462	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
82	72, 81, 79	seq3p1 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
83	82	oveq2d 5684	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
84		simpl 108	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝜑)
85		eqid 2089	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝐾) = (ℤ≥‘𝐾)
86	85, 40, 33, 34	seqf 9943	. . . . . . . . . . 11 ⊢ (𝜑 → seq𝐾( + , 𝐹):(ℤ≥‘𝐾)⟶𝑆)
87	86, 32	ffvelrnd 5451	. . . . . . . . . 10 ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆)
88	87	adantr 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆)
89		eqid 2089	. . . . . . . . . . 11 ⊢ (ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(𝑀 + 1))
90	37	adantr 271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈ ℤ)
91	89, 90, 81, 79	seqf 9943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → seq(𝑀 + 1)( + , 𝐹):(ℤ≥‘(𝑀 + 1))⟶𝑆)
92	91, 72	ffvelrnd 5451	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆)
93		fveq2 5320	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1)))
94	93	eleq1d 2157	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆))
95	33	ralrimiva 2447	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝐾)(𝐹‘𝑥) ∈ 𝑆)
96	95	adantr 271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑥 ∈ (ℤ≥‘𝐾)(𝐹‘𝑥) ∈ 𝑆)
97		fzssuz 9542	. . . . . . . . . . . 12 ⊢ ((𝑀 + 1)...𝑁) ⊆ (ℤ≥‘(𝑀 + 1))
98		uzss 9102	. . . . . . . . . . . . 13 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝐾) → (ℤ≥‘(𝑀 + 1)) ⊆ (ℤ≥‘𝐾))
99	74, 98	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ≥‘(𝑀 + 1)) ⊆ (ℤ≥‘𝐾))
100	97, 99	syl5ss 3039	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (ℤ≥‘𝐾))
101		simpr 109	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))
102		ssel2 3023	. . . . . . . . . . 11 ⊢ ((((𝑀 + 1)...𝑁) ⊆ (ℤ≥‘𝐾) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ (ℤ≥‘𝐾))
103	100, 101, 102	syl2an 284	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (ℤ≥‘𝐾))
104	94, 96, 103	rspcdva 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆)
105		seq3split.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
106	105	caovassg 5819	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆 ∧ (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
107	84, 88, 92, 104, 106	syl13anc 1177	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
108	83, 107	eqtr4d 2124	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))))
109	80, 108	eqeq12d 2103	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) ↔ ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1)))))
110	71, 109	syl5ibr 155	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))
111	70, 110	animpimp2impd 527	. . . 4 ⊢ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))))
112	10, 17, 24, 31, 66, 111	uzind4 9139	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))))
113	1, 112	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))
114	3, 113	mpd 13	1 ⊢ (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 925   = wceq 1290   ∈ wcel 1439  ∀wral 2360   ⊆ wss 3002   class class class wbr 3853  ‘cfv 5030  (class class class)co 5668  ℝcr 7412  1c1 7414   + caddc 7416   ≤ cle 7586  ℤcz 8813  ℤ_≥cuz 9082  ...cfz 9487  seqcseq 9915

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3962  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-iinf 4418  ax-cnex 7499  ax-resscn 7500  ax-1cn 7501  ax-1re 7502  ax-icn 7503  ax-addcl 7504  ax-addrcl 7505  ax-mulcl 7506  ax-addcom 7508  ax-addass 7510  ax-distr 7512  ax-i2m1 7513  ax-0lt1 7514  ax-0id 7516  ax-rnegex 7517  ax-cnre 7519  ax-pre-ltirr 7520  ax-pre-ltwlin 7521  ax-pre-lttrn 7522  ax-pre-ltadd 7524

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-nel 2352  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2624  df-sbc 2844  df-csb 2937  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-iun 3740  df-br 3854  df-opab 3908  df-mpt 3909  df-tr 3945  df-id 4131  df-iord 4204  df-on 4206  df-ilim 4207  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-riota 5624  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-1st 5927  df-2nd 5928  df-recs 6086  df-frec 6172  df-pnf 7587  df-mnf 7588  df-xr 7589  df-ltxr 7590  df-le 7591  df-sub 7718  df-neg 7719  df-inn 8486  df-n0 8737  df-z 8814  df-uz 9083  df-fz 9488  df-iseq 9916  df-seq3 9917

This theorem is referenced by:  seq3-1p  9972  seq3f1olemqsumk  9991  seq3f1olemqsum  9992  clim2ser  10788  clim2ser2  10789  isumsplit  10948  cvgratnnlemseq  10983