seq3f1olemqsumk - Intuitionistic Logic Explorer

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

Theorem seq3f1olemqsumk 10621

Description: Lemma for seq3f1o 10626. 𝑄 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 10620	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
14	13	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
15		f1ocnv 5520	. . . . . . . . . . . 12 ⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
16	8, 15	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
17		f1of 5507	. . . . . . . . . . 11 ⊢ (^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
18	16, 17	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
19	18, 7	ffvelcdmd 5701	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (𝑀...𝑁))
20		elfzelz 10117	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
21	19, 20	syl 14	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℤ)
22	21	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
23	22	peano2zd 9468	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ∈ ℤ)
24		elfzel2 10115	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
25	7, 24	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	25	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ)
27		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) < 𝑁)
28		zltp1le 9397	. . . . . . . 8 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
29	22, 26, 28	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
30	27, 29	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑁)
31		eluz2 9624	. . . . . 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 10116	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
37	36	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ)
38	33, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ)
39		elfzelz 10117	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ)
40	39	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ)
41	37, 38, 40	3jca 1179	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ))
42	36	zred 9465	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	42	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ)
44	21	zred 9465	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℝ)
45		peano2re 8179	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝐾) ∈ ℝ → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
47	46	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
48	40	zred 9465	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ)
49		elfzelz 10117	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
50	7, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
51	50	zred 9465	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℝ)
52		elfzle1 10119	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
53	7, 52	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
54	4, 7, 8, 9	iseqf1olemkle 10606	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ≤ (^◡𝐽‘𝐾))
55	42, 51, 44, 53, 54	letrd 8167	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ≤ (^◡𝐽‘𝐾))
56	44	lep1d 8975	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ ((^◡𝐽‘𝐾) + 1))
57	42, 44, 46, 55, 56	letrd 8167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
58	57	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
59		elfzle1 10119	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
60	59	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
61	43, 47, 48, 58, 60	letrd 8167	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣)
62		elfzle2 10120	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁)
63	62	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁)
64	61, 63	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
65		elfz2 10107	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
66	41, 64, 65	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁))
67	33, 34, 66, 11	iseqf1olemqval 10609	. . . . . . . 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 8974	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < ((^◡𝐽‘𝐾) + 1))
72	60	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
73	68, 69, 70, 71, 72	ltletrd 8467	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < 𝑣)
74		elfzle2 10120	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)) → 𝑣 ≤ (^◡𝐽‘𝐾))
75	74	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ≤ (^◡𝐽‘𝐾))
76	70, 68, 75	lensymd 8165	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ¬ (^◡𝐽‘𝐾) < 𝑣)
77	73, 76	pm2.65da 662	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)))
78	77	iffalsed 3572	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣))
79	67, 78	eqtrd 2229	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣))
80	79	fveq2d 5565	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣)))
81	33, 34, 11	iseqf1olemqf1o 10615	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
82	6	ralrimiva 2570	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
83	82	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
84	83	r19.21bi 2585	. . . . . . 7 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
85	33, 81, 66, 84, 12	iseqf1olemfvp 10619	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣)))
86	33, 34, 66, 84, 12	iseqf1olemfvp 10619	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣)))
87	80, 85, 86	3eqtr4rd 2240	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣))
88	36	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ)
89		eluzelz 9627	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ)
90	89	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ)
91	42	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ)
92	46	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
93	90	zred 9465	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ)
94	57	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
95		eluzle 9630	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
96	95	adantl 277	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
97	91, 92, 93, 94, 96	letrd 8167	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥)
98		eluz2 9624	. . . . . . 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 10617	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
104	99, 103	syldan 282	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
105	7, 8, 11, 6, 12	iseqf1olemqpcl 10618	. . . . . . 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 10588	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
110	14, 109	oveq12d 5943	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
111	3	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
112		eluz2 9624	. . . . . 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 10113	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_≥‘𝑀))
118	116, 117	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (ℤ_≥‘𝑀))
119		uztrn 9635	. . . . . . 7 ⊢ ((𝑥 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑥 ∈ (ℤ_≥‘𝑀))
120	115, 118, 119	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝑀))
121	7, 8, 11, 6, 12	iseqf1olemjpcl 10617	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
122	120, 121	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
123	122	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
124	108, 111, 32, 114, 123	seq3split 10597	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)))
125	120, 105	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
126	125	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
127	108, 111, 32, 114, 126	seq3split 10597	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
128	110, 124, 127	3eqtr4d 2239	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
129	13	adantr 276	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
130		simpr 110	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (^◡𝐽‘𝐾) = 𝑁)
131	130	fveq2d 5565	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))
132	130	fveq2d 5565	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
133	129, 131, 132	3eqtr3d 2237	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
134		elfzle2 10120	. . . 4 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ≤ 𝑁)
135	19, 134	syl 14	. . 3 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ 𝑁)
136		zleloe 9390	. . . 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 2167 ≠ wne 2367 ∀wral 2475 ⦋csb 3084 ifcif 3562 class class class wbr 4034 ↦ cmpt 4095 ^◡ccnv 4663 ⟶wf 5255 –1-1-onto→wf1o 5258 ‘cfv 5259 (class class class)co 5925 ℝcr 7895 1c1 7897 + caddc 7899 < clt 8078 ≤ cle 8079 − cmin 8214 ℤcz 9343 ℤ_≥cuz 9618 ...cfz 10100 ..^cfzo 10234 seqcseq 10556

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-addcom 7996 ax-addass 7998 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-0id 8004 ax-rnegex 8005 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012

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 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-frec 6458 df-1o 6483 df-er 6601 df-en 6809 df-fin 6811 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-inn 9008 df-n0 9267 df-z 9344 df-uz 9619 df-fz 10101 df-fzo 10235 df-seqfrec 10557

This theorem is referenced by: seq3f1olemqsum 10622

W3C validator