iseqid2 - Intuitionistic Logic Explorer

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

Theorem iseqid2 9783

Description: The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for +) are all the same. (Contributed by Jim Kingdon, 5-Mar-2022.)

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

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

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

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

Step	Hyp	Ref	Expression
1		iseqid2.3	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝐾))
2		eluzfz2 9341	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝐾) → 𝑁 ∈ (𝐾...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝐾...𝑁))
4		eleq1 2145	. . . . . 6 ⊢ (𝑥 = 𝐾 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝐾 ∈ (𝐾...𝑁)))
5		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹, 𝑆)‘𝑥) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))
6	5	eqeq2d 2094	. . . . . 6 ⊢ (𝑥 = 𝐾 → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾)))
7	4, 6	imbi12d 232	. . . . 5 ⊢ (𝑥 = 𝐾 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥)) ↔ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))))
8	7	imbi2d 228	. . . 4 ⊢ (𝑥 = 𝐾 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾)))))
9		eleq1 2145	. . . . . 6 ⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑛 ∈ (𝐾...𝑁)))
10		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹, 𝑆)‘𝑥) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))
11	10	eqeq2d 2094	. . . . . 6 ⊢ (𝑥 = 𝑛 → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)))
12	9, 11	imbi12d 232	. . . . 5 ⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥)) ↔ (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))))
13	12	imbi2d 228	. . . 4 ⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)))))
14		eleq1 2145	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝐾...𝑁) ↔ (𝑛 + 1) ∈ (𝐾...𝑁)))
15		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑥) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))
16	15	eqeq2d 2094	. . . . . 6 ⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))))
17	14, 16	imbi12d 232	. . . . 5 ⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
18	17	imbi2d 228	. . . 4 ⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
19		eleq1 2145	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝐾...𝑁) ↔ 𝑁 ∈ (𝐾...𝑁)))
20		fveq2 5253	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘𝑥) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))
21	20	eqeq2d 2094	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)))
22	19, 21	imbi12d 232	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥)) ↔ (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))))
23	22	imbi2d 228	. . . 4 ⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)))))
24		eqidd 2084	. . . . 5 ⊢ (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))
25	24	2a1i 27	. . . 4 ⊢ (𝐾 ∈ ℤ → (𝜑 → (𝐾 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))))
26		peano2fzr 9346	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁)) → 𝑛 ∈ (𝐾...𝑁))
27	26	adantl 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (𝐾...𝑁))
28	27	expr 367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑛 ∈ (𝐾...𝑁)))
29	28	imim1d 74	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))))
30		oveq1 5598	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
31		fveq2 5253	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1)))
32	31	eqeq1d 2091	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑥) = 𝑍 ↔ (𝐹‘(𝑛 + 1)) = 𝑍))
33		iseqid2.5	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = 𝑍)
34	33	ralrimiva 2440	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑥) = 𝑍)
35	34	adantr 270	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)(𝐹‘𝑥) = 𝑍)
36		eluzp1p1 8939	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) → (𝑛 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
37	36	ad2antrl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
38		elfzuz3 9332	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 + 1) ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ_≥‘(𝑛 + 1)))
39	38	ad2antll 475	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑁 ∈ (ℤ_≥‘(𝑛 + 1)))
40		elfzuzb 9329	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 + 1) ∈ ((𝐾 + 1)...𝑁) ↔ ((𝑛 + 1) ∈ (ℤ_≥‘(𝐾 + 1)) ∧ 𝑁 ∈ (ℤ_≥‘(𝑛 + 1))))
41	37, 39, 40	sylanbrc 408	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝑛 + 1) ∈ ((𝐾 + 1)...𝑁))
42	32, 35, 41	rspcdva 2717	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (𝐹‘(𝑛 + 1)) = 𝑍)
43	42	oveq2d 5607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + 𝑍))
44		oveq1 5598	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝐾) → (𝑥 + 𝑍) = ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + 𝑍))
45		id 19	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝐾) → 𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))
46	44, 45	eqeq12d 2097	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq𝑀( + , 𝐹, 𝑆)‘𝐾) → ((𝑥 + 𝑍) = 𝑥 ↔ ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾)))
47		iseqid2.1	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑥)
48	47	ralrimiva 2440	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (𝑥 + 𝑍) = 𝑥)
49		iseqid2.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) ∈ 𝑆)
50	46, 48, 49	rspcdva 2717	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))
51	50	adantr 270	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + 𝑍) = (seq𝑀( + , 𝐹, 𝑆)‘𝐾))
52	43, 51	eqtr2d 2116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + (𝐹‘(𝑛 + 1))))
53		simprl 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ_≥‘𝐾))
54		iseqid2.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘𝑀))
55	54	adantr 270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝐾 ∈ (ℤ_≥‘𝑀))
56		uztrn 8930	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑛 ∈ (ℤ_≥‘𝑀))
57	53, 55, 56	syl2anc 403	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → 𝑛 ∈ (ℤ_≥‘𝑀))
58		iseqid2.f	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
59	58	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
60		iseqid2.cl	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
61	60	adantlr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
62	57, 59, 61	iseqp1 9757	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
63	52, 62	eqeq12d 2097	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) ↔ ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) + (𝐹‘(𝑛 + 1))) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))))
64	30, 63	syl5ibr 154	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝐾) ∧ (𝑛 + 1) ∈ (𝐾...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))))
65	64	expr 367	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → ((seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
66	65	a2d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
67	29, 66	syld 44	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))))
68	67	expcom 114	. . . . 5 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) → (𝜑 → ((𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛)) → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
69	68	a2d 26	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) → ((𝜑 → (𝑛 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))))))
70	8, 13, 18, 23, 25, 69	uzind4 8971	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝐾) → (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))))
71	1, 70	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ (𝐾...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁)))
72	3, 71	mpd 13	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝐾) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 102 = wceq 1285 ∈ wcel 1434 ∀wral 2353 ‘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: fisumcvg 10574

W3C validator