iseqshft2 - Intuitionistic Logic Explorer

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

Theorem iseqshft2 9961

Description: Shifting the index set of a sequence.

New proofs should use seq3shft2 9962 instead (together with iseqsst 9949 or iseqseq3 9965 if need be).

(Contributed by Jim Kingdon, 15-Aug-2021.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
iseqshft2.1	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
iseqshft2.2	⊢ (𝜑 → 𝐾 ∈ ℤ)
iseqshft2.3	⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)))
iseqshft2.f	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
iseqshft2.g	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 𝐾))) → (𝐺‘𝑥) ∈ 𝑆)
iseqshft2.pl	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)

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

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

Proof of Theorem iseqshft2 Dummy variables 𝑛 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseqshft2.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
2		eluzfz2 9509	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		eleq1 2151	. . . . . 6 ⊢ (𝑤 = 𝑀 → (𝑤 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁)))
5		fveq2 5320	. . . . . . 7 ⊢ (𝑤 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑀))
6		oveq1 5675	. . . . . . . 8 ⊢ (𝑤 = 𝑀 → (𝑤 + 𝐾) = (𝑀 + 𝐾))
7	6	fveq2d 5324	. . . . . . 7 ⊢ (𝑤 = 𝑀 → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾)))
8	5, 7	eqeq12d 2103	. . . . . 6 ⊢ (𝑤 = 𝑀 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾))))
9	4, 8	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑀 → ((𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾))) ↔ (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾)))))
10	9	imbi2d 229	. . . 4 ⊢ (𝑤 = 𝑀 → ((𝜑 → (𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾))))))
11		eleq1 2151	. . . . . 6 ⊢ (𝑤 = 𝑛 → (𝑤 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁)))
12		fveq2 5320	. . . . . . 7 ⊢ (𝑤 = 𝑛 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))
13		oveq1 5675	. . . . . . . 8 ⊢ (𝑤 = 𝑛 → (𝑤 + 𝐾) = (𝑛 + 𝐾))
14	13	fveq2d 5324	. . . . . . 7 ⊢ (𝑤 = 𝑛 → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)))
15	12, 14	eqeq12d 2103	. . . . . 6 ⊢ (𝑤 = 𝑛 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))))
16	11, 15	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑛 → ((𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾))) ↔ (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)))))
17	16	imbi2d 229	. . . 4 ⊢ (𝑤 = 𝑛 → ((𝜑 → (𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))))))
18		eleq1 2151	. . . . . 6 ⊢ (𝑤 = (𝑛 + 1) → (𝑤 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁)))
19		fveq2 5320	. . . . . . 7 ⊢ (𝑤 = (𝑛 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))
20		oveq1 5675	. . . . . . . 8 ⊢ (𝑤 = (𝑛 + 1) → (𝑤 + 𝐾) = ((𝑛 + 1) + 𝐾))
21	20	fveq2d 5324	. . . . . . 7 ⊢ (𝑤 = (𝑛 + 1) → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)))
22	19, 21	eqeq12d 2103	. . . . . 6 ⊢ (𝑤 = (𝑛 + 1) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) ↔ (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾))))
23	18, 22	imbi12d 233	. . . . 5 ⊢ (𝑤 = (𝑛 + 1) → ((𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾))) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)))))
24	23	imbi2d 229	. . . 4 ⊢ (𝑤 = (𝑛 + 1) → ((𝜑 → (𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾))))))
25		eleq1 2151	. . . . . 6 ⊢ (𝑤 = 𝑁 → (𝑤 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
26		fveq2 5320	. . . . . . 7 ⊢ (𝑤 = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))
27		oveq1 5675	. . . . . . . 8 ⊢ (𝑤 = 𝑁 → (𝑤 + 𝐾) = (𝑁 + 𝐾))
28	27	fveq2d 5324	. . . . . . 7 ⊢ (𝑤 = 𝑁 → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾)))
29	26, 28	eqeq12d 2103	. . . . . 6 ⊢ (𝑤 = 𝑁 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)) ↔ (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾))))
30	25, 29	imbi12d 233	. . . . 5 ⊢ (𝑤 = 𝑁 → ((𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾))) ↔ (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾)))))
31	30	imbi2d 229	. . . 4 ⊢ (𝑤 = 𝑁 → ((𝜑 → (𝑤 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑤) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑤 + 𝐾)))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾))))))
32		fveq2 5320	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀))
33		oveq1 5675	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (𝑘 + 𝐾) = (𝑀 + 𝐾))
34	33	fveq2d 5324	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐺‘(𝑘 + 𝐾)) = (𝐺‘(𝑀 + 𝐾)))
35	32, 34	eqeq12d 2103	. . . . . . 7 ⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)) ↔ (𝐹‘𝑀) = (𝐺‘(𝑀 + 𝐾))))
36		iseqshft2.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)))
37	36	ralrimiva 2447	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)))
38		eluzfz1 9508	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
39	1, 38	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁))
40	35, 37, 39	rspcdva 2730	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑀) = (𝐺‘(𝑀 + 𝐾)))
41		eluzel2 9087	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
42	1, 41	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
43		iseqshft2.f	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
44		iseqshft2.pl	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
45	42, 43, 44	iseq1 9938	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀))
46		iseqshft2.2	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
47	42, 46	zaddcld 8935	. . . . . . 7 ⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ)
48		iseqshft2.g	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 𝐾))) → (𝐺‘𝑥) ∈ 𝑆)
49	47, 48, 44	iseq1 9938	. . . . . 6 ⊢ (𝜑 → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾)) = (𝐺‘(𝑀 + 𝐾)))
50	40, 45, 49	3eqtr4d 2131	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾)))
51	50	a1i13 24	. . . 4 ⊢ (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑀 + 𝐾)))))
52		peano2fzr 9514	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁))
53	52	adantl 272	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...𝑁))
54	53	expr 368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁)))
55	54	imim1d 75	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)))))
56		oveq1 5675	. . . . . . . . . 10 ⊢ ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1))))
57		simprl 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (ℤ_≥‘𝑀))
58	43	adantlr 462	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
59	44	adantlr 462	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
60	57, 58, 59	iseqp1 9945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
61	46	adantr 271	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝐾 ∈ ℤ)
62		eluzadd 9110	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑛 + 𝐾) ∈ (ℤ_≥‘(𝑀 + 𝐾)))
63	57, 61, 62	syl2anc 404	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 𝐾) ∈ (ℤ_≥‘(𝑀 + 𝐾)))
64	48	adantlr 462	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 𝐾))) → (𝐺‘𝑥) ∈ 𝑆)
65	63, 64, 59	iseqp1 9945	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 𝐾) + 1)) = ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐺‘((𝑛 + 𝐾) + 1))))
66		eluzelz 9091	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
67	57, 66	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ ℤ)
68		zcn 8818	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
69		zcn 8818	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
70		ax-1cn 7501	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
71		add32 7704	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1))
72	70, 71	mp3an2 1262	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1))
73	68, 69, 72	syl2an 284	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1))
74	67, 61, 73	syl2anc 404	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝑛 + 1) + 𝐾) = ((𝑛 + 𝐾) + 1))
75	74	fveq2d 5324	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 𝐾) + 1)))
76		fveq2 5320	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
77		oveq1 5675	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑛 + 1) → (𝑘 + 𝐾) = ((𝑛 + 1) + 𝐾))
78	77	fveq2d 5324	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝐺‘(𝑘 + 𝐾)) = (𝐺‘((𝑛 + 1) + 𝐾)))
79	76, 78	eqeq12d 2103	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)) ↔ (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 1) + 𝐾))))
80	37	adantr 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = (𝐺‘(𝑘 + 𝐾)))
81		simprr 500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁))
82	79, 80, 81	rspcdva 2730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 1) + 𝐾)))
83	74	fveq2d 5324	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐺‘((𝑛 + 1) + 𝐾)) = (𝐺‘((𝑛 + 𝐾) + 1)))
84	82, 83	eqtrd 2121	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) = (𝐺‘((𝑛 + 𝐾) + 1)))
85	84	oveq2d 5684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐺‘((𝑛 + 𝐾) + 1))))
86	65, 75, 85	3eqtr4d 2131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)) = ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1))))
87	60, 86	eqeq12d 2103	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)) ↔ ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))) = ((seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) + (𝐹‘(𝑛 + 1)))))
88	56, 87	syl5ibr 155	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾))))
89	88	expr 368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)))))
90	89	a2d 26	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)))))
91	55, 90	syld 45	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾)))))
92	91	expcom 115	. . . . 5 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → (𝜑 → ((𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾))) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾))))))
93	92	a2d 26	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑛) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑛 + 𝐾)))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘((𝑛 + 1) + 𝐾))))))
94	10, 17, 24, 31, 51, 93	uzind4 9139	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾)))))
95	1, 94	mpcom 36	. 2 ⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾))))
96	3, 95	mpd 13	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑁) = (seq(𝑀 + 𝐾)( + , 𝐺, 𝑆)‘(𝑁 + 𝐾)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 = wceq 1290 ∈ wcel 1439 ∀wral 2360 ‘cfv 5030 (class class class)co 5668 ℂcc 7411 1c1 7414 + caddc 7416 ℤcz 8813 ℤ_≥cuz 9082 ...cfz 9487 seqcseq4 9914

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

This theorem is referenced by: seq3shft2 9962

W3C validator