iseqsplit - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > iseqsplit		GIF version

Theorem iseqsplit 9773

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

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

**Assertion**
Ref	Expression
iseqsplit	⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))

Distinct variable groups: 𝑥,𝑦,𝑧,𝐹 𝑥,𝐾,𝑦,𝑧 𝑥,𝑀,𝑦,𝑧 𝜑,𝑥,𝑦,𝑧 𝑥,𝑁,𝑦,𝑧 𝑥, + ,𝑦,𝑧 𝑥,𝑆,𝑦,𝑧 Allowed substitution hints: 𝑉(𝑥,𝑦,𝑧)

Proof of Theorem iseqsplit Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseqsplit.3	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
2		eluzfz2 9341	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁))
4		eleq1 2145	. . . . . 6 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁)))
5		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = (𝑀 + 1) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)))
6		fveq2 5253	. . . . . . . 8 ⊢ (𝑥 = (𝑀 + 1) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))
7	6	oveq2d 5607	. . . . . . 7 ⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))
8	5, 7	eqeq12d 2097	. . . . . 6 ⊢ (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))))
9	4, 8	imbi12d 232	. . . . 5 ⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))))
10	9	imbi2d 228	. . . 4 ⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)))))))
11		eleq1 2145	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁)))
12		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘𝑛))
13		fveq2 5253	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))
14	13	oveq2d 5607	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))
15	12, 14	eqeq12d 2097	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))))
16	11, 15	imbi12d 232	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))))
17	16	imbi2d 228	. . . 4 ⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))))))
18		eleq1 2145	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)))
19		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)))
20		fveq2 5253	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))
21	20	oveq2d 5607	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))
22	19, 21	eqeq12d 2097	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
23	18, 22	imbi12d 232	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
24	23	imbi2d 228	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))))
25		eleq1 2145	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁)))
26		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = (seq𝐾( + , 𝐹, 𝑆)‘𝑁))
27		fveq2 5253	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))
28	27	oveq2d 5607	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))
29	26, 28	eqeq12d 2097	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)) ↔ (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))))
30	25, 29	imbi12d 232	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))))
31	30	imbi2d 228	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑥) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑥)))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))))))
32		iseqsplit.4	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝐾))
33		iseqsplit.5	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆)
34		iseqsplit.1	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
35	32, 33, 34	iseqp1 9757	. . . . . 6 ⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (𝐹‘(𝑀 + 1))))
36		eluzel2 8919	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀 + 1) ∈ ℤ)
37	1, 36	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝑀 + 1) ∈ ℤ)
38		eluzelz 8923	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘𝐾) → 𝑀 ∈ ℤ)
39	32, 38	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
40		peano2uzr 8968	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘𝑀))
41	39, 40	sylan 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘𝑀))
42	32	adantr 270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ (ℤ_≥‘𝐾))
43		uztrn 8930	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (ℤ_≥‘𝑀) ∧ 𝑀 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝐾))
44	41, 42, 43	syl2anc 403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘𝐾))
45	44, 33	syldan 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
46	37, 45, 34	iseq1 9752	. . . . . . 7 ⊢ (𝜑 → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1)))
47	46	oveq2d 5607	. . . . . 6 ⊢ (𝜑 → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (𝐹‘(𝑀 + 1))))
48	35, 47	eqtr4d 2118	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))
49	48	a1i13 24	. . . 4 ⊢ ((𝑀 + 1) ∈ ℤ → (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑀 + 1))))))
50		peano2fzr 9346	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
51	50	adantl 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
52	51	expr 367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁)))
53	52	imim1d 74	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))))
54		oveq1 5598	. . . . . . . . . 10 ⊢ ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))))
55		simprl 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ_≥‘(𝑀 + 1)))
56		peano2uz 8966	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘𝐾) → (𝑀 + 1) ∈ (ℤ_≥‘𝐾))
57	32, 56	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘𝐾))
58	57	adantr 270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈ (ℤ_≥‘𝐾))
59		uztrn 8930	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑀 + 1) ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
60	55, 58, 59	syl2anc 403	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ_≥‘𝐾))
61	33	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (𝐹‘𝑥) ∈ 𝑆)
62	34	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
63	60, 61, 62	iseqp1 9757	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
64	45	adantlr 461	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝑆)
65	55, 64, 62	iseqp1 9757	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
66	65	oveq2d 5607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))))
67		simpl 107	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝜑)
68	32, 33, 34	iseqcl 9756	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆)
69	68	adantr 270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆)
70	55, 64, 62	iseqcl 9756	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆)
71		fveq2 5253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1)))
72	71	eleq1d 2151	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆))
73		elfzuz 9331	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ (ℤ_≥‘𝐾))
74	73, 33	sylan2 280	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹‘𝑥) ∈ 𝑆)
75	74	ralrimiva 2440	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆)
76	75	adantr 270	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑥 ∈ (𝐾...𝑁)(𝐹‘𝑥) ∈ 𝑆)
77		fzss1 9371	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘𝐾) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁))
78	32, 56, 77	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁))
79		simpr 108	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))
80		ssel2 3005	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ (𝐾...𝑁))
81	78, 79, 80	syl2an 283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝐾...𝑁))
82	72, 76, 81	rspcdva 2717	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆)
83		iseqsplit.2	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
84	83	caovassg 5738	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) ∈ 𝑆 ∧ (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) → (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))))
85	67, 69, 70, 82, 84	syl13anc 1172	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))))
86	66, 85	eqtr4d 2118	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1))))
87	63, 86	eqeq12d 2097	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))) ↔ ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) + (𝐹‘(𝑛 + 1)))))
88	54, 87	syl5ibr 154	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
89	88	expr 367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → ((seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
90	89	a2d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(𝑀 + 1))) → (((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
91	53, 90	syld 44	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
92	91	expcom 114	. . . . 5 ⊢ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝜑 → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))))
93	92	a2d 26	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑛) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑛)))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘(𝑛 + 1)))))))
94	10, 17, 24, 31, 49, 93	uzind4 8971	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))))
95	1, 94	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁))))
96	3, 95	mpd 13	1 ⊢ (𝜑 → (seq𝐾( + , 𝐹, 𝑆)‘𝑁) = ((seq𝐾( + , 𝐹, 𝑆)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹, 𝑆)‘𝑁)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 = wceq 1285 ∈ wcel 1434 ∀wral 2353 ⊆ wss 2984 ‘cfv 4969 (class class class)co 5591 1c1 7254 + caddc 7256 ℤcz 8646 ℤ_≥cuz 8914 ...cfz 9319 seqcseq 9740

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-coll 3919 ax-sep 3922 ax-nul 3930 ax-pow 3974 ax-pr 4000 ax-un 4224 ax-setind 4316 ax-iinf 4366 ax-cnex 7339 ax-resscn 7340 ax-1cn 7341 ax-1re 7342 ax-icn 7343 ax-addcl 7344 ax-addrcl 7345 ax-mulcl 7346 ax-addcom 7348 ax-addass 7350 ax-distr 7352 ax-i2m1 7353 ax-0lt1 7354 ax-0id 7356 ax-rnegex 7357 ax-cnre 7359 ax-pre-ltirr 7360 ax-pre-ltwlin 7361 ax-pre-lttrn 7362 ax-pre-ltadd 7364

This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-nel 2345 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2614 df-sbc 2827 df-csb 2920 df-dif 2986 df-un 2988 df-in 2990 df-ss 2997 df-nul 3270 df-pw 3408 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-int 3663 df-iun 3706 df-br 3812 df-opab 3866 df-mpt 3867 df-tr 3902 df-id 4084 df-iord 4157 df-on 4159 df-ilim 4160 df-suc 4162 df-iom 4369 df-xp 4407 df-rel 4408 df-cnv 4409 df-co 4410 df-dm 4411 df-rn 4412 df-res 4413 df-ima 4414 df-iota 4934 df-fun 4971 df-fn 4972 df-f 4973 df-f1 4974 df-fo 4975 df-f1o 4976 df-fv 4977 df-riota 5547 df-ov 5594 df-oprab 5595 df-mpt2 5596 df-1st 5846 df-2nd 5847 df-recs 6002 df-frec 6088 df-pnf 7427 df-mnf 7428 df-xr 7429 df-ltxr 7430 df-le 7431 df-sub 7558 df-neg 7559 df-inn 8317 df-n0 8566 df-z 8647 df-uz 8915 df-fz 9320 df-iseq 9741

This theorem is referenced by: iseq1p 9774 ibcval5 10006 clim2iser 10549 clim2iser2 10550

W3C validator