seq3f1olemqsumk - Intuitionistic Logic Explorer

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

Theorem seq3f1olemqsumk 10513

Description: Lemma for seq3f1o 10518. 𝑄 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 10512	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
14	13	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
15		f1ocnv 5486	. . . . . . . . . . . 12 ⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
16	8, 15	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
17		f1of 5473	. . . . . . . . . . 11 ⊢ (^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
18	16, 17	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
19	18, 7	ffvelcdmd 5665	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (𝑀...𝑁))
20		elfzelz 10039	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
21	19, 20	syl 14	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℤ)
22	21	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
23	22	peano2zd 9392	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ∈ ℤ)
24		elfzel2 10037	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
25	7, 24	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	25	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ)
27		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) < 𝑁)
28		zltp1le 9321	. . . . . . . 8 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
29	22, 26, 28	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
30	27, 29	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑁)
31		eluz2 9548	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) ↔ (((^◡𝐽‘𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
32	23, 26, 30, 31	syl3anbrc 1182	. . . . 5 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)))
33	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
34	8	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
35		elfzel1 10038	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
37	36	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ)
38	33, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ)
39		elfzelz 10039	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ)
40	39	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ)
41	37, 38, 40	3jca 1178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ))
42	36	zred 9389	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	42	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ)
44	21	zred 9389	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℝ)
45		peano2re 8107	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝐾) ∈ ℝ → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
47	46	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
48	40	zred 9389	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ)
49		elfzelz 10039	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
50	7, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
51	50	zred 9389	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℝ)
52		elfzle1 10041	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
53	7, 52	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
54	4, 7, 8, 9	iseqf1olemkle 10498	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ≤ (^◡𝐽‘𝐾))
55	42, 51, 44, 53, 54	letrd 8095	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ≤ (^◡𝐽‘𝐾))
56	44	lep1d 8902	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ ((^◡𝐽‘𝐾) + 1))
57	42, 44, 46, 55, 56	letrd 8095	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
58	57	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
59		elfzle1 10041	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
60	59	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
61	43, 47, 48, 58, 60	letrd 8095	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣)
62		elfzle2 10042	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁)
63	62	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁)
64	61, 63	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
65		elfz2 10029	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
66	41, 64, 65	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁))
67	33, 34, 66, 11	iseqf1olemqval 10501	. . . . . . . 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 8901	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < ((^◡𝐽‘𝐾) + 1))
72	60	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
73	68, 69, 70, 71, 72	ltletrd 8394	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < 𝑣)
74		elfzle2 10042	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)) → 𝑣 ≤ (^◡𝐽‘𝐾))
75	74	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ≤ (^◡𝐽‘𝐾))
76	70, 68, 75	lensymd 8093	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ¬ (^◡𝐽‘𝐾) < 𝑣)
77	73, 76	pm2.65da 662	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)))
78	77	iffalsed 3556	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣))
79	67, 78	eqtrd 2220	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣))
80	79	fveq2d 5531	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣)))
81	33, 34, 11	iseqf1olemqf1o 10507	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
82	6	ralrimiva 2560	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
83	82	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
84	83	r19.21bi 2575	. . . . . . 7 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
85	33, 81, 66, 84, 12	iseqf1olemfvp 10511	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣)))
86	33, 34, 66, 84, 12	iseqf1olemfvp 10511	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣)))
87	80, 85, 86	3eqtr4rd 2231	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣))
88	36	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ)
89		eluzelz 9551	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ)
90	89	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ)
91	42	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ)
92	46	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
93	90	zred 9389	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ)
94	57	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
95		eluzle 9554	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
96	95	adantl 277	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
97	91, 92, 93, 94, 96	letrd 8095	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥)
98		eluz2 9548	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))
99	88, 90, 97, 98	syl3anbrc 1182	. . . . . 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 10509	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
104	99, 103	syldan 282	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
105	7, 8, 11, 6, 12	iseqf1olemqpcl 10510	. . . . . . 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 10485	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
110	14, 109	oveq12d 5906	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
111	3	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
112		eluz2 9548	. . . . . 6 ⊢ ((^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ (^◡𝐽‘𝐾) ∈ ℤ ∧ 𝐾 ≤ (^◡𝐽‘𝐾)))
113	50, 21, 54, 112	syl3anbrc 1182	. . . . 5 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
114	113	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
115		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝐾))
116	7	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
117		elfzuz 10035	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_≥‘𝑀))
118	116, 117	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (ℤ_≥‘𝑀))
119		uztrn 9558	. . . . . . 7 ⊢ ((𝑥 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑥 ∈ (ℤ_≥‘𝑀))
120	115, 118, 119	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝑀))
121	7, 8, 11, 6, 12	iseqf1olemjpcl 10509	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
122	120, 121	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
123	122	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
124	108, 111, 32, 114, 123	seq3split 10493	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)))
125	120, 105	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
126	125	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
127	108, 111, 32, 114, 126	seq3split 10493	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
128	110, 124, 127	3eqtr4d 2230	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
129	13	adantr 276	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
130		simpr 110	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (^◡𝐽‘𝐾) = 𝑁)
131	130	fveq2d 5531	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))
132	130	fveq2d 5531	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
133	129, 131, 132	3eqtr3d 2228	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
134		elfzle2 10042	. . . 4 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ≤ 𝑁)
135	19, 134	syl 14	. . 3 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ 𝑁)
136		zleloe 9314	. . . 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 979 = wceq 1363 ∈ wcel 2158 ≠ wne 2357 ∀wral 2465 ⦋csb 3069 ifcif 3546 class class class wbr 4015 ↦ cmpt 4076 ^◡ccnv 4637 ⟶wf 5224 –1-1-onto→wf1o 5227 ‘cfv 5228 (class class class)co 5888 ℝcr 7824 1c1 7826 + caddc 7828 < clt 8006 ≤ cle 8007 − cmin 8142 ℤcz 9267 ℤ_≥cuz 9542 ...cfz 10022 ..^cfzo 10156 seqcseq 10459

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-addcom 7925 ax-addass 7927 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-0id 7933 ax-rnegex 7934 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-frec 6406 df-1o 6431 df-er 6549 df-en 6755 df-fin 6757 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-inn 8934 df-n0 9191 df-z 9268 df-uz 9543 df-fz 10023 df-fzo 10157 df-seqfrec 10460

This theorem is referenced by: seq3f1olemqsum 10514

W3C validator