Theorem summodclem2a 10989

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

Hypotheses

Ref	Expression
isummo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
isummo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
isummolem2a.dc	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
isummolem2a.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
isummolem2a.h	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
summolem2.5	⊢ (𝜑 → 𝑁 ∈ ℕ)
summolem2.6	⊢ (𝜑 → 𝑀 ∈ ℤ)
summolem2.7	⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))
summolem2.8	⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
summolem2.9	⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))

Assertion

Ref	Expression
summodclem2a	⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

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

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

Proof of Theorem summodclem2a

Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isummo.1	. . 3 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
2		isummo.2	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
3		isummolem2a.dc	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
4		summolem2.7	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))
5		summolem2.9	. . . . . . . 8 ⊢ (𝜑 → 𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴))
6		1zzd 8933	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
7		summolem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9024	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10045	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		summolem2.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10377	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12		nnnn0 8836	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13		hashfz1 10370	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
14	7, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2134	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5722	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5637	. . . . . . . . 9 ⊢ ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
18	16, 17	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
19	5, 18	mpbid 146	. . . . . . 7 ⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴))
20		isof1o 5640	. . . . . . 7 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21	19, 20	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
22		f1of 5301	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
23	21, 22	syl 14	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
24		nnuz 9211	. . . . . . 7 ⊢ ℕ = (ℤ≥‘1)
25	7, 24	syl6eleq 2192	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
26		eluzfz2 9653	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
27	25, 26	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
28	23, 27	ffvelrnd 5488	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
29	4, 28	sseldd 3048	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀))
30	4	sselda 3047	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀))
31		f1ocnvfv2 5611	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
32	21, 31	sylan 279	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
33		f1ocnv 5314	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5301	. . . . . . . . . . . 12 ⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁))
35	21, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelrnda 5487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁))
37		elfzle2 9649	. . . . . . . . . 10 ⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁)
39	19	adantr 272	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 9686	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ≥‘1)
41		uzssz 9195	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘1) ⊆ ℤ
42		zssre 8913	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3056	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘1) ⊆ ℝ
44	40, 43	sstri 3056	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 7681	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ*
46	44, 45	sstri 3056	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆ ℝ*)
48	4	adantr 272	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀))
49		uzssz 9195	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
50	49, 42	sstri 3056	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℝ
51	48, 50	syl6ss 3059	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ)
52	51, 45	syl6ss 3059	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ*)
53	27	adantr 272	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10421	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*) ∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1193	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 3897	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁))
58		eluzelz 9185	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
59	30, 58	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ)
60		eluzelz 9185	. . . . . . . . . 10 ⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ)
61	29, 60	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
62	61	adantr 272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
63		eluz 9189	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
64	59, 62, 63	syl2anc 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
65	57, 64	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))
66		elfzuzb 9641	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)))
67	30, 65, 66	sylanbrc 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))
68	67	ex 114	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁))))
69	68	ssrdv 3053	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
70	1, 2, 3, 29, 69	fsum3cvg 10985	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)))
71		addid2 7772	. . . . 5 ⊢ (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
72	71	adantl 273	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
73		addid1 7771	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
74	73	adantl 273	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
75		addcl 7617	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
76	75	adantl 273	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
77		0cnd 7631	. . . 4 ⊢ (𝜑 → 0 ∈ ℂ)
78	27, 16	eleqtrrd 2179	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
79		iftrue 3426	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
80	79	adantl 273	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
81	80, 2	eqeltrd 2176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
82	81	adantlr 464	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
83	82	adantlr 464	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
84		iffalse 3429	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
85		0cn 7630	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
86	84, 85	syl6eqel 2190	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
87	86	adantl 273	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
88	3	adantlr 464	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
89		exmiddc 788	. . . . . . . . 9 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
90	88, 89	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
91	83, 87, 90	mpjaodan 753	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
92		simpll 499	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝜑)
93		simpr 109	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ (ℤ≥‘𝑀))
94	4	ssneld 3049	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ≥‘𝑀) → ¬ 𝑘 ∈ 𝐴))
95	92, 93, 94	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴)
96	95, 86	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
97		summolem2.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		eluzdc 9254	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
99	97, 98	sylan 279	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
100		exmiddc 788	. . . . . . . 8 ⊢ (DECID 𝑘 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
101	99, 100	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
102	91, 96, 101	mpjaodan 753	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
103	102, 1	fmptd 5506	. . . . 5 ⊢ (𝜑 → 𝐹:ℤ⟶ℂ)
104		eluzelz 9185	. . . . 5 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
105		ffvelrn 5485	. . . . 5 ⊢ ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) ∈ ℂ)
106	103, 104, 105	syl2an 285	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
107		elnnuz 9212	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ≥‘1))
108	107	biimpri 132	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℕ)
109	108	adantl 273	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℕ)
110		isof1o 5640	. . . . . . . . . . . 12 ⊢ (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴)
111		f1of 5301	. . . . . . . . . . . 12 ⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
112	5, 110, 111	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
113	112	ad2antrr 475	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴)
114		1zzd 8933	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ∈ ℤ)
115	15, 8	eqeltrd 2176	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
116	115	ad2antrr 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈ ℤ)
117		eluzelz 9185	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℤ)
118	117	ad2antlr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ)
119	114, 116, 118	3jca 1129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ))
120		eluzle 9188	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 1 ≤ 𝑚)
121	120	ad2antlr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚)
122		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁)
123	15	breq2d 3887	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
124	123	ad2antrr 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
125	122, 124	mpbird 166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴))
126	121, 125	jca 302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))
127		elfz2 9638	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))))
128	119, 126, 127	sylanbrc 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴)))
129	113, 128	ffvelrnd 5488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
130	129	iftrued 3428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	4	ad2antrr 475	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ≥‘𝑀))
132	23	ad2antrr 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴)
133	16	eleq2d 2169	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
134	133	ad2antrr 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
135	128, 134	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁))
136	132, 135	ffvelrnd 5488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
137	131, 136	sseldd 3048	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ≥‘𝑀))
138	49, 137	sseldi 3045	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ)
139	102	ralrimiva 2464	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
140	139	ad2antrr 475	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
141		nfv 1476	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴
142		nfcsb1v 2985	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
143		nfcv 2240	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘0
144	141, 142, 143	nfif 3447	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)
145	144	nfel1 2251	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ
146		eleq1 2162	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴))
147		csbeq1a 2963	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
148	146, 147	ifbieq1d 3441	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
149	148	eleq1d 2168	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
150	145, 149	rspc 2738	. . . . . . . . 9 ⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
151	138, 140, 150	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
152	130, 151	eqeltrrd 2177	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
153		0cnd 7631	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈ ℂ)
154	109	nnzd 9024	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℤ)
155	8	adantr 272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑁 ∈ ℤ)
156		zdcle 8979	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑚 ≤ 𝑁)
157	154, 155, 156	syl2anc 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → DECID 𝑚 ≤ 𝑁)
158	152, 153, 157	ifcldadc 3448	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
159		breq1 3878	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
160		fveq2 5353	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
161	160	csbeq1d 2961	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
162	159, 161	ifbieq1d 3441	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
163		isummolem2a.h	. . . . . . 7 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
164	162, 163	fvmptg 5429	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
165	109, 158, 164	syl2anc 406	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
166	165, 158	eqeltrd 2176	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
167		fveqeq2 5362	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0))
168		eldifi 3145	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
169		elfzelz 9647	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
170	168, 169	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
171		eldifn 3146	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴)
172	171, 84	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
173	172, 85	syl6eqel 2190	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
174	1	fvmpt2 5436	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
175	170, 173, 174	syl2anc 406	. . . . . . 7 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
176	175, 172	eqtrd 2132	. . . . . 6 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0)
177	167, 176	vtoclga 2707	. . . . 5 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0)
178	177	adantl 273	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0)
179	112	ffvelrnda 5487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
180	179	iftrued 3428	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
181	4	adantr 272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀))
182	181, 179	sseldd 3048	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀))
183		eluzelz 9185	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ)
184	182, 183	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
185		simpl 108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑)
186	185, 184	jca 302	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))
187		nfv 1476	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)
188		nfv 1476	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
189		nfcsb1v 2985	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
190	188, 189, 143	nfif 3447	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)
191	190	nfel1 2251	. . . . . . . . 9 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ
192	187, 191	nfim 1519	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
193		eleq1 2162	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ))
194	193	anbi2d 455	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)))
195		eleq1 2162	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
196		csbeq1a 2963	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
197	195, 196	ifbieq1d 3441	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
198	197	eleq1d 2168	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
199	194, 198	imbi12d 233	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)))
200	192, 199, 102	vtoclg1f 2700	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
201	179, 186, 200	sylc 62	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
202		eleq1 2162	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
203		csbeq1 2958	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
204	202, 203	ifbieq1d 3441	. . . . . . 7 ⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
205		nfcv 2240	. . . . . . . . 9 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
206		nfv 1476	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
207		nfcsb1v 2985	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
208	206, 207, 143	nfif 3447	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
209		eleq1 2162	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
210		csbeq1a 2963	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
211	209, 210	ifbieq1d 3441	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
212	205, 208, 211	cbvmpt 3963	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
213	1, 212	eqtri 2120	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
214	204, 213	fvmptg 5429	. . . . . 6 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
215	184, 201, 214	syl2anc 406	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
216		elfznn 9675	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
217	216	adantl 273	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
218		elfzle2 9649	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
219	218	adantl 273	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
220	15	breq2d 3887	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
221	220	adantr 272	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
222	219, 221	mpbid 146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁)
223	222	iftrued 3428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
224	180, 201	eqeltrrd 2177	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
225	223, 224	eqeltrd 2176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
226		breq1 3878	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁))
227		fveq2 5353	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥))
228	227	csbeq1d 2961	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
229	226, 228	ifbieq1d 3441	. . . . . . . 8 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
230	229, 163	fvmptg 5429	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
231	217, 225, 230	syl2anc 406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
232	231, 223	eqtrd 2132	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
233	180, 215, 232	3eqtr4rd 2143	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
234	72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233	seq3coll 10426	. . 3 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
235	15, 7	eqeltrd 2176	. . . . 5 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
236	235, 7	jca 302	. . . 4 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈ ℕ))
237	16	eqcomd 2105	. . . . . 6 ⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴)))
238		f1oeq2 5293	. . . . . 6 ⊢ ((1...𝑁) = (1...(♯‘𝐴)) → (𝑓:(1...𝑁)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))
239	237, 238	syl 14	. . . . 5 ⊢ (𝜑 → (𝑓:(1...𝑁)–1-1-onto→𝐴 ↔ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))
240	10, 239	mpbid 146	. . . 4 ⊢ (𝜑 → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
241		isummolem2a.g	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
242	1, 2, 236, 240, 21, 241, 163	summodclem3 10988	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁))
243	15	fveq2d 5357	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁))
244	234, 242, 243	3eqtr2d 2138	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁))
245	70, 244	breqtrd 3899	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 670  DECID wdc 786   ∧ w3a 930   = wceq 1299   ∈ wcel 1448  ∀wral 2375  ⦋csb 2955   ∖ cdif 3018   ⊆ wss 3021  ifcif 3421   class class class wbr 3875   ↦ cmpt 3929  ^◡ccnv 4476  ⟶wf 5055  –1-1-onto→wf1o 5058  ‘cfv 5059   Isom wiso 5060  (class class class)co 5706  ℂcc 7498  ℝcr 7499  0cc0 7500  1c1 7501   + caddc 7503  ℝ^*cxr 7671   < clt 7672   ≤ cle 7673  ℕcn 8578  ℕ₀cn0 8829  ℤcz 8906  ℤ_≥cuz 9176  ...cfz 9631  seqcseq 10059  ♯chash 10362   ⇝ cli 10886

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-mulrcl 7594  ax-addcom 7595  ax-mulcom 7596  ax-addass 7597  ax-mulass 7598  ax-distr 7599  ax-i2m1 7600  ax-0lt1 7601  ax-1rid 7602  ax-0id 7603  ax-rnegex 7604  ax-precex 7605  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-apti 7610  ax-pre-ltadd 7611  ax-pre-mulgt0 7612  ax-pre-mulext 7613

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-rmo 2383  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-po 4156  df-iso 4157  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-isom 5068  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-reap 8203  df-ap 8210  df-div 8294  df-inn 8579  df-2 8637  df-n0 8830  df-z 8907  df-uz 9177  df-rp 9292  df-fz 9632  df-fzo 9761  df-seqfrec 10060  df-exp 10134  df-ihash 10363  df-cj 10455  df-rsqrt 10610  df-abs 10611  df-clim 10887

This theorem is referenced by:  summodclem2  10990  zsumdc  10992