seq3f1olemqsumk - Intuitionistic Logic Explorer

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

Theorem seq3f1olemqsumk 10583

Description: Lemma for seq3f1o 10588. 𝑄 gives the same sum as 𝐽 in the range (𝐾...𝑁). (Contributed by Jim Kingdon, 22-Aug-2022.)

**Hypotheses**
Ref	Expression
iseqf1o.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
iseqf1o.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
iseqf1o.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
iseqf1o.4	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
iseqf1o.6	⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
iseqf1o.7	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
iseqf1olemstep.k	⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
iseqf1olemstep.j	⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
iseqf1olemstep.const	⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥)
iseqf1olemnk	⊢ (𝜑 → 𝐾 ≠ (^◡𝐽‘𝐾))
iseqf1olemqres.q	⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢)))
iseqf1olemqsumk.p	⊢ 𝑃 = (𝑥 ∈ (ℤ_≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀)))

**Assertion**
Ref	Expression
seq3f1olemqsumk	⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))

Distinct variable groups: 𝑢,𝐽 𝑢,𝐾,𝑥 𝑢,𝑀,𝑥 𝑢,𝑁 𝑥,𝐽 𝑥,𝑄 𝜑,𝑥 𝑥, + ,𝑦,𝑧 𝑓,𝐺,𝑥 𝑓,𝐽,𝑦,𝑧 𝑦,𝐾,𝑧 𝑓,𝑀 𝑓,𝑁,𝑥,𝑦,𝑧 𝑥,𝑃,𝑦,𝑧 𝑄,𝑓,𝑦,𝑧 𝑥,𝑆,𝑦,𝑧 𝜑,𝑢 𝜑,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑓) 𝑃(𝑢,𝑓) + (𝑢,𝑓) 𝑄(𝑢) 𝑆(𝑢,𝑓) 𝐹(𝑥,𝑦,𝑧,𝑢,𝑓) 𝐺(𝑦,𝑧,𝑢) 𝐾(𝑓) 𝑀(𝑦,𝑧)

