Theorem summodclem2a 11308

Description: Lemma for summodc 11310. (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 9209	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
7		summolem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9303	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10356	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		summolem2.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10692	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12		nnnn0 9112	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13		hashfz1 10685	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
14	7, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2199	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5852	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5766	. . . . . . . . 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 5769	. . . . . . 7 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21	19, 20	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
22		f1of 5426	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
23	21, 22	syl 14	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
24		nnuz 9492	. . . . . . 7 ⊢ ℕ = (ℤ≥‘1)
25	7, 24	eleqtrdi 2257	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘1))
26		eluzfz2 9957	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘1) → 𝑁 ∈ (1...𝑁))
27	25, 26	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
28	23, 27	ffvelrnd 5615	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
29	4, 28	sseldd 3138	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ≥‘𝑀))
30	4	sselda 3137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ≥‘𝑀))
31		f1ocnvfv2 5740	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
32	21, 31	sylan 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) = 𝑛)
33		f1ocnv 5439	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5426	. . . . . . . . . . . 12 ⊢ (◡𝐾:𝐴–1-1-onto→(1...𝑁) → ◡𝐾:𝐴⟶(1...𝑁))
35	21, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelrnda 5614	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ∈ (1...𝑁))
37		elfzle2 9953	. . . . . . . . . 10 ⊢ ((◡𝐾‘𝑛) ∈ (1...𝑁) → (◡𝐾‘𝑛) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (◡𝐾‘𝑛) ≤ 𝑁)
39	19	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 9990	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ≥‘1)
41		uzssz 9476	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘1) ⊆ ℤ
42		zssre 9189	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3146	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘1) ⊆ ℝ
44	40, 43	sstri 3146	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 7933	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ*
46	44, 45	sstri 3146	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆ ℝ*)
48	4	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ≥‘𝑀))
49		uzssz 9476	. . . . . . . . . . . . 13 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
50	49, 42	sstri 3146	. . . . . . . . . . . 12 ⊢ (ℤ≥‘𝑀) ⊆ ℝ
51	48, 50	sstrdi 3149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ)
52	51, 45	sstrdi 3149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ*)
53	27	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10736	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ*) ∧ ((◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4000	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁))
58		eluzelz 9466	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
59	30, 58	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ)
60		eluzelz 9466	. . . . . . . . . 10 ⊢ ((𝐾‘𝑁) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ)
61	29, 60	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
62	61	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
63		eluz 9470	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
64	59, 62, 63	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
65	57, 64	mpbird 166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ≥‘𝑛))
66		elfzuzb 9945	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ≥‘𝑛)))
67	30, 65, 66	sylanbrc 414	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))
68	67	ex 114	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁))))
69	68	ssrdv 3143	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
70	1, 2, 3, 29, 69	fsum3cvg 11305	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)))
71		addid2 8028	. . . . 5 ⊢ (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
72	71	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
73		addid1 8027	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
74	73	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
75		addcl 7869	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
76	75	adantl 275	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
77		0cnd 7883	. . . 4 ⊢ (𝜑 → 0 ∈ ℂ)
78	27, 16	eleqtrrd 2244	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
79		iftrue 3520	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
80	79	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
81	80, 2	eqeltrd 2241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
82	81	adantlr 469	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
83	82	adantlr 469	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
84		iffalse 3523	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
85		0cn 7882	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
86	84, 85	eqeltrdi 2255	. . . . . . . . 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 3139	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ≥‘𝑀) → ¬ 𝑘 ∈ 𝐴))
95	92, 93, 94	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴)
96	95, 86	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
97		summolem2.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		eluzdc 9539	. . . . . . . . 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 5633	. . . . 5 ⊢ (𝜑 → 𝐹:ℤ⟶ℂ)
104		eluzelz 9466	. . . . 5 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
105		ffvelrn 5612	. . . . 5 ⊢ ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) ∈ ℂ)
106	103, 104, 105	syl2an 287	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
107		elnnuz 9493	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ≥‘1))
108	107	biimpri 132	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℕ)
109	108	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℕ)
110		isof1o 5769	. . . . . . . . . . . 12 ⊢ (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴)
111		f1of 5426	. . . . . . . . . . . 12 ⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
112	5, 110, 111	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
113	112	ad2antrr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴)
114		1zzd 9209	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ∈ ℤ)
115	15, 8	eqeltrd 2241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
116	115	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈ ℤ)
117		eluzelz 9466	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 𝑚 ∈ ℤ)
118	117	ad2antlr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ)
119	114, 116, 118	3jca 1166	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ))
120		eluzle 9469	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ≥‘1) → 1 ≤ 𝑚)
121	120	ad2antlr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚)
122		simpr 109	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁)
123	15	breq2d 3988	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
124	123	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
125	122, 124	mpbird 166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴))
126	121, 125	jca 304	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))
127		elfz2 9942	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))))
128	119, 126, 127	sylanbrc 414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴)))
129	113, 128	ffvelrnd 5615	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
130	129	iftrued 3522	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	4	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ≥‘𝑀))
132	23	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴)
133	16	eleq2d 2234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
134	133	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
135	128, 134	mpbid 146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁))
136	132, 135	ffvelrnd 5615	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
137	131, 136	sseldd 3138	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ≥‘𝑀))
138	49, 137	sseldi 3135	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ)
139	102	ralrimiva 2537	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
140	139	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
141		nfv 1515	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴
142		nfcsb1v 3073	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
143		nfcv 2306	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘0
144	141, 142, 143	nfif 3543	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)
145	144	nfel1 2317	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ
146		eleq1 2227	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴))
147		csbeq1a 3049	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
148	146, 147	ifbieq1d 3537	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
149	148	eleq1d 2233	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
150	145, 149	rspc 2819	. . . . . . . . 9 ⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
151	138, 140, 150	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
152	130, 151	eqeltrrd 2242	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
153		0cnd 7883	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) ∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈ ℂ)
154	109	nnzd 9303	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑚 ∈ ℤ)
155	8	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → 𝑁 ∈ ℤ)
156		zdcle 9258	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑚 ≤ 𝑁)
157	154, 155, 156	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → DECID 𝑚 ≤ 𝑁)
158	152, 153, 157	ifcldadc 3544	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
159		breq1 3979	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
160		fveq2 5480	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
161	160	csbeq1d 3047	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
162	159, 161	ifbieq1d 3537	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
163		isummolem2a.h	. . . . . . 7 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
164	162, 163	fvmptg 5556	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
165	109, 158, 164	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
166	165, 158	eqeltrd 2241	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
167		fveqeq2 5489	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0))
168		eldifi 3239	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
169		elfzelz 9951	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
170	168, 169	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
171		eldifn 3240	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴)
172	171, 84	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
173	172, 85	eqeltrdi 2255	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
174	1	fvmpt2 5563	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
175	170, 173, 174	syl2anc 409	. . . . . . 7 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
176	175, 172	eqtrd 2197	. . . . . 6 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0)
177	167, 176	vtoclga 2787	. . . . 5 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0)
178	177	adantl 275	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0)
179	112	ffvelrnda 5614	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
180	179	iftrued 3522	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
181	4	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀))
182	181, 179	sseldd 3138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ≥‘𝑀))
183		eluzelz 9466	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ (ℤ≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ)
184	182, 183	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
185		simpl 108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑)
186	185, 184	jca 304	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))
187		nfv 1515	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)
188		nfv 1515	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
189		nfcsb1v 3073	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
190	188, 189, 143	nfif 3543	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)
191	190	nfel1 2317	. . . . . . . . 9 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ
192	187, 191	nfim 1559	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
193		eleq1 2227	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ))
194	193	anbi2d 460	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)))
195		eleq1 2227	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
196		csbeq1a 3049	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
197	195, 196	ifbieq1d 3537	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
198	197	eleq1d 2233	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
199	194, 198	imbi12d 233	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)))
200	192, 199, 102	vtoclg1f 2780	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
201	179, 186, 200	sylc 62	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
202		eleq1 2227	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
203		csbeq1 3043	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
204	202, 203	ifbieq1d 3537	. . . . . . 7 ⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
205		nfcv 2306	. . . . . . . . 9 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
206		nfv 1515	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
207		nfcsb1v 3073	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
208	206, 207, 143	nfif 3543	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
209		eleq1 2227	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
210		csbeq1a 3049	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
211	209, 210	ifbieq1d 3537	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
212	205, 208, 211	cbvmpt 4071	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
213	1, 212	eqtri 2185	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
214	204, 213	fvmptg 5556	. . . . . 6 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
215	184, 201, 214	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
216		elfznn 9979	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
217	216	adantl 275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
218		elfzle2 9953	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
219	218	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
220	15	breq2d 3988	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
221	220	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
222	219, 221	mpbid 146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁)
223	222	iftrued 3522	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
224	180, 201	eqeltrrd 2242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
225	223, 224	eqeltrd 2241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
226		breq1 3979	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁))
227		fveq2 5480	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥))
228	227	csbeq1d 3047	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
229	226, 228	ifbieq1d 3537	. . . . . . . 8 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
230	229, 163	fvmptg 5556	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
231	217, 225, 230	syl2anc 409	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
232	231, 223	eqtrd 2197	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
233	180, 215, 232	3eqtr4rd 2208	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
234	72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233	seq3coll 10741	. . 3 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
235	15, 7	eqeltrd 2241	. . . . 5 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
236	235, 7	jca 304	. . . 4 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈ ℕ))
237	16	eqcomd 2170	. . . . . 6 ⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴)))
238		f1oeq2 5416	. . . . . 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 11307	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁))
243	15	fveq2d 5484	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁))
244	234, 242, 243	3eqtr2d 2203	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁))
245	70, 244	breqtrd 4002	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 824   ∧ w3a 967   = wceq 1342   ∈ wcel 2135  ∀wral 2442  ⦋csb 3040   ∖ cdif 3108   ⊆ wss 3111  ifcif 3515   class class class wbr 3976   ↦ cmpt 4037  ^◡ccnv 4597  ⟶wf 5178  –1-1-onto→wf1o 5181  ‘cfv 5182   Isom wiso 5183  (class class class)co 5836  ℂcc 7742  ℝcr 7743  0cc0 7744  1c1 7745   + caddc 7747  ℝ^*cxr 7923   < clt 7924   ≤ cle 7925  ℕcn 8848  ℕ₀cn0 9105  ℤcz 9182  ℤ_≥cuz 9457  ...cfz 9935  seqcseq 10370  ♯chash 10677   ⇝ cli 11205

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4091  ax-sep 4094  ax-nul 4102  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-iinf 4559  ax-cnex 7835  ax-resscn 7836  ax-1cn 7837  ax-1re 7838  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-mulrcl 7843  ax-addcom 7844  ax-mulcom 7845  ax-addass 7846  ax-mulass 7847  ax-distr 7848  ax-i2m1 7849  ax-0lt1 7850  ax-1rid 7851  ax-0id 7852  ax-rnegex 7853  ax-precex 7854  ax-cnre 7855  ax-pre-ltirr 7856  ax-pre-ltwlin 7857  ax-pre-lttrn 7858  ax-pre-apti 7859  ax-pre-ltadd 7860  ax-pre-mulgt0 7861  ax-pre-mulext 7862

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rmo 2450  df-rab 2451  df-v 2723  df-sbc 2947  df-csb 3041  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-nul 3405  df-if 3516  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-int 3819  df-iun 3862  df-br 3977  df-opab 4038  df-mpt 4039  df-tr 4075  df-id 4265  df-po 4268  df-iso 4269  df-iord 4338  df-on 4340  df-ilim 4341  df-suc 4343  df-iom 4562  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-f1 5187  df-fo 5188  df-f1o 5189  df-fv 5190  df-isom 5191  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-1st 6100  df-2nd 6101  df-recs 6264  df-frec 6350  df-1o 6375  df-er 6492  df-en 6698  df-dom 6699  df-fin 6700  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930  df-sub 8062  df-neg 8063  df-reap 8464  df-ap 8471  df-div 8560  df-inn 8849  df-2 8907  df-n0 9106  df-z 9183  df-uz 9458  df-rp 9581  df-fz 9936  df-fzo 10068  df-seqfrec 10371  df-exp 10445  df-ihash 10678  df-cj 10770  df-rsqrt 10926  df-abs 10927  df-clim 11206

This theorem is referenced by:  summodclem2  11309  zsumdc  11311