Theorem summodclem2a 11150

Description: Lemma for summodc 11152. (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 9081	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
7		summolem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9172	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10204	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		summolem2.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10536	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12		nnnn0 8984	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13		hashfz1 10529	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
14	7, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2174	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5790	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5705	. . . . . . . . 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 5708	. . . . . . 7 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21	19, 20	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
22		f1of 5367	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
23	21, 22	syl 14	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
24		nnuz 9361	. . . . . . 7 ⊢ ℕ = (ℤ≥‘1)
25	7, 24	eleqtrdi 2232	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
26		eluzfz2 9812	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
27	25, 26	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
28	23, 27	ffvelrnd 5556	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
29	4, 28	sseldd 3098	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀))
30	4	sselda 3097	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀))
31		f1ocnvfv2 5679	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
32	21, 31	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
33		f1ocnv 5380	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5367	. . . . . . . . . . . 12 ⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁))
35	21, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelrnda 5555	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁))
37		elfzle2 9808	. . . . . . . . . 10 ⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁)
39	19	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 9845	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ≥‘1)
41		uzssz 9345	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘1) ⊆ ℤ
42		zssre 9061	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3106	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘1) ⊆ ℝ
44	40, 43	sstri 3106	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 7809	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ*
46	44, 45	sstri 3106	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆ ℝ*)
48	4	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀))
49		uzssz 9345	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
50	49, 42	sstri 3106	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℝ
51	48, 50	sstrdi 3109	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ)
52	51, 45	sstrdi 3109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ*)
53	27	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10580	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*) ∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1225	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 3952	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁))
58		eluzelz 9335	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
59	30, 58	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ)
60		eluzelz 9335	. . . . . . . . . 10 ⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ)
61	29, 60	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
62	61	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
63		eluz 9339	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
64	59, 62, 63	syl2anc 408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
65	57, 64	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))
66		elfzuzb 9800	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)))
67	30, 65, 66	sylanbrc 413	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))
68	67	ex 114	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁))))
69	68	ssrdv 3103	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
70	1, 2, 3, 29, 69	fsum3cvg 11147	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)))
71		addid2 7901	. . . . 5 ⊢ (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
72	71	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
73		addid1 7900	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
74	73	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
75		addcl 7745	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
76	75	adantl 275	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
77		0cnd 7759	. . . 4 ⊢ (𝜑 → 0 ∈ ℂ)
78	27, 16	eleqtrrd 2219	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
79		iftrue 3479	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
80	79	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
81	80, 2	eqeltrd 2216	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
82	81	adantlr 468	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
83	82	adantlr 468	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
84		iffalse 3482	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
85		0cn 7758	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
86	84, 85	eqeltrdi 2230	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
87	86	adantl 275	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
88	3	adantlr 468	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
89		exmiddc 821	. . . . . . . . 9 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
90	88, 89	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
91	83, 87, 90	mpjaodan 787	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
92		simpll 518	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝜑)
93		simpr 109	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ (ℤ≥‘𝑀))
94	4	ssneld 3099	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ≥‘𝑀) → ¬ 𝑘 ∈ 𝐴))
95	92, 93, 94	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴)
96	95, 86	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
97		summolem2.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		eluzdc 9404	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
99	97, 98	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
100		exmiddc 821	. . . . . . . 8 ⊢ (DECID 𝑘 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
101	99, 100	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
102	91, 96, 101	mpjaodan 787	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
103	102, 1	fmptd 5574	. . . . 5 ⊢ (𝜑 → 𝐹:ℤ⟶ℂ)
104		eluzelz 9335	. . . . 5 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
105		ffvelrn 5553	. . . . 5 ⊢ ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) ∈ ℂ)
106	103, 104, 105	syl2an 287	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
107		elnnuz 9362	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ≥‘1))
108	107	biimpri 132	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℕ)
109	108	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℕ)
110		isof1o 5708	. . . . . . . . . . . 12 ⊢ (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴)
111		f1of 5367	. . . . . . . . . . . 12 ⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
112	5, 110, 111	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
113	112	ad2antrr 479	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴)
114		1zzd 9081	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ∈ ℤ)
115	15, 8	eqeltrd 2216	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
116	115	ad2antrr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈ ℤ)
117		eluzelz 9335	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℤ)
118	117	ad2antlr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ)
119	114, 116, 118	3jca 1161	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ))
120		eluzle 9338	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 1 ≤ 𝑚)
121	120	ad2antlr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚)
122		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁)
123	15	breq2d 3941	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
124	123	ad2antrr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
125	122, 124	mpbird 166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴))
126	121, 125	jca 304	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))
127		elfz2 9797	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))))
128	119, 126, 127	sylanbrc 413	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴)))
129	113, 128	ffvelrnd 5556	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
130	129	iftrued 3481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	4	ad2antrr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ≥‘𝑀))
132	23	ad2antrr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴)
133	16	eleq2d 2209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
134	133	ad2antrr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
135	128, 134	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁))
136	132, 135	ffvelrnd 5556	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
137	131, 136	sseldd 3098	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ≥‘𝑀))
138	49, 137	sseldi 3095	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ)
139	102	ralrimiva 2505	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
140	139	ad2antrr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
141		nfv 1508	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴
142		nfcsb1v 3035	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
143		nfcv 2281	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘0
144	141, 142, 143	nfif 3500	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)
145	144	nfel1 2292	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ
146		eleq1 2202	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴))
147		csbeq1a 3012	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
148	146, 147	ifbieq1d 3494	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
149	148	eleq1d 2208	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
150	145, 149	rspc 2783	. . . . . . . . 9 ⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
151	138, 140, 150	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
152	130, 151	eqeltrrd 2217	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
153		0cnd 7759	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈ ℂ)
154	109	nnzd 9172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℤ)
155	8	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑁 ∈ ℤ)
156		zdcle 9127	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑚 ≤ 𝑁)
157	154, 155, 156	syl2anc 408	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → DECID 𝑚 ≤ 𝑁)
158	152, 153, 157	ifcldadc 3501	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
159		breq1 3932	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
160		fveq2 5421	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
161	160	csbeq1d 3010	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
162	159, 161	ifbieq1d 3494	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
163		isummolem2a.h	. . . . . . 7 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
164	162, 163	fvmptg 5497	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
165	109, 158, 164	syl2anc 408	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
166	165, 158	eqeltrd 2216	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
167		fveqeq2 5430	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0))
168		eldifi 3198	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
169		elfzelz 9806	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
170	168, 169	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
171		eldifn 3199	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴)
172	171, 84	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
173	172, 85	eqeltrdi 2230	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
174	1	fvmpt2 5504	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
175	170, 173, 174	syl2anc 408	. . . . . . 7 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
176	175, 172	eqtrd 2172	. . . . . 6 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0)
177	167, 176	vtoclga 2752	. . . . 5 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0)
178	177	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0)
179	112	ffvelrnda 5555	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
180	179	iftrued 3481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
181	4	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀))
182	181, 179	sseldd 3098	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀))
183		eluzelz 9335	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ)
184	182, 183	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
185		simpl 108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑)
186	185, 184	jca 304	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))
187		nfv 1508	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)
188		nfv 1508	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
189		nfcsb1v 3035	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
190	188, 189, 143	nfif 3500	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)
191	190	nfel1 2292	. . . . . . . . 9 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ
192	187, 191	nfim 1551	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
193		eleq1 2202	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ))
194	193	anbi2d 459	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)))
195		eleq1 2202	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
196		csbeq1a 3012	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
197	195, 196	ifbieq1d 3494	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
198	197	eleq1d 2208	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
199	194, 198	imbi12d 233	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)))
200	192, 199, 102	vtoclg1f 2745	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
201	179, 186, 200	sylc 62	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
202		eleq1 2202	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
203		csbeq1 3006	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
204	202, 203	ifbieq1d 3494	. . . . . . 7 ⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
205		nfcv 2281	. . . . . . . . 9 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
206		nfv 1508	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
207		nfcsb1v 3035	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
208	206, 207, 143	nfif 3500	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
209		eleq1 2202	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
210		csbeq1a 3012	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
211	209, 210	ifbieq1d 3494	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
212	205, 208, 211	cbvmpt 4023	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
213	1, 212	eqtri 2160	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
214	204, 213	fvmptg 5497	. . . . . 6 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
215	184, 201, 214	syl2anc 408	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
216		elfznn 9834	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
217	216	adantl 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
218		elfzle2 9808	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
219	218	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
220	15	breq2d 3941	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
221	220	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
222	219, 221	mpbid 146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁)
223	222	iftrued 3481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
224	180, 201	eqeltrrd 2217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
225	223, 224	eqeltrd 2216	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
226		breq1 3932	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁))
227		fveq2 5421	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥))
228	227	csbeq1d 3010	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
229	226, 228	ifbieq1d 3494	. . . . . . . 8 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
230	229, 163	fvmptg 5497	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
231	217, 225, 230	syl2anc 408	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
232	231, 223	eqtrd 2172	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
233	180, 215, 232	3eqtr4rd 2183	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
234	72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233	seq3coll 10585	. . 3 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
235	15, 7	eqeltrd 2216	. . . . 5 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
236	235, 7	jca 304	. . . 4 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈ ℕ))
237	16	eqcomd 2145	. . . . . 6 ⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴)))
238		f1oeq2 5357	. . . . . 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 11149	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁))
243	15	fveq2d 5425	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁))
244	234, 242, 243	3eqtr2d 2178	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁))
245	70, 244	breqtrd 3954	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  ∀wral 2416  ⦋csb 3003   ∖ cdif 3068   ⊆ wss 3071  ifcif 3474   class class class wbr 3929   ↦ cmpt 3989  ^◡ccnv 4538  ⟶wf 5119  –1-1-onto→wf1o 5122  ‘cfv 5123   Isom wiso 5124  (class class class)co 5774  ℂcc 7618  ℝcr 7619  0cc0 7620  1c1 7621   + caddc 7623  ℝ^*cxr 7799   < clt 7800   ≤ cle 7801  ℕcn 8720  ℕ₀cn0 8977  ℤcz 9054  ℤ_≥cuz 9326  ...cfz 9790  seqcseq 10218  ♯chash 10521   ⇝ cli 11047

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-mulrcl 7719  ax-addcom 7720  ax-mulcom 7721  ax-addass 7722  ax-mulass 7723  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-1rid 7727  ax-0id 7728  ax-rnegex 7729  ax-precex 7730  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-apti 7735  ax-pre-ltadd 7736  ax-pre-mulgt0 7737  ax-pre-mulext 7738

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-1o 6313  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-reap 8337  df-ap 8344  df-div 8433  df-inn 8721  df-2 8779  df-n0 8978  df-z 9055  df-uz 9327  df-rp 9442  df-fz 9791  df-fzo 9920  df-seqfrec 10219  df-exp 10293  df-ihash 10522  df-cj 10614  df-rsqrt 10770  df-abs 10771  df-clim 11048

This theorem is referenced by:  summodclem2  11151  zsumdc  11153