Proof of Theorem seq3f1olemqsumk Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iseqf1o.1	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
2		iseqf1o.2	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
3		iseqf1o.3	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
4		iseqf1o.4	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
5		iseqf1o.6	. . . . . 6 ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
6		iseqf1o.7	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
7		iseqf1olemstep.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
8		iseqf1olemstep.j	. . . . . 6 ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
9		iseqf1olemstep.const	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀..^𝐾)(𝐽‘𝑥) = 𝑥)
10		iseqf1olemnk	. . . . . 6 ⊢ (𝜑 → 𝐾 ≠ (^◡𝐽‘𝐾))
11		iseqf1olemqres.q	. . . . . 6 ⊢ 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽‘𝑢)))
12		iseqf1olemqsumk.p	. . . . . 6 ⊢ 𝑃 = (𝑥 ∈ (ℤ_≥‘𝑀) ↦ if(𝑥 ≤ 𝑁, (𝐺‘(𝑓‘𝑥)), (𝐺‘𝑀)))
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	seq3f1olemqsumkj 10582	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
14	13	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
15		f1ocnv 5513	. . . . . . . . . . . 12 ⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
16	8, 15	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
17		f1of 5500	. . . . . . . . . . 11 ⊢ (^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
18	16, 17	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
19	18, 7	ffvelcdmd 5694	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (𝑀...𝑁))
20		elfzelz 10091	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
21	19, 20	syl 14	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℤ)
22	21	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
23	22	peano2zd 9442	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ∈ ℤ)
24		elfzel2 10089	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
25	7, 24	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	25	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ)
27		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) < 𝑁)
28		zltp1le 9371	. . . . . . . 8 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
29	22, 26, 28	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
30	27, 29	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑁)
31		eluz2 9598	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) ↔ (((^◡𝐽‘𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
32	23, 26, 30, 31	syl3anbrc 1183	. . . . 5 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)))
33	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
34	8	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
35		elfzel1 10090	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
37	36	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ)
38	33, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ)
39		elfzelz 10091	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ)
40	39	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ)
41	37, 38, 40	3jca 1179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ))
42	36	zred 9439	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	42	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ)
44	21	zred 9439	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℝ)
45		peano2re 8155	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝐾) ∈ ℝ → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
47	46	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
48	40	zred 9439	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ)
49		elfzelz 10091	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
50	7, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
51	50	zred 9439	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℝ)
52		elfzle1 10093	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
53	7, 52	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
54	4, 7, 8, 9	iseqf1olemkle 10568	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ≤ (^◡𝐽‘𝐾))
55	42, 51, 44, 53, 54	letrd 8143	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ≤ (^◡𝐽‘𝐾))
56	44	lep1d 8950	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ ((^◡𝐽‘𝐾) + 1))
57	42, 44, 46, 55, 56	letrd 8143	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
58	57	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
59		elfzle1 10093	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
60	59	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
61	43, 47, 48, 58, 60	letrd 8143	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣)
62		elfzle2 10094	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁)
63	62	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁)
64	61, 63	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
65		elfz2 10081	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
66	41, 64, 65	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁))
67	33, 34, 66, 11	iseqf1olemqval 10571	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)))
68	44	ad3antrrr 492	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) ∈ ℝ)
69	68, 45	syl 14	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
70	48	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ∈ ℝ)
71	68	ltp1d 8949	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < ((^◡𝐽‘𝐾) + 1))
72	60	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
73	68, 69, 70, 71, 72	ltletrd 8442	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < 𝑣)
74		elfzle2 10094	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)) → 𝑣 ≤ (^◡𝐽‘𝐾))
75	74	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ≤ (^◡𝐽‘𝐾))
76	70, 68, 75	lensymd 8141	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ¬ (^◡𝐽‘𝐾) < 𝑣)
77	73, 76	pm2.65da 662	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)))
78	77	iffalsed 3567	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣))
79	67, 78	eqtrd 2226	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣))
80	79	fveq2d 5558	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣)))
81	33, 34, 11	iseqf1olemqf1o 10577	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
82	6	ralrimiva 2567	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
83	82	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
84	83	r19.21bi 2582	. . . . . . 7 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
85	33, 81, 66, 84, 12	iseqf1olemfvp 10581	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣)))
86	33, 34, 66, 84, 12	iseqf1olemfvp 10581	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣)))
87	80, 85, 86	3eqtr4rd 2237	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣))
88	36	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ)
89		eluzelz 9601	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ)
90	89	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ)
91	42	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ)
92	46	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
93	90	zred 9439	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ)
94	57	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
95		eluzle 9604	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
96	95	adantl 277	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
97	91, 92, 93, 94, 96	letrd 8143	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥)
98		eluz2 9598	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))
99	88, 90, 97, 98	syl3anbrc 1183	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ (ℤ_≥‘𝑀))
100	7	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝐾 ∈ (𝑀...𝑁))
101	8	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
102	6	adantlr 477	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
103	100, 101, 11, 102, 12	iseqf1olemjpcl 10579	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
104	99, 103	syldan 282	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
105	7, 8, 11, 6, 12	iseqf1olemqpcl 10580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
106	105	adantlr 477	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
107	99, 106	syldan 282	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
108	1	adantlr 477	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
109	32, 87, 104, 107, 108	seq3fveq 10550	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
110	14, 109	oveq12d 5936	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
111	3	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
112		eluz2 9598	. . . . . 6 ⊢ ((^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ (^◡𝐽‘𝐾) ∈ ℤ ∧ 𝐾 ≤ (^◡𝐽‘𝐾)))
113	50, 21, 54, 112	syl3anbrc 1183	. . . . 5 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
114	113	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
115		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝐾))
116	7	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
117		elfzuz 10087	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_≥‘𝑀))
118	116, 117	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (ℤ_≥‘𝑀))
119		uztrn 9609	. . . . . . 7 ⊢ ((𝑥 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑥 ∈ (ℤ_≥‘𝑀))
120	115, 118, 119	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝑀))
121	7, 8, 11, 6, 12	iseqf1olemjpcl 10579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
122	120, 121	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
123	122	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
124	108, 111, 32, 114, 123	seq3split 10559	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)))
125	120, 105	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
126	125	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
127	108, 111, 32, 114, 126	seq3split 10559	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
128	110, 124, 127	3eqtr4d 2236	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
129	13	adantr 276	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
130		simpr 110	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (^◡𝐽‘𝐾) = 𝑁)
131	130	fveq2d 5558	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))
132	130	fveq2d 5558	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
133	129, 131, 132	3eqtr3d 2234	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
134		elfzle2 10094	. . . 4 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ≤ 𝑁)
135	19, 134	syl 14	. . 3 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ 𝑁)
136		zleloe 9364	. . . 4 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
137	21, 25, 136	syl2anc 411	. . 3 ⊢ (𝜑 → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
138	135, 137	mpbid 147	. 2 ⊢ (𝜑 → ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁))
139	128, 133, 138	mpjaodan 799	1 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ∀wral 2472 ⦋csb 3080 ifcif 3557 class class class wbr 4029 ↦ cmpt 4090 ^◡ccnv 4658 ⟶wf 5250 –1-1-onto→wf1o 5253 ‘cfv 5254 (class class class)co 5918 ℝcr 7871 1c1 7873 + caddc 7875 < clt 8054 ≤ cle 8055 − cmin 8190 ℤcz 9317 ℤ_≥cuz 9592 ...cfz 10074 ..^cfzo 10208 seqcseq 10518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-0id 7980 ax-rnegex 7981 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-1o 6469 df-er 6587 df-en 6795 df-fin 6797 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-inn 8983 df-n0 9241 df-z 9318 df-uz 9593 df-fz 10075 df-fzo 10209 df-seqfrec 10519

This theorem is referenced by: seq3f1olemqsum 10584

W3C validator