Theorem iseqcaopr3 9460

Description: Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.)

Hypotheses

Ref	Expression
iseqcaopr3.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
iseqcaopr3.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)
iseqcaopr3.3	⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
iseqcaopr3.4	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
iseqcaopr3.5	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆)
iseqcaopr3.6	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))
iseqcaopr3.7	⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))))
iseqcaopr3.s	⊢ (𝜑 → 𝑆 ∈ 𝑉)

Assertion

Ref	Expression
iseqcaopr3	⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))

Distinct variable groups:   + ,𝑛,𝑥,𝑦   𝑘,𝐹,𝑛,𝑥,𝑦   𝑘,𝐺,𝑛,𝑥,𝑦   𝑘,𝐻,𝑛,𝑥,𝑦   𝑘,𝑀,𝑛,𝑥,𝑦   𝑘,𝑁,𝑛,𝑥,𝑦   𝑄,𝑘,𝑛,𝑥,𝑦   𝑆,𝑘,𝑛,𝑥,𝑦   𝜑,𝑘,𝑛,𝑥,𝑦

Allowed substitution hints:   + (𝑘)   𝑉(𝑥,𝑦,𝑘,𝑛)

Proof of Theorem iseqcaopr3

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseqcaopr3.3	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
2		eluzfz2 9051	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		fveq2 5198	. . . . 5 ⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = (seq𝑀( + , 𝐻, 𝑆)‘𝑀))
5		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐹, 𝑆)‘𝑧) = (seq𝑀( + , 𝐹, 𝑆)‘𝑀))
6		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑀 → (seq𝑀( + , 𝐺, 𝑆)‘𝑧) = (seq𝑀( + , 𝐺, 𝑆)‘𝑀))
7	5, 6	oveq12d 5550	. . . . 5 ⊢ (𝑧 = 𝑀 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀)))
8	4, 7	eqeq12d 2095	. . . 4 ⊢ (𝑧 = 𝑀 → ((seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) ↔ (seq𝑀( + , 𝐻, 𝑆)‘𝑀) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀))))
9	8	imbi2d 228	. . 3 ⊢ (𝑧 = 𝑀 → ((𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑀) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀)))))
10		fveq2 5198	. . . . 5 ⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = (seq𝑀( + , 𝐻, 𝑆)‘𝑛))
11		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐹, 𝑆)‘𝑧) = (seq𝑀( + , 𝐹, 𝑆)‘𝑛))
12		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑛 → (seq𝑀( + , 𝐺, 𝑆)‘𝑧) = (seq𝑀( + , 𝐺, 𝑆)‘𝑛))
13	11, 12	oveq12d 5550	. . . . 5 ⊢ (𝑧 = 𝑛 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)))
14	10, 13	eqeq12d 2095	. . . 4 ⊢ (𝑧 = 𝑛 → ((seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) ↔ (seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛))))
15	14	imbi2d 228	. . 3 ⊢ (𝑧 = 𝑛 → ((𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)))))
16		fveq2 5198	. . . . 5 ⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)))
17		fveq2 5198	. . . . . 6 ⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐹, 𝑆)‘𝑧) = (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)))
18		fveq2 5198	. . . . . 6 ⊢ (𝑧 = (𝑛 + 1) → (seq𝑀( + , 𝐺, 𝑆)‘𝑧) = (seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1)))
19	17, 18	oveq12d 5550	. . . . 5 ⊢ (𝑧 = (𝑛 + 1) → ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))))
20	16, 19	eqeq12d 2095	. . . 4 ⊢ (𝑧 = (𝑛 + 1) → ((seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) ↔ (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1)))))
21	20	imbi2d 228	. . 3 ⊢ (𝑧 = (𝑛 + 1) → ((𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))))))
22		fveq2 5198	. . . . 5 ⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = (seq𝑀( + , 𝐻, 𝑆)‘𝑁))
23		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐹, 𝑆)‘𝑧) = (seq𝑀( + , 𝐹, 𝑆)‘𝑁))
24		fveq2 5198	. . . . . 6 ⊢ (𝑧 = 𝑁 → (seq𝑀( + , 𝐺, 𝑆)‘𝑧) = (seq𝑀( + , 𝐺, 𝑆)‘𝑁))
25	23, 24	oveq12d 5550	. . . . 5 ⊢ (𝑧 = 𝑁 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))
26	22, 25	eqeq12d 2095	. . . 4 ⊢ (𝑧 = 𝑁 → ((seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧)) ↔ (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁))))
27	26	imbi2d 228	. . 3 ⊢ (𝑧 = 𝑁 → ((𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑧) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑧)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑧))) ↔ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))))
28		eluzel2 8624	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
29	1, 28	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
30		uzid 8633	. . . . . . 7 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
31	29, 30	syl 14	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
32		iseqcaopr3.6	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))
33	32	ralrimiva 2434	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))
34		fveq2 5198	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → (𝐻‘𝑘) = (𝐻‘𝑀))
35		fveq2 5198	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀))
36		fveq2 5198	. . . . . . . . 9 ⊢ (𝑘 = 𝑀 → (𝐺‘𝑘) = (𝐺‘𝑀))
37	35, 36	oveq12d 5550	. . . . . . . 8 ⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀)))
38	34, 37	eqeq12d 2095	. . . . . . 7 ⊢ (𝑘 = 𝑀 → ((𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ↔ (𝐻‘𝑀) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀))))
39	38	rspcv 2697	. . . . . 6 ⊢ (𝑀 ∈ (ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) → (𝐻‘𝑀) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀))))
40	31, 33, 39	sylc 61	. . . . 5 ⊢ (𝜑 → (𝐻‘𝑀) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀)))
41		iseqcaopr3.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ 𝑉)
42		iseqcaopr3.2	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆)
43	42	ralrimivva 2443	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑄𝑦) ∈ 𝑆)
44	43	adantr 270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑄𝑦) ∈ 𝑆)
45		iseqcaopr3.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)
46		iseqcaopr3.5	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ 𝑆)
47		oveq1 5539	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝐹‘𝑘) → (𝑥𝑄𝑦) = ((𝐹‘𝑘)𝑄𝑦))
48	47	eleq1d 2147	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐹‘𝑘) → ((𝑥𝑄𝑦) ∈ 𝑆 ↔ ((𝐹‘𝑘)𝑄𝑦) ∈ 𝑆))
49		oveq2 5540	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑘)𝑄𝑦) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))
50	49	eleq1d 2147	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐺‘𝑘) → (((𝐹‘𝑘)𝑄𝑦) ∈ 𝑆 ↔ ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ∈ 𝑆))
51	48, 50	rspc2v 2713	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑘) ∈ 𝑆 ∧ (𝐺‘𝑘) ∈ 𝑆) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑄𝑦) ∈ 𝑆 → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ∈ 𝑆))
52	45, 46, 51	syl2anc 403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑄𝑦) ∈ 𝑆 → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ∈ 𝑆))
53	44, 52	mpd 13	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ∈ 𝑆)
54	32, 53	eqeltrd 2155	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑘) ∈ 𝑆)
55	54	ralrimiva 2434	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) ∈ 𝑆)
56		fveq2 5198	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (𝐻‘𝑘) = (𝐻‘𝑥))
57	56	eleq1d 2147	. . . . . . . 8 ⊢ (𝑘 = 𝑥 → ((𝐻‘𝑘) ∈ 𝑆 ↔ (𝐻‘𝑥) ∈ 𝑆))
58	57	rspcv 2697	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) ∈ 𝑆 → (𝐻‘𝑥) ∈ 𝑆))
59	55, 58	mpan9 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑥) ∈ 𝑆)
60		iseqcaopr3.1	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
61	29, 41, 59, 60	iseq1 9442	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑀) = (𝐻‘𝑀))
62	45	ralrimiva 2434	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ 𝑆)
63		fveq2 5198	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥))
64	63	eleq1d 2147	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ((𝐹‘𝑘) ∈ 𝑆 ↔ (𝐹‘𝑥) ∈ 𝑆))
65	64	rspcv 2697	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ 𝑆 → (𝐹‘𝑥) ∈ 𝑆))
66	62, 65	mpan9 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
67	29, 41, 66, 60	iseq1 9442	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐹, 𝑆)‘𝑀) = (𝐹‘𝑀))
68	46	ralrimiva 2434	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆)
69		fveq2 5198	. . . . . . . . . 10 ⊢ (𝑘 = 𝑥 → (𝐺‘𝑘) = (𝐺‘𝑥))
70	69	eleq1d 2147	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → ((𝐺‘𝑘) ∈ 𝑆 ↔ (𝐺‘𝑥) ∈ 𝑆))
71	70	rspcv 2697	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐺‘𝑘) ∈ 𝑆 → (𝐺‘𝑥) ∈ 𝑆))
72	68, 71	mpan9 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
73	29, 41, 72, 60	iseq1 9442	. . . . . 6 ⊢ (𝜑 → (seq𝑀( + , 𝐺, 𝑆)‘𝑀) = (𝐺‘𝑀))
74	67, 73	oveq12d 5550	. . . . 5 ⊢ (𝜑 → ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀)) = ((𝐹‘𝑀)𝑄(𝐺‘𝑀)))
75	40, 61, 74	3eqtr4d 2123	. . . 4 ⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑀) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀)))
76	75	a1i 9	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑀) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑀)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑀))))
77		oveq1 5539	. . . . . 6 ⊢ ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) → ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + (𝐻‘(𝑛 + 1))))
78		elfzouz 9161	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀))
79	78	adantl 271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀))
80	41	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑆 ∈ 𝑉)
81	59	adantlr 460	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐻‘𝑥) ∈ 𝑆)
82	60	adantlr 460	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
83	79, 80, 81, 82	iseqp1 9445	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) + (𝐻‘(𝑛 + 1))))
84		iseqcaopr3.7	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))))
85		fzofzp1 9236	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁))
86		elfzuz 9041	. . . . . . . . . . . 12 ⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝑛 + 1) ∈ (ℤ≥‘𝑀))
87	85, 86	syl 14	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (ℤ≥‘𝑀))
88	87	adantl 271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝑛 + 1) ∈ (ℤ≥‘𝑀))
89	33	adantr 270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)))
90		fveq2 5198	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 + 1) → (𝐻‘𝑘) = (𝐻‘(𝑛 + 1)))
91		fveq2 5198	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
92		fveq2 5198	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1)))
93	91, 92	oveq12d 5550	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1))))
94	90, 93	eqeq12d 2095	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → ((𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) ↔ (𝐻‘(𝑛 + 1)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))))
95	94	rspcv 2697	. . . . . . . . . 10 ⊢ ((𝑛 + 1) ∈ (ℤ≥‘𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑀)(𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘)) → (𝐻‘(𝑛 + 1)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))))
96	88, 89, 95	sylc 61	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐻‘(𝑛 + 1)) = ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1))))
97	96	oveq2d 5548	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))))
98	66	adantlr 460	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆)
99	79, 80, 98, 82	iseqp1 9445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1))))
100	72	adantlr 460	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
101	79, 80, 100, 82	iseqp1 9445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1))))
102	99, 101	oveq12d 5550	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺, 𝑆)‘𝑛) + (𝐺‘(𝑛 + 1)))))
103	84, 97, 102	3eqtr4rd 2124	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + (𝐻‘(𝑛 + 1))))
104	83, 103	eqeq12d 2095	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))) ↔ ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) + (𝐻‘(𝑛 + 1))) = (((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) + (𝐻‘(𝑛 + 1)))))
105	77, 104	syl5ibr 154	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) → (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1)))))
106	105	expcom 114	. . . 4 ⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛)) → (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))))))
107	106	a2d 26	. . 3 ⊢ (𝑛 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑛) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑛)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑛))) → (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘(𝑛 + 1)) = ((seq𝑀( + , 𝐹, 𝑆)‘(𝑛 + 1))𝑄(seq𝑀( + , 𝐺, 𝑆)‘(𝑛 + 1))))))
108	9, 15, 21, 27, 76, 107	fzind2 9248	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁))))
109	3, 108	mpcom 36	1 ⊢ (𝜑 → (seq𝑀( + , 𝐻, 𝑆)‘𝑁) = ((seq𝑀( + , 𝐹, 𝑆)‘𝑁)𝑄(seq𝑀( + , 𝐺, 𝑆)‘𝑁)))

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1284   ∈ wcel 1433  ∀wral 2348  ‘cfv 4922  (class class class)co 5532  1c1 6982   + caddc 6984  ℤcz 8351  ℤ_≥cuz 8619  ...cfz 9029  ..^cfzo 9152  seqcseq 9431

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 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-1re 7070  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-addcom 7076  ax-addass 7078  ax-distr 7080  ax-i2m1 7081  ax-0lt1 7082  ax-0id 7084  ax-rnegex 7085  ax-cnre 7087  ax-pre-ltirr 7088  ax-pre-ltwlin 7089  ax-pre-lttrn 7090  ax-pre-ltadd 7092

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-nel 2340  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-id 4048  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-recs 5943  df-frec 6001  df-pnf 7155  df-mnf 7156  df-xr 7157  df-ltxr 7158  df-le 7159  df-sub 7281  df-neg 7282  df-inn 8040  df-n0 8289  df-z 8352  df-uz 8620  df-fz 9030  df-fzo 9153  df-iseq 9432

This theorem is referenced by:  iseqcaopr2  9461