Theorem summodclem2a 11322

Description: Lemma for summodc 11324. (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 9218	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
7		summolem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9312	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10366	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		summolem2.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10703	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12		nnnn0 9121	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13		hashfz1 10696	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
14	7, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2200	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5858	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5772	. . . . . . . . 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 5775	. . . . . . 7 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21	19, 20	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
22		f1of 5432	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
23	21, 22	syl 14	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
24		nnuz 9501	. . . . . . 7 ⊢ ℕ = (ℤ≥‘1)
25	7, 24	eleqtrdi 2259	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
26		eluzfz2 9967	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
27	25, 26	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
28	23, 27	ffvelrnd 5621	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
29	4, 28	sseldd 3143	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀))
30	4	sselda 3142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀))
31		f1ocnvfv2 5746	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
32	21, 31	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
33		f1ocnv 5445	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5432	. . . . . . . . . . . 12 ⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁))
35	21, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelrnda 5620	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁))
37		elfzle2 9963	. . . . . . . . . 10 ⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁)
39	19	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10000	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ≥‘1)
41		uzssz 9485	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘1) ⊆ ℤ
42		zssre 9198	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3151	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘1) ⊆ ℝ
44	40, 43	sstri 3151	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 7942	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ*
46	44, 45	sstri 3151	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆ ℝ*)
48	4	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀))
49		uzssz 9485	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
50	49, 42	sstri 3151	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℝ
51	48, 50	sstrdi 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ)
52	51, 45	sstrdi 3154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ*)
53	27	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10750	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*) ∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4006	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁))
58		eluzelz 9475	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
59	30, 58	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ)
60		eluzelz 9475	. . . . . . . . . 10 ⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ)
61	29, 60	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
62	61	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
63		eluz 9479	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
64	59, 62, 63	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
65	57, 64	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))
66		elfzuzb 9954	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)))
67	30, 65, 66	sylanbrc 414	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))
68	67	ex 114	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁))))
69	68	ssrdv 3148	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
70	1, 2, 3, 29, 69	fsum3cvg 11319	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)))
71		addid2 8037	. . . . 5 ⊢ (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
72	71	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
73		addid1 8036	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
74	73	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
75		addcl 7878	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
76	75	adantl 275	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
77		0cnd 7892	. . . 4 ⊢ (𝜑 → 0 ∈ ℂ)
78	27, 16	eleqtrrd 2246	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
79		iftrue 3525	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
80	79	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
81	80, 2	eqeltrd 2243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
82	81	adantlr 469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
83	82	adantlr 469	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
84		iffalse 3528	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
85		0cn 7891	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
86	84, 85	eqeltrdi 2257	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
87	86	adantl 275	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
88	3	adantlr 469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
89		exmiddc 826	. . . . . . . . 9 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
90	88, 89	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
91	83, 87, 90	mpjaodan 788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
92		simpll 519	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝜑)
93		simpr 109	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ (ℤ≥‘𝑀))
94	4	ssneld 3144	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ≥‘𝑀) → ¬ 𝑘 ∈ 𝐴))
95	92, 93, 94	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴)
96	95, 86	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
97		summolem2.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		eluzdc 9548	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
99	97, 98	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ≥‘𝑀))
100		exmiddc 826	. . . . . . . 8 ⊢ (DECID 𝑘 ∈ (ℤ≥‘𝑀) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
101	99, 100	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ≥‘𝑀)))
102	91, 96, 101	mpjaodan 788	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
103	102, 1	fmptd 5639	. . . . 5 ⊢ (𝜑 → 𝐹:ℤ⟶ℂ)
104		eluzelz 9475	. . . . 5 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
105		ffvelrn 5618	. . . . 5 ⊢ ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) ∈ ℂ)
106	103, 104, 105	syl2an 287	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
107		elnnuz 9502	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ≥‘1))
108	107	biimpri 132	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℕ)
109	108	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℕ)
110		isof1o 5775	. . . . . . . . . . . 12 ⊢ (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴)
111		f1of 5432	. . . . . . . . . . . 12 ⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
112	5, 110, 111	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
113	112	ad2antrr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴)
114		1zzd 9218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ∈ ℤ)
115	15, 8	eqeltrd 2243	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
116	115	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈ ℤ)
117		eluzelz 9475	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℤ)
118	117	ad2antlr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ)
119	114, 116, 118	3jca 1167	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ))
120		eluzle 9478	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 1 ≤ 𝑚)
121	120	ad2antlr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚)
122		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁)
123	15	breq2d 3994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
124	123	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
125	122, 124	mpbird 166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴))
126	121, 125	jca 304	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))
127		elfz2 9951	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))))
128	119, 126, 127	sylanbrc 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴)))
129	113, 128	ffvelrnd 5621	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
130	129	iftrued 3527	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	4	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ≥‘𝑀))
132	23	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴)
133	16	eleq2d 2236	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
134	133	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
135	128, 134	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁))
136	132, 135	ffvelrnd 5621	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
137	131, 136	sseldd 3143	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ≥‘𝑀))
138	49, 137	sselid 3140	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ)
139	102	ralrimiva 2539	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
140	139	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
141		nfv 1516	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴
142		nfcsb1v 3078	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
143		nfcv 2308	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘0
144	141, 142, 143	nfif 3548	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)
145	144	nfel1 2319	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ
146		eleq1 2229	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴))
147		csbeq1a 3054	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
148	146, 147	ifbieq1d 3542	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
149	148	eleq1d 2235	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
150	145, 149	rspc 2824	. . . . . . . . 9 ⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
151	138, 140, 150	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
152	130, 151	eqeltrrd 2244	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
153		0cnd 7892	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈ ℂ)
154	109	nnzd 9312	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℤ)
155	8	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑁 ∈ ℤ)
156		zdcle 9267	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑚 ≤ 𝑁)
157	154, 155, 156	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → DECID 𝑚 ≤ 𝑁)
158	152, 153, 157	ifcldadc 3549	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
159		breq1 3985	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
160		fveq2 5486	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
161	160	csbeq1d 3052	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
162	159, 161	ifbieq1d 3542	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
163		isummolem2a.h	. . . . . . 7 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
164	162, 163	fvmptg 5562	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
165	109, 158, 164	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
166	165, 158	eqeltrd 2243	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
167		fveqeq2 5495	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0))
168		eldifi 3244	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
169		elfzelz 9960	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
170	168, 169	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
171		eldifn 3245	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴)
172	171, 84	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
173	172, 85	eqeltrdi 2257	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
174	1	fvmpt2 5569	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
175	170, 173, 174	syl2anc 409	. . . . . . 7 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
176	175, 172	eqtrd 2198	. . . . . 6 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0)
177	167, 176	vtoclga 2792	. . . . 5 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0)
178	177	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0)
179	112	ffvelrnda 5620	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
180	179	iftrued 3527	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
181	4	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀))
182	181, 179	sseldd 3143	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀))
183		eluzelz 9475	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ)
184	182, 183	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
185		simpl 108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑)
186	185, 184	jca 304	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))
187		nfv 1516	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)
188		nfv 1516	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
189		nfcsb1v 3078	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
190	188, 189, 143	nfif 3548	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)
191	190	nfel1 2319	. . . . . . . . 9 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ
192	187, 191	nfim 1560	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
193		eleq1 2229	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ))
194	193	anbi2d 460	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)))
195		eleq1 2229	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
196		csbeq1a 3054	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
197	195, 196	ifbieq1d 3542	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
198	197	eleq1d 2235	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
199	194, 198	imbi12d 233	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)))
200	192, 199, 102	vtoclg1f 2785	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
201	179, 186, 200	sylc 62	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
202		eleq1 2229	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
203		csbeq1 3048	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
204	202, 203	ifbieq1d 3542	. . . . . . 7 ⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
205		nfcv 2308	. . . . . . . . 9 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
206		nfv 1516	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
207		nfcsb1v 3078	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
208	206, 207, 143	nfif 3548	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
209		eleq1 2229	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
210		csbeq1a 3054	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
211	209, 210	ifbieq1d 3542	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
212	205, 208, 211	cbvmpt 4077	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
213	1, 212	eqtri 2186	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
214	204, 213	fvmptg 5562	. . . . . 6 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
215	184, 201, 214	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
216		elfznn 9989	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
217	216	adantl 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
218		elfzle2 9963	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
219	218	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
220	15	breq2d 3994	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
221	220	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
222	219, 221	mpbid 146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁)
223	222	iftrued 3527	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
224	180, 201	eqeltrrd 2244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
225	223, 224	eqeltrd 2243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
226		breq1 3985	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁))
227		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥))
228	227	csbeq1d 3052	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
229	226, 228	ifbieq1d 3542	. . . . . . . 8 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
230	229, 163	fvmptg 5562	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
231	217, 225, 230	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
232	231, 223	eqtrd 2198	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
233	180, 215, 232	3eqtr4rd 2209	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
234	72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233	seq3coll 10755	. . 3 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
235	15, 7	eqeltrd 2243	. . . . 5 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
236	235, 7	jca 304	. . . 4 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈ ℕ))
237	16	eqcomd 2171	. . . . . 6 ⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴)))
238		f1oeq2 5422	. . . . . 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 11321	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁))
243	15	fveq2d 5490	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁))
244	234, 242, 243	3eqtr2d 2204	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁))
245	70, 244	breqtrd 4008	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 824   ∧ w3a 968   = wceq 1343   ∈ wcel 2136  ∀wral 2444  ⦋csb 3045   ∖ cdif 3113   ⊆ wss 3116  ifcif 3520   class class class wbr 3982   ↦ cmpt 4043  ^◡ccnv 4603  ⟶wf 5184  –1-1-onto→wf1o 5187  ‘cfv 5188   Isom wiso 5189  (class class class)co 5842  ℂcc 7751  ℝcr 7752  0cc0 7753  1c1 7754   + caddc 7756  ℝ^*cxr 7932   < clt 7933   ≤ cle 7934  ℕcn 8857  ℕ₀cn0 9114  ℤcz 9191  ℤ_≥cuz 9466  ...cfz 9944  seqcseq 10380  ♯chash 10688   ⇝ cli 11219

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-mulrcl 7852  ax-addcom 7853  ax-mulcom 7854  ax-addass 7855  ax-mulass 7856  ax-distr 7857  ax-i2m1 7858  ax-0lt1 7859  ax-1rid 7860  ax-0id 7861  ax-rnegex 7862  ax-precex 7863  ax-cnre 7864  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-apti 7868  ax-pre-ltadd 7869  ax-pre-mulgt0 7870  ax-pre-mulext 7871

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-rmo 2452  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-po 4274  df-iso 4275  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-isom 5197  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-dom 6708  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-reap 8473  df-ap 8480  df-div 8569  df-inn 8858  df-2 8916  df-n0 9115  df-z 9192  df-uz 9467  df-rp 9590  df-fz 9945  df-fzo 10078  df-seqfrec 10381  df-exp 10455  df-ihash 10689  df-cj 10784  df-rsqrt 10940  df-abs 10941  df-clim 11220

This theorem is referenced by:  summodclem2  11323  zsumdc  11325