seq3f1olemqsumk - Intuitionistic Logic Explorer

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

Theorem seq3f1olemqsumk 10696

Description: Lemma for seq3f1o 10701. 𝑄 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 10695	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
14	13	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
15		f1ocnv 5558	. . . . . . . . . . . 12 ⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
16	8, 15	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
17		f1of 5545	. . . . . . . . . . 11 ⊢ (^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
18	16, 17	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
19	18, 7	ffvelcdmd 5741	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (𝑀...𝑁))
20		elfzelz 10184	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
21	19, 20	syl 14	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℤ)
22	21	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
23	22	peano2zd 9535	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ∈ ℤ)
24		elfzel2 10182	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
25	7, 24	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	25	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ)
27		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) < 𝑁)
28		zltp1le 9464	. . . . . . . 8 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
29	22, 26, 28	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
30	27, 29	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑁)
31		eluz2 9691	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) ↔ (((^◡𝐽‘𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
32	23, 26, 30, 31	syl3anbrc 1184	. . . . 5 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)))
33	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
34	8	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
35		elfzel1 10183	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
37	36	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ)
38	33, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ)
39		elfzelz 10184	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ)
40	39	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ)
41	37, 38, 40	3jca 1180	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ))
42	36	zred 9532	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	42	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ)
44	21	zred 9532	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℝ)
45		peano2re 8245	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝐾) ∈ ℝ → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
47	46	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
48	40	zred 9532	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ)
49		elfzelz 10184	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
50	7, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
51	50	zred 9532	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℝ)
52		elfzle1 10186	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
53	7, 52	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
54	4, 7, 8, 9	iseqf1olemkle 10681	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ≤ (^◡𝐽‘𝐾))
55	42, 51, 44, 53, 54	letrd 8233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ≤ (^◡𝐽‘𝐾))
56	44	lep1d 9041	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ ((^◡𝐽‘𝐾) + 1))
57	42, 44, 46, 55, 56	letrd 8233	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
58	57	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
59		elfzle1 10186	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
60	59	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
61	43, 47, 48, 58, 60	letrd 8233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣)
62		elfzle2 10187	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁)
63	62	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁)
64	61, 63	jca 306	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
65		elfz2 10174	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
66	41, 64, 65	sylanbrc 417	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁))
67	33, 34, 66, 11	iseqf1olemqval 10684	. . . . . . . 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 9040	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < ((^◡𝐽‘𝐾) + 1))
72	60	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
73	68, 69, 70, 71, 72	ltletrd 8533	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < 𝑣)
74		elfzle2 10187	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)) → 𝑣 ≤ (^◡𝐽‘𝐾))
75	74	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ≤ (^◡𝐽‘𝐾))
76	70, 68, 75	lensymd 8231	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ¬ (^◡𝐽‘𝐾) < 𝑣)
77	73, 76	pm2.65da 663	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)))
78	77	iffalsed 3590	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣))
79	67, 78	eqtrd 2240	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣))
80	79	fveq2d 5604	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣)))
81	33, 34, 11	iseqf1olemqf1o 10690	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
82	6	ralrimiva 2581	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
83	82	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
84	83	r19.21bi 2596	. . . . . . 7 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
85	33, 81, 66, 84, 12	iseqf1olemfvp 10694	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣)))
86	33, 34, 66, 84, 12	iseqf1olemfvp 10694	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣)))
87	80, 85, 86	3eqtr4rd 2251	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣))
88	36	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ)
89		eluzelz 9694	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ)
90	89	adantl 277	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ)
91	42	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ)
92	46	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
93	90	zred 9532	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ)
94	57	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
95		eluzle 9697	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
96	95	adantl 277	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
97	91, 92, 93, 94, 96	letrd 8233	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥)
98		eluz2 9691	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))
99	88, 90, 97, 98	syl3anbrc 1184	. . . . . 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 10692	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
104	99, 103	syldan 282	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
105	7, 8, 11, 6, 12	iseqf1olemqpcl 10693	. . . . . . 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 10663	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
110	14, 109	oveq12d 5987	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
111	3	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
112		eluz2 9691	. . . . . 6 ⊢ ((^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ (^◡𝐽‘𝐾) ∈ ℤ ∧ 𝐾 ≤ (^◡𝐽‘𝐾)))
113	50, 21, 54, 112	syl3anbrc 1184	. . . . 5 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
114	113	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
115		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝐾))
116	7	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
117		elfzuz 10180	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_≥‘𝑀))
118	116, 117	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (ℤ_≥‘𝑀))
119		uztrn 9702	. . . . . . 7 ⊢ ((𝑥 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑥 ∈ (ℤ_≥‘𝑀))
120	115, 118, 119	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝑀))
121	7, 8, 11, 6, 12	iseqf1olemjpcl 10692	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
122	120, 121	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
123	122	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
124	108, 111, 32, 114, 123	seq3split 10672	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)))
125	120, 105	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
126	125	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
127	108, 111, 32, 114, 126	seq3split 10672	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
128	110, 124, 127	3eqtr4d 2250	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
129	13	adantr 276	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
130		simpr 110	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (^◡𝐽‘𝐾) = 𝑁)
131	130	fveq2d 5604	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))
132	130	fveq2d 5604	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
133	129, 131, 132	3eqtr3d 2248	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
134		elfzle2 10187	. . . 4 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ≤ 𝑁)
135	19, 134	syl 14	. . 3 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ 𝑁)
136		zleloe 9456	. . . 4 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
137	21, 25, 136	syl2anc 411	. . 3 ⊢ (𝜑 → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
138	135, 137	mpbid 147	. 2 ⊢ (𝜑 → ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁))
139	128, 133, 138	mpjaodan 800	1 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 ∧ w3a 981 = wceq 1373 ∈ wcel 2178 ≠ wne 2378 ∀wral 2486 ⦋csb 3102 ifcif 3580 class class class wbr 4060 ↦ cmpt 4122 ^◡ccnv 4693 ⟶wf 5287 –1-1-onto→wf1o 5290 ‘cfv 5291 (class class class)co 5969 ℝcr 7961 1c1 7963 + caddc 7965 < clt 8144 ≤ cle 8145 − cmin 8280 ℤcz 9409 ℤ_≥cuz 9685 ...cfz 10167 ..^cfzo 10301 seqcseq 10631

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-coll 4176 ax-sep 4179 ax-nul 4187 ax-pow 4235 ax-pr 4270 ax-un 4499 ax-setind 4604 ax-iinf 4655 ax-cnex 8053 ax-resscn 8054 ax-1cn 8055 ax-1re 8056 ax-icn 8057 ax-addcl 8058 ax-addrcl 8059 ax-mulcl 8060 ax-addcom 8062 ax-addass 8064 ax-distr 8066 ax-i2m1 8067 ax-0lt1 8068 ax-0id 8070 ax-rnegex 8071 ax-cnre 8073 ax-pre-ltirr 8074 ax-pre-ltwlin 8075 ax-pre-lttrn 8076 ax-pre-apti 8077 ax-pre-ltadd 8078

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rab 2495 df-v 2779 df-sbc 3007 df-csb 3103 df-dif 3177 df-un 3179 df-in 3181 df-ss 3188 df-nul 3470 df-if 3581 df-pw 3629 df-sn 3650 df-pr 3651 df-op 3653 df-uni 3866 df-int 3901 df-iun 3944 df-br 4061 df-opab 4123 df-mpt 4124 df-tr 4160 df-id 4359 df-iord 4432 df-on 4434 df-ilim 4435 df-suc 4437 df-iom 4658 df-xp 4700 df-rel 4701 df-cnv 4702 df-co 4703 df-dm 4704 df-rn 4705 df-res 4706 df-ima 4707 df-iota 5252 df-fun 5293 df-fn 5294 df-f 5295 df-f1 5296 df-fo 5297 df-f1o 5298 df-fv 5299 df-riota 5924 df-ov 5972 df-oprab 5973 df-mpo 5974 df-1st 6251 df-2nd 6252 df-recs 6416 df-frec 6502 df-1o 6527 df-er 6645 df-en 6853 df-fin 6855 df-pnf 8146 df-mnf 8147 df-xr 8148 df-ltxr 8149 df-le 8150 df-sub 8282 df-neg 8283 df-inn 9074 df-n0 9333 df-z 9410 df-uz 9686 df-fz 10168 df-fzo 10302 df-seqfrec 10632

This theorem is referenced by: seq3f1olemqsum 10697

W3C validator