seq3f1olemqsumk - Intuitionistic Logic Explorer

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

Theorem seq3f1olemqsumk 10434

Description: Lemma for seq3f1o 10439. 𝑄 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 10433	. . . . 5 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
14	13	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
15		f1ocnv 5445	. . . . . . . . . . . 12 ⊢ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
16	8, 15	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
17		f1of 5432	. . . . . . . . . . 11 ⊢ (^◡𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
18	16, 17	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
19	18, 7	ffvelrnd 5621	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (𝑀...𝑁))
20		elfzelz 9960	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
21	19, 20	syl 14	. . . . . . . 8 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℤ)
22	21	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ ℤ)
23	22	peano2zd 9316	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ∈ ℤ)
24		elfzel2 9958	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
25	7, 24	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
26	25	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ ℤ)
27		simpr 109	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) < 𝑁)
28		zltp1le 9245	. . . . . . . 8 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
29	22, 26, 28	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) < 𝑁 ↔ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
30	27, 29	mpbid 146	. . . . . 6 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑁)
31		eluz2 9472	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) ↔ (((^◡𝐽‘𝐾) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((^◡𝐽‘𝐾) + 1) ≤ 𝑁))
32	23, 26, 30, 31	syl3anbrc 1171	. . . . 5 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝑁 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)))
33	7	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
34	8	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
35		elfzel1 9959	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
36	7, 35	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
37	36	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℤ)
38	33, 24	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑁 ∈ ℤ)
39		elfzelz 9960	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ∈ ℤ)
40	39	adantl 275	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℤ)
41	37, 38, 40	3jca 1167	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ))
42	36	zred 9313	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
43	42	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ∈ ℝ)
44	21	zred 9313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ ℝ)
45		peano2re 8034	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝐾) ∈ ℝ → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
46	44, 45	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
47	46	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
48	40	zred 9313	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ ℝ)
49		elfzelz 9960	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
50	7, 49	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
51	50	zred 9313	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ ℝ)
52		elfzle1 9962	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)
53	7, 52	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
54	4, 7, 8, 9	iseqf1olemkle 10419	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ≤ (^◡𝐽‘𝐾))
55	42, 51, 44, 53, 54	letrd 8022	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ≤ (^◡𝐽‘𝐾))
56	44	lep1d 8826	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ ((^◡𝐽‘𝐾) + 1))
57	42, 44, 46, 55, 56	letrd 8022	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
58	57	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
59		elfzle1 9962	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
60	59	adantl 275	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
61	43, 47, 48, 58, 60	letrd 8022	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑀 ≤ 𝑣)
62		elfzle2 9963	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁) → 𝑣 ≤ 𝑁)
63	62	adantl 275	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ≤ 𝑁)
64	61, 63	jca 304	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁))
65		elfz2 9951	. . . . . . . . . 10 ⊢ (𝑣 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑀 ≤ 𝑣 ∧ 𝑣 ≤ 𝑁)))
66	41, 64, 65	sylanbrc 414	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑣 ∈ (𝑀...𝑁))
67	33, 34, 66, 11	iseqf1olemqval 10422	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)))
68	44	ad3antrrr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) ∈ ℝ)
69	68, 45	syl 14	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
70	48	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ∈ ℝ)
71	68	ltp1d 8825	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < ((^◡𝐽‘𝐾) + 1))
72	60	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑣)
73	68, 69, 70, 71, 72	ltletrd 8321	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → (^◡𝐽‘𝐾) < 𝑣)
74		elfzle2 9963	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)) → 𝑣 ≤ (^◡𝐽‘𝐾))
75	74	adantl 275	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → 𝑣 ≤ (^◡𝐽‘𝐾))
76	70, 68, 75	lensymd 8020	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾))) → ¬ (^◡𝐽‘𝐾) < 𝑣)
77	73, 76	pm2.65da 651	. . . . . . . . 9 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ¬ 𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)))
78	77	iffalsed 3530	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → if(𝑣 ∈ (𝐾...(^◡𝐽‘𝐾)), if(𝑣 = 𝐾, 𝐾, (𝐽‘(𝑣 − 1))), (𝐽‘𝑣)) = (𝐽‘𝑣))
79	67, 78	eqtrd 2198	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝑄‘𝑣) = (𝐽‘𝑣))
80	79	fveq2d 5490	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (𝐺‘(𝑄‘𝑣)) = (𝐺‘(𝐽‘𝑣)))
81	33, 34, 11	iseqf1olemqf1o 10428	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → 𝑄:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
82	6	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
83	82	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → ∀𝑥 ∈ (ℤ_≥‘𝑀)(𝐺‘𝑥) ∈ 𝑆)
84	83	r19.21bi 2554	. . . . . . 7 ⊢ ((((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
85	33, 81, 66, 84, 12	iseqf1olemfvp 10432	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝑄‘𝑣)))
86	33, 34, 66, 84, 12	iseqf1olemfvp 10432	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (𝐺‘(𝐽‘𝑣)))
87	80, 85, 86	3eqtr4rd 2209	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑣 ∈ (((^◡𝐽‘𝐾) + 1)...𝑁)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑣) = (⦋𝑄 / 𝑓⦌𝑃‘𝑣))
88	36	ad2antrr 480	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℤ)
89		eluzelz 9475	. . . . . . . 8 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → 𝑥 ∈ ℤ)
90	89	adantl 275	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℤ)
91	42	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ∈ ℝ)
92	46	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ∈ ℝ)
93	90	zred 9313	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ ℝ)
94	57	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ ((^◡𝐽‘𝐾) + 1))
95		eluzle 9478	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1)) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
96	95	adantl 275	. . . . . . . 8 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → ((^◡𝐽‘𝐾) + 1) ≤ 𝑥)
97	91, 92, 93, 94, 96	letrd 8022	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑀 ≤ 𝑥)
98		eluz2 9472	. . . . . . 7 ⊢ (𝑥 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑀 ≤ 𝑥))
99	88, 90, 97, 98	syl3anbrc 1171	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → 𝑥 ∈ (ℤ_≥‘𝑀))
100	7	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝐾 ∈ (𝑀...𝑁))
101	8	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
102	6	adantlr 469	. . . . . . 7 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (𝐺‘𝑥) ∈ 𝑆)
103	100, 101, 11, 102, 12	iseqf1olemjpcl 10430	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
104	99, 103	syldan 280	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
105	7, 8, 11, 6, 12	iseqf1olemqpcl 10431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
106	105	adantlr 469	. . . . . 6 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
107	99, 106	syldan 280	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘((^◡𝐽‘𝐾) + 1))) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
108	1	adantlr 469	. . . . 5 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
109	32, 87, 104, 107, 108	seq3fveq 10406	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
110	14, 109	oveq12d 5860	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
111	3	adantlr 469	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
112		eluz2 9472	. . . . . 6 ⊢ ((^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ (^◡𝐽‘𝐾) ∈ ℤ ∧ 𝐾 ≤ (^◡𝐽‘𝐾)))
113	50, 21, 54, 112	syl3anbrc 1171	. . . . 5 ⊢ (𝜑 → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
114	113	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (^◡𝐽‘𝐾) ∈ (ℤ_≥‘𝐾))
115		simpr 109	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝐾))
116	7	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (𝑀...𝑁))
117		elfzuz 9956	. . . . . . . 8 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ_≥‘𝑀))
118	116, 117	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ (ℤ_≥‘𝑀))
119		uztrn 9482	. . . . . . 7 ⊢ ((𝑥 ∈ (ℤ_≥‘𝐾) ∧ 𝐾 ∈ (ℤ_≥‘𝑀)) → 𝑥 ∈ (ℤ_≥‘𝑀))
120	115, 118, 119	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → 𝑥 ∈ (ℤ_≥‘𝑀))
121	7, 8, 11, 6, 12	iseqf1olemjpcl 10430	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝑀)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
122	120, 121	syldan 280	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
123	122	adantlr 469	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝐽 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
124	108, 111, 32, 114, 123	seq3split 10414	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁)))
125	120, 105	syldan 280	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
126	125	adantlr 469	. . . 4 ⊢ (((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) ∧ 𝑥 ∈ (ℤ_≥‘𝐾)) → (⦋𝑄 / 𝑓⦌𝑃‘𝑥) ∈ 𝑆)
127	108, 111, 32, 114, 126	seq3split 10414	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁) = ((seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) + (seq((^◡𝐽‘𝐾) + 1)( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁)))
128	110, 124, 127	3eqtr4d 2208	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) < 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
129	13	adantr 274	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)))
130		simpr 109	. . . 4 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (^◡𝐽‘𝐾) = 𝑁)
131	130	fveq2d 5490	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁))
132	130	fveq2d 5490	. . 3 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘(^◡𝐽‘𝐾)) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
133	129, 131, 132	3eqtr3d 2206	. 2 ⊢ ((𝜑 ∧ (^◡𝐽‘𝐾) = 𝑁) → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))
134		elfzle2 9963	. . . 4 ⊢ ((^◡𝐽‘𝐾) ∈ (𝑀...𝑁) → (^◡𝐽‘𝐾) ≤ 𝑁)
135	19, 134	syl 14	. . 3 ⊢ (𝜑 → (^◡𝐽‘𝐾) ≤ 𝑁)
136		zleloe 9238	. . . 4 ⊢ (((^◡𝐽‘𝐾) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
137	21, 25, 136	syl2anc 409	. . 3 ⊢ (𝜑 → ((^◡𝐽‘𝐾) ≤ 𝑁 ↔ ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁)))
138	135, 137	mpbid 146	. 2 ⊢ (𝜑 → ((^◡𝐽‘𝐾) < 𝑁 ∨ (^◡𝐽‘𝐾) = 𝑁))
139	128, 133, 138	mpjaodan 788	1 ⊢ (𝜑 → (seq𝐾( + , ⦋𝐽 / 𝑓⦌𝑃)‘𝑁) = (seq𝐾( + , ⦋𝑄 / 𝑓⦌𝑃)‘𝑁))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 ∧ w3a 968 = wceq 1343 ∈ wcel 2136 ≠ wne 2336 ∀wral 2444 ⦋csb 3045 ifcif 3520 class class class wbr 3982 ↦ cmpt 4043 ^◡ccnv 4603 ⟶wf 5184 –1-1-onto→wf1o 5187 ‘cfv 5188 (class class class)co 5842 ℝcr 7752 1c1 7754 + caddc 7756 < clt 7933 ≤ cle 7934 − cmin 8069 ℤcz 9191 ℤ_≥cuz 9466 ...cfz 9944 ..^cfzo 10077 seqcseq 10380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-addcom 7853 ax-addass 7855 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-0id 7861 ax-rnegex 7862 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-1o 6384 df-er 6501 df-en 6707 df-fin 6709 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-inn 8858 df-n0 9115 df-z 9192 df-uz 9467 df-fz 9945 df-fzo 10078 df-seqfrec 10381

This theorem is referenced by: seq3f1olemqsum 10435

W3C validator