Theorem summodclem3 10988

Description: Lemma for summodc 10991. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

Hypotheses

Ref	Expression
isummo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
isummo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
isummolem3.5	⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
isummolem3.6	⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
isummolem3.7	⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
isummolem3.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
isummolem3.4	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))

Assertion

Ref	Expression
summodclem3	⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))

Distinct variable groups:   𝑘,𝑛,𝐴   𝑛,𝐹   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛   𝑘,𝑀,𝑛   𝐵,𝑛   𝑘,𝐾,𝑛   𝑓,𝑘,𝑛

Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑓,𝑘)   𝐹(𝑓,𝑘)   𝐺(𝑓,𝑘,𝑛)   𝐻(𝑓,𝑘,𝑛)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem summodclem3

Dummy variables 𝑖 𝑗 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		addcl 7617	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) ∈ ℂ)
2	1	adantl 273	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) ∈ ℂ)
3		addcom 7770	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
4	3	adantl 273	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 + 𝑗) = (𝑗 + 𝑚))
5		addass 7622	. . . 4 ⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
6	5	adantl 273	. . 3 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑚 + 𝑗) + 𝑦) = (𝑚 + (𝑗 + 𝑦)))
7		isummolem3.5	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ))
8	7	simpld 111	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
9		nnuz 9211	. . . 4 ⊢ ℕ = (ℤ≥‘1)
10	8, 9	syl6eleq 2192	. . 3 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
11		isummolem3.6	. . . . . 6 ⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴)
12		f1ocnv 5314	. . . . . 6 ⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀))
13	11, 12	syl 14	. . . . 5 ⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀))
14		isummolem3.7	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
15		f1oco 5324	. . . . 5 ⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
16	13, 14, 15	syl2anc 406	. . . 4 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))
17		isummo.1	. . . . . . . 8 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
18		isummo.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
19	17, 18, 7, 11, 14	isummolemnm 10987	. . . . . . 7 ⊢ (𝜑 → 𝑁 = 𝑀)
20	19	eqcomd 2105	. . . . . 6 ⊢ (𝜑 → 𝑀 = 𝑁)
21	20	oveq2d 5722	. . . . 5 ⊢ (𝜑 → (1...𝑀) = (1...𝑁))
22		f1oeq2 5293	. . . . 5 ⊢ ((1...𝑀) = (1...𝑁) → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)))
23	21, 22	syl 14	. . . 4 ⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)))
24	16, 23	mpbird 166	. . 3 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀))
25		elnnuz 9212	. . . 4 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ≥‘1))
26		isummolem3.g	. . . . . . 7 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
27		breq1 3878	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑀 ↔ 𝑚 ≤ 𝑀))
28		fveq2 5353	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
29	28	csbeq1d 2961	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
30	27, 29	ifbieq1d 3441	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0))
31		simplr 500	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ)
32		elfzle2 9649	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ≤ 𝑀)
33	32	adantl 273	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ≤ 𝑀)
34	33	iftrued 3428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
35		f1of 5301	. . . . . . . . . . . 12 ⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴)
36	11, 35	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴)
37	36	ffvelrnda 5487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴)
38	18	ralrimiva 2464	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
39	38	adantr 272	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
40		nfcsb1v 2985	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵
41	40	nfel1 2251	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
42		csbeq1a 2963	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵)
43	42	eleq1d 2168	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
44	41, 43	rspc 2738	. . . . . . . . . 10 ⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
45	37, 39, 44	sylc 62	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
46	45	adantlr 464	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
47	34, 46	eqeltrd 2176	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
48	26, 30, 31, 47	fvmptd3 5446	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0))
49	48, 47	eqeltrd 2176	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ)
50		simplr 500	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑚 ∈ ℕ)
51	8	ad2antrr 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℕ)
52	51	nnzd 9024	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
53		eluzp1l 9200	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑚)
54	52, 53	sylancom 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑚)
55	50	nnzd 9024	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑚 ∈ ℤ)
56		zltnle 8952	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑀))
57	52, 55, 56	syl2anc 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 < 𝑚 ↔ ¬ 𝑚 ≤ 𝑀))
58	54, 57	mpbid 146	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → ¬ 𝑚 ≤ 𝑀)
59	58	iffalsed 3431	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) = 0)
60		0cn 7630	. . . . . . . 8 ⊢ 0 ∈ ℂ
61	59, 60	syl6eqel 2190	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
62	26, 30, 50, 61	fvmptd3 5446	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐺‘𝑚) = if(𝑚 ≤ 𝑀, ⦋(𝑓‘𝑚) / 𝑘⦌𝐵, 0))
63	62, 61	eqeltrd 2176	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐺‘𝑚) ∈ ℂ)
64		nnsplit 9755	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ℕ = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
65	8, 64	syl 14	. . . . . . . 8 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
66	65	eleq2d 2169	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ ↔ 𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))))
67	66	biimpa 292	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
68		elun 3164	. . . . . 6 ⊢ (𝑚 ∈ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))))
69	67, 68	sylib 121	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑀) ∨ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))))
70	49, 63, 69	mpjaodan 753	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℂ)
71	25, 70	sylan2br 284	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐺‘𝑚) ∈ ℂ)
72	19	oveq2d 5722	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) = (1...𝑀))
73	72	eleq2d 2169	. . . . . . . 8 ⊢ (𝜑 → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀)))
74	73	adantr 272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ (1...𝑁) ↔ 𝑚 ∈ (1...𝑀)))
75	74	pm5.32i 445	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) ↔ ((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)))
76		isummolem3.4	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
77		breq1 3878	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
78		fveq2 5353	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
79	78	csbeq1d 2961	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
80	77, 79	ifbieq1d 3441	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
81		simplr 500	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ∈ ℕ)
82		elfzle2 9649	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...𝑁) → 𝑚 ≤ 𝑁)
83	82	adantl 273	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → 𝑚 ≤ 𝑁)
84	83	iftrued 3428	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
85		f1of 5301	. . . . . . . . . . . . 13 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
86	14, 85	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
87	86	ffvelrnda 5487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → (𝐾‘𝑚) ∈ 𝐴)
88	38	adantr 272	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
89		nfcsb1v 2985	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
90	89	nfel1 2251	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ
91		csbeq1a 2963	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
92	91	eleq1d 2168	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
93	90, 92	rspc 2738	. . . . . . . . . . 11 ⊢ ((𝐾‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ))
94	87, 88, 93	sylc 62	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑁)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
95	94	adantlr 464	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
96	84, 95	eqeltrd 2176	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
97	76, 80, 81, 96	fvmptd3 5446	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
98	97, 96	eqeltrd 2176	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑁)) → (𝐻‘𝑚) ∈ ℂ)
99	75, 98	sylbir 134	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑀)) → (𝐻‘𝑚) ∈ ℂ)
100	19	breq2d 3887	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑚 ≤ 𝑁 ↔ 𝑚 ≤ 𝑀))
101	100	notbid 633	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝑚 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑀))
102	101	ad2antrr 475	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (¬ 𝑚 ≤ 𝑁 ↔ ¬ 𝑚 ≤ 𝑀))
103	58, 102	mpbird 166	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → ¬ 𝑚 ≤ 𝑁)
104	103	iffalsed 3431	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = 0)
105	104, 60	syl6eqel 2190	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
106	76, 80, 50, 105	fvmptd3 5446	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
107	106, 105	eqeltrd 2176	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐻‘𝑚) ∈ ℂ)
108	99, 107, 69	mpjaodan 753	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ∈ ℂ)
109	25, 108	sylan2br 284	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
110		f1oeq2 5293	. . . . . . . . . . 11 ⊢ ((1...𝑀) = (1...𝑁) → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴))
111	21, 110	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴))
112	14, 111	mpbird 166	. . . . . . . . 9 ⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴)
113		f1of 5301	. . . . . . . . 9 ⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴)
114	112, 113	syl 14	. . . . . . . 8 ⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴)
115		fvco3 5424	. . . . . . . 8 ⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖)))
116	114, 115	sylan 279	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖)))
117	116	fveq2d 5357	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖))))
118	11	adantr 272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴)
119	114	ffvelrnda 5487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴)
120		f1ocnvfv2 5611	. . . . . . 7 ⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖))
121	118, 119, 120	syl2anc 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖))
122	117, 121	eqtr2d 2133	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)))
123	122	csbeq1d 2961	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
124		elfznn 9675	. . . . . 6 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ)
125		elfzle2 9649	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
126	125	adantl 273	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ 𝑀)
127	20	breq2d 3887	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ≤ 𝑀 ↔ 𝑖 ≤ 𝑁))
128	127	adantr 272	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑖 ≤ 𝑀 ↔ 𝑖 ≤ 𝑁))
129	126, 128	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ≤ 𝑁)
130	129	iftrued 3428	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
131	38	adantr 272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
132		nfcsb1v 2985	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵
133	132	nfel1 2251	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ
134		csbeq1a 2963	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑖) → 𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
135	134	eleq1d 2168	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑖) → (𝐵 ∈ ℂ ↔ ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ))
136	133, 135	rspc 2738	. . . . . . . 8 ⊢ ((𝐾‘𝑖) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ))
137	119, 131, 136	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝐾‘𝑖) / 𝑘⦌𝐵 ∈ ℂ)
138	130, 137	eqeltrd 2176	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) ∈ ℂ)
139		breq1 3878	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ 𝑁 ↔ 𝑖 ≤ 𝑁))
140		fveq2 5353	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → (𝐾‘𝑛) = (𝐾‘𝑖))
141	140	csbeq1d 2961	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
142	139, 141	ifbieq1d 3441	. . . . . . 7 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0))
143	142, 76	fvmptg 5429	. . . . . 6 ⊢ ((𝑖 ∈ ℕ ∧ if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑖) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0))
144	124, 138, 143	syl2an2 564	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = if(𝑖 ≤ 𝑁, ⦋(𝐾‘𝑖) / 𝑘⦌𝐵, 0))
145	144, 130	eqtrd 2132	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
146		breq1 3878	. . . . . . 7 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑛 ≤ 𝑀 ↔ ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀))
147		fveq2 5353	. . . . . . . 8 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑛) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)))
148	147	csbeq1d 2961	. . . . . . 7 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
149	146, 148	ifbieq1d 3441	. . . . . 6 ⊢ (𝑛 = ((◡𝑓 ∘ 𝐾)‘𝑖) → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0))
150		f1of 5301	. . . . . . . . 9 ⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀))
151	24, 150	syl 14	. . . . . . . 8 ⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀))
152	151	ffvelrnda 5487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀))
153		elfznn 9675	. . . . . . 7 ⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ)
154	152, 153	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ)
155		elfzle2 9649	. . . . . . . . . 10 ⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀)
156	152, 155	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀)
157	156	iftrued 3428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
158	157, 123	eqtr4d 2135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵)
159	158, 137	eqeltrd 2176	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0) ∈ ℂ)
160	26, 149, 154, 159	fvmptd3 5446	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = if(((◡𝑓 ∘ 𝐾)‘𝑖) ≤ 𝑀, ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵, 0))
161	160, 157	eqtrd 2132	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)
162	123, 145, 161	3eqtr4d 2142	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)))
163	2, 4, 6, 10, 24, 71, 109, 162	seq3f1o 10118	. 2 ⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐺)‘𝑀))
164	20	fveq2d 5357	. 2 ⊢ (𝜑 → (seq1( + , 𝐻)‘𝑀) = (seq1( + , 𝐻)‘𝑁))
165	163, 164	eqtr3d 2134	1 ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , 𝐻)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 670   ∧ w3a 930   = wceq 1299   ∈ wcel 1448  ∀wral 2375  ⦋csb 2955   ∪ cun 3019  ifcif 3421   class class class wbr 3875   ↦ cmpt 3929  ^◡ccnv 4476   ∘ ccom 4481  ⟶wf 5055  –1-1-onto→wf1o 5058  ‘cfv 5059  (class class class)co 5706  ℂcc 7498  0cc0 7500  1c1 7501   + caddc 7503   < clt 7672   ≤ cle 7673  ℕcn 8578  ℤcz 8906  ℤ_≥cuz 9176  ...cfz 9631  seqcseq 10059

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-coll 3983  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0lt1 7601  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-apti 7610  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-csb 2956  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-iun 3762  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-ilim 4229  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-f1 5064  df-fo 5065  df-f1o 5066  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1st 5969  df-2nd 5970  df-recs 6132  df-frec 6218  df-1o 6243  df-er 6359  df-en 6565  df-dom 6566  df-fin 6567  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-le 7678  df-sub 7806  df-neg 7807  df-inn 8579  df-n0 8830  df-z 8907  df-uz 9177  df-fz 9632  df-fzo 9761  df-seqfrec 10060  df-ihash 10363

This theorem is referenced by:  summodclem2a  10989  summodc  10991