summodclem2a - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > summodclem2a		GIF version

Theorem summodclem2a 11391

Description: Lemma for summodc 11393. (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 9282	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
7		summolem2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	nnzd 9376	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9	6, 8	fzfigd 10433	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10		summolem2.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑓:(1...𝑁)–1-1-onto→𝐴)
11	9, 10	fihasheqf1od 10771	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘𝐴))
12		nnnn0 9185	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
13		hashfz1 10765	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
14	7, 12, 13	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
15	11, 14	eqtr3d 2212	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐴) = 𝑁)
16	15	oveq2d 5893	. . . . . . . . 9 ⊢ (𝜑 → (1...(♯‘𝐴)) = (1...𝑁))
17		isoeq4 5807	. . . . . . . . 9 ⊢ ((1...(♯‘𝐴)) = (1...𝑁) → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
18	16, 17	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) ↔ 𝐾 Isom < , < ((1...𝑁), 𝐴)))
19	5, 18	mpbid 147	. . . . . . 7 ⊢ (𝜑 → 𝐾 Isom < , < ((1...𝑁), 𝐴))
20		isof1o 5810	. . . . . . 7 ⊢ (𝐾 Isom < , < ((1...𝑁), 𝐴) → 𝐾:(1...𝑁)–1-1-onto→𝐴)
21	19, 20	syl 14	. . . . . 6 ⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴)
22		f1of 5463	. . . . . 6 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → 𝐾:(1...𝑁)⟶𝐴)
23	21, 22	syl 14	. . . . 5 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶𝐴)
24		nnuz 9565	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
25	7, 24	eleqtrdi 2270	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
26		eluzfz2 10034	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
27	25, 26	syl 14	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
28	23, 27	ffvelcdmd 5654	. . . 4 ⊢ (𝜑 → (𝐾‘𝑁) ∈ 𝐴)
29	4, 28	sseldd 3158	. . 3 ⊢ (𝜑 → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑀))
30	4	sselda 3157	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℤ_≥‘𝑀))
31		f1ocnvfv2 5781	. . . . . . . . 9 ⊢ ((𝐾:(1...𝑁)–1-1-onto→𝐴 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑛)) = 𝑛)
32	21, 31	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑛)) = 𝑛)
33		f1ocnv 5476	. . . . . . . . . . . 12 ⊢ (𝐾:(1...𝑁)–1-1-onto→𝐴 → ^◡𝐾:𝐴–1-1-onto→(1...𝑁))
34		f1of 5463	. . . . . . . . . . . 12 ⊢ (^◡𝐾:𝐴–1-1-onto→(1...𝑁) → ^◡𝐾:𝐴⟶(1...𝑁))
35	21, 33, 34	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ^◡𝐾:𝐴⟶(1...𝑁))
36	35	ffvelcdmda 5653	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (^◡𝐾‘𝑛) ∈ (1...𝑁))
37		elfzle2 10030	. . . . . . . . . 10 ⊢ ((^◡𝐾‘𝑛) ∈ (1...𝑁) → (^◡𝐾‘𝑛) ≤ 𝑁)
38	36, 37	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (^◡𝐾‘𝑛) ≤ 𝑁)
39	19	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐾 Isom < , < ((1...𝑁), 𝐴))
40		fzssuz 10067	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
41		uzssz 9549	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘1) ⊆ ℤ
42		zssre 9262	. . . . . . . . . . . . . 14 ⊢ ℤ ⊆ ℝ
43	41, 42	sstri 3166	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘1) ⊆ ℝ
44	40, 43	sstri 3166	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℝ
45		ressxr 8003	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℝ^*
46	44, 45	sstri 3166	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℝ^*
47	46	a1i 9	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1...𝑁) ⊆ ℝ^*)
48	4	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ (ℤ_≥‘𝑀))
49		uzssz 9549	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
50	49, 42	sstri 3166	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
51	48, 50	sstrdi 3169	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ)
52	51, 45	sstrdi 3169	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐴 ⊆ ℝ^*)
53	27	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑁 ∈ (1...𝑁))
54		leisorel 10819	. . . . . . . . . 10 ⊢ ((𝐾 Isom < , < ((1...𝑁), 𝐴) ∧ ((1...𝑁) ⊆ ℝ^* ∧ 𝐴 ⊆ ℝ^*) ∧ ((^◡𝐾‘𝑛) ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → ((^◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
55	39, 47, 52, 36, 53, 54	syl122anc 1247	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((^◡𝐾‘𝑛) ≤ 𝑁 ↔ (𝐾‘(^◡𝐾‘𝑛)) ≤ (𝐾‘𝑁)))
56	38, 55	mpbid 147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘(^◡𝐾‘𝑛)) ≤ (𝐾‘𝑁))
57	32, 56	eqbrtrrd 4029	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ≤ (𝐾‘𝑁))
58		eluzelz 9539	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
59	30, 58	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℤ)
60		eluzelz 9539	. . . . . . . . . 10 ⊢ ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑀) → (𝐾‘𝑁) ∈ ℤ)
61	29, 60	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝐾‘𝑁) ∈ ℤ)
62	61	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ ℤ)
63		eluz 9543	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ (𝐾‘𝑁) ∈ ℤ) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
64	59, 62, 63	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((𝐾‘𝑁) ∈ (ℤ_≥‘𝑛) ↔ 𝑛 ≤ (𝐾‘𝑁)))
65	57, 64	mpbird 167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐾‘𝑁) ∈ (ℤ_≥‘𝑛))
66		elfzuzb 10021	. . . . . 6 ⊢ (𝑛 ∈ (𝑀...(𝐾‘𝑁)) ↔ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ (𝐾‘𝑁) ∈ (ℤ_≥‘𝑛)))
67	30, 65, 66	sylanbrc 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ (𝑀...(𝐾‘𝑁)))
68	67	ex 115	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝐴 → 𝑛 ∈ (𝑀...(𝐾‘𝑁))))
69	68	ssrdv 3163	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝑀...(𝐾‘𝑁)))
70	1, 2, 3, 29, 69	fsum3cvg 11388	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)))
71		addlid 8098	. . . . 5 ⊢ (𝑚 ∈ ℂ → (0 + 𝑚) = 𝑚)
72	71	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (0 + 𝑚) = 𝑚)
73		addid1 8097	. . . . 5 ⊢ (𝑚 ∈ ℂ → (𝑚 + 0) = 𝑚)
74	73	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℂ) → (𝑚 + 0) = 𝑚)
75		addcl 7938	. . . . 5 ⊢ ((𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑚 + 𝑥) ∈ ℂ)
76	75	adantl 277	. . . 4 ⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑚 + 𝑥) ∈ ℂ)
77		0cnd 7952	. . . 4 ⊢ (𝜑 → 0 ∈ ℂ)
78	27, 16	eleqtrrd 2257	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))
79		iftrue 3541	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
80	79	adantl 277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 𝐵)
81	80, 2	eqeltrd 2254	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
82	81	adantlr 477	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
83	82	adantlr 477	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
84		iffalse 3544	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
85		0cn 7951	. . . . . . . . . 10 ⊢ 0 ∈ ℂ
86	84, 85	eqeltrdi 2268	. . . . . . . . 9 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
87	86	adantl 277	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
88	3	adantlr 477	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → DECID 𝑘 ∈ 𝐴)
89		exmiddc 836	. . . . . . . . 9 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
90	88, 89	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
91	83, 87, 90	mpjaodan 798	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
92		simpll 527	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)) → 𝜑)
93		simpr 110	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑘 ∈ (ℤ_≥‘𝑀))
94	4	ssneld 3159	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝑘 ∈ (ℤ_≥‘𝑀) → ¬ 𝑘 ∈ 𝐴))
95	92, 93, 94	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑘 ∈ 𝐴)
96	95, 86	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
97		summolem2.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℤ)
98		eluzdc 9612	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ_≥‘𝑀))
99	97, 98	sylan 283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ (ℤ_≥‘𝑀))
100		exmiddc 836	. . . . . . . 8 ⊢ (DECID 𝑘 ∈ (ℤ_≥‘𝑀) → (𝑘 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)))
101	99, 100	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑘 ∈ (ℤ_≥‘𝑀)))
102	91, 96, 101	mpjaodan 798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
103	102, 1	fmptd 5672	. . . . 5 ⊢ (𝜑 → 𝐹:ℤ⟶ℂ)
104		eluzelz 9539	. . . . 5 ⊢ (𝑚 ∈ (ℤ_≥‘𝑀) → 𝑚 ∈ ℤ)
105		ffvelcdm 5651	. . . . 5 ⊢ ((𝐹:ℤ⟶ℂ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) ∈ ℂ)
106	103, 104, 105	syl2an 289	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑚) ∈ ℂ)
107		elnnuz 9566	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ ↔ 𝑚 ∈ (ℤ_≥‘1))
108	107	biimpri 133	. . . . . . 7 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℕ)
109	108	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℕ)
110		isof1o 5810	. . . . . . . . . . . 12 ⊢ (𝐾 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴)
111		f1of 5463	. . . . . . . . . . . 12 ⊢ (𝐾:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
112	5, 110, 111	3syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾:(1...(♯‘𝐴))⟶𝐴)
113	112	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...(♯‘𝐴))⟶𝐴)
114		1zzd 9282	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ∈ ℤ)
115	15, 8	eqeltrd 2254	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
116	115	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (♯‘𝐴) ∈ ℤ)
117		eluzelz 9539	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 𝑚 ∈ ℤ)
118	117	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ ℤ)
119	114, 116, 118	3jca 1177	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ))
120		eluzle 9542	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (ℤ_≥‘1) → 1 ≤ 𝑚)
121	120	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 1 ≤ 𝑚)
122		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ 𝑁)
123	15	breq2d 4017	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
124	123	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ≤ (♯‘𝐴) ↔ 𝑚 ≤ 𝑁))
125	122, 124	mpbird 167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ≤ (♯‘𝐴))
126	121, 125	jca 306	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴)))
127		elfz2 10017	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (1 ≤ 𝑚 ∧ 𝑚 ≤ (♯‘𝐴))))
128	119, 126, 127	sylanbrc 417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...(♯‘𝐴)))
129	113, 128	ffvelcdmd 5654	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
130	129	iftrued 3543	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
131	4	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐴 ⊆ (ℤ_≥‘𝑀))
132	23	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝐾:(1...𝑁)⟶𝐴)
133	16	eleq2d 2247	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
134	133	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝑚 ∈ (1...(♯‘𝐴)) ↔ 𝑚 ∈ (1...𝑁)))
135	128, 134	mpbid 147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → 𝑚 ∈ (1...𝑁))
136	132, 135	ffvelcdmd 5654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ 𝐴)
137	131, 136	sseldd 3158	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ (ℤ_≥‘𝑀))
138	49, 137	sselid 3155	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → (𝐾‘𝑚) ∈ ℤ)
139	102	ralrimiva 2550	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
140	139	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
141		nfv 1528	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(𝐾‘𝑚) ∈ 𝐴
142		nfcsb1v 3092	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋(𝐾‘𝑚) / 𝑘⦌𝐵
143		nfcv 2319	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘0
144	141, 142, 143	nfif 3564	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0)
145	144	nfel1 2330	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ
146		eleq1 2240	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑚) ∈ 𝐴))
147		csbeq1a 3068	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐾‘𝑚) → 𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
148	146, 147	ifbieq1d 3558	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑚) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
149	148	eleq1d 2246	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑚) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
150	145, 149	rspc 2837	. . . . . . . . 9 ⊢ ((𝐾‘𝑚) ∈ ℤ → (∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ))
151	138, 140, 150	sylc 62	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → if((𝐾‘𝑚) ∈ 𝐴, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
152	130, 151	eqeltrrd 2255	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ 𝑚 ≤ 𝑁) → ⦋(𝐾‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)
153		0cnd 7952	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑚 ≤ 𝑁) → 0 ∈ ℂ)
154	109	nnzd 9376	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑚 ∈ ℤ)
155	8	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → 𝑁 ∈ ℤ)
156		zdcle 9331	. . . . . . . 8 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑚 ≤ 𝑁)
157	154, 155, 156	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → DECID 𝑚 ≤ 𝑁)
158	152, 153, 157	ifcldadc 3565	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ)
159		breq1 4008	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑛 ≤ 𝑁 ↔ 𝑚 ≤ 𝑁))
160		fveq2 5517	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚))
161	160	csbeq1d 3066	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑚) / 𝑘⦌𝐵)
162	159, 161	ifbieq1d 3558	. . . . . . 7 ⊢ (𝑛 = 𝑚 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
163		isummolem2a.h	. . . . . . 7 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0))
164	162, 163	fvmptg 5594	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
165	109, 158, 164	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) = if(𝑚 ≤ 𝑁, ⦋(𝐾‘𝑚) / 𝑘⦌𝐵, 0))
166	165, 158	eqeltrd 2254	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘1)) → (𝐻‘𝑚) ∈ ℂ)
167		fveqeq2 5526	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((𝐹‘𝑘) = 0 ↔ (𝐹‘𝑚) = 0))
168		eldifi 3259	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))))
169		elfzelz 10027	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝑀...(𝐾‘(♯‘𝐴))) → 𝑘 ∈ ℤ)
170	168, 169	syl 14	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → 𝑘 ∈ ℤ)
171		eldifn 3260	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → ¬ 𝑘 ∈ 𝐴)
172	171, 84	syl 14	. . . . . . . . 9 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) = 0)
173	172, 85	eqeltrdi 2268	. . . . . . . 8 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
174	1	fvmpt2 5601	. . . . . . . 8 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
175	170, 173, 174	syl2anc 411	. . . . . . 7 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
176	175, 172	eqtrd 2210	. . . . . 6 ⊢ (𝑘 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑘) = 0)
177	167, 176	vtoclga 2805	. . . . 5 ⊢ (𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴) → (𝐹‘𝑚) = 0)
178	177	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((𝑀...(𝐾‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑚) = 0)
179	112	ffvelcdmda 5653	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ 𝐴)
180	179	iftrued 3543	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
181	4	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
182	181, 179	sseldd 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ (ℤ_≥‘𝑀))
183		eluzelz 9539	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ (ℤ_≥‘𝑀) → (𝐾‘𝑥) ∈ ℤ)
184	182, 183	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐾‘𝑥) ∈ ℤ)
185		simpl 109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝜑)
186	185, 184	jca 306	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ))
187		nfv 1528	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)
188		nfv 1528	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝐾‘𝑥) ∈ 𝐴
189		nfcsb1v 3092	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(𝐾‘𝑥) / 𝑘⦌𝐵
190	188, 189, 143	nfif 3564	. . . . . . . . . 10 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0)
191	190	nfel1 2330	. . . . . . . . 9 ⊢ Ⅎ𝑘if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ
192	187, 191	nfim 1572	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
193		eleq1 2240	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ ℤ ↔ (𝐾‘𝑥) ∈ ℤ))
194	193	anbi2d 464	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → ((𝜑 ∧ 𝑘 ∈ ℤ) ↔ (𝜑 ∧ (𝐾‘𝑥) ∈ ℤ)))
195		eleq1 2240	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → (𝑘 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
196		csbeq1a 3068	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐾‘𝑥) → 𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
197	195, 196	ifbieq1d 3558	. . . . . . . . . 10 ⊢ (𝑘 = (𝐾‘𝑥) → if(𝑘 ∈ 𝐴, 𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
198	197	eleq1d 2246	. . . . . . . . 9 ⊢ (𝑘 = (𝐾‘𝑥) → (if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ ↔ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
199	194, 198	imbi12d 234	. . . . . . . 8 ⊢ (𝑘 = (𝐾‘𝑥) → (((𝜑 ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) ↔ ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)))
200	192, 199, 102	vtoclg1f 2798	. . . . . . 7 ⊢ ((𝐾‘𝑥) ∈ 𝐴 → ((𝜑 ∧ (𝐾‘𝑥) ∈ ℤ) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ))
201	179, 186, 200	sylc 62	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
202		eleq1 2240	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → (𝑛 ∈ 𝐴 ↔ (𝐾‘𝑥) ∈ 𝐴))
203		csbeq1 3062	. . . . . . . 8 ⊢ (𝑛 = (𝐾‘𝑥) → ⦋𝑛 / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
204	202, 203	ifbieq1d 3558	. . . . . . 7 ⊢ (𝑛 = (𝐾‘𝑥) → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
205		nfcv 2319	. . . . . . . . 9 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
206		nfv 1528	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
207		nfcsb1v 3092	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
208	206, 207, 143	nfif 3564	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
209		eleq1 2240	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
210		csbeq1a 3068	. . . . . . . . . 10 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
211	209, 210	ifbieq1d 3558	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
212	205, 208, 211	cbvmpt 4100	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
213	1, 212	eqtri 2198	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
214	204, 213	fvmptg 5594	. . . . . 6 ⊢ (((𝐾‘𝑥) ∈ ℤ ∧ if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
215	184, 201, 214	syl2anc 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(𝐾‘𝑥)) = if((𝐾‘𝑥) ∈ 𝐴, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
216		elfznn 10056	. . . . . . . 8 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ∈ ℕ)
217	216	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ∈ ℕ)
218		elfzle2 10030	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(♯‘𝐴)) → 𝑥 ≤ (♯‘𝐴))
219	218	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ (♯‘𝐴))
220	15	breq2d 4017	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
221	220	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑥 ≤ (♯‘𝐴) ↔ 𝑥 ≤ 𝑁))
222	219, 221	mpbid 147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → 𝑥 ≤ 𝑁)
223	222	iftrued 3543	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
224	180, 201	eqeltrrd 2255	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ⦋(𝐾‘𝑥) / 𝑘⦌𝐵 ∈ ℂ)
225	223, 224	eqeltrd 2254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ)
226		breq1 4008	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑁 ↔ 𝑥 ≤ 𝑁))
227		fveq2 5517	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝐾‘𝑛) = (𝐾‘𝑥))
228	227	csbeq1d 3066	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → ⦋(𝐾‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
229	226, 228	ifbieq1d 3558	. . . . . . . 8 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑁, ⦋(𝐾‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
230	229, 163	fvmptg 5594	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0) ∈ ℂ) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
231	217, 225, 230	syl2anc 411	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = if(𝑥 ≤ 𝑁, ⦋(𝐾‘𝑥) / 𝑘⦌𝐵, 0))
232	231, 223	eqtrd 2210	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = ⦋(𝐾‘𝑥) / 𝑘⦌𝐵)
233	180, 215, 232	3eqtr4rd 2221	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑥) = (𝐹‘(𝐾‘𝑥)))
234	72, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233	seq3coll 10824	. . 3 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐻)‘𝑁))
235	15, 7	eqeltrd 2254	. . . . 5 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
236	235, 7	jca 306	. . . 4 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ∧ 𝑁 ∈ ℕ))
237	16	eqcomd 2183	. . . . . 6 ⊢ (𝜑 → (1...𝑁) = (1...(♯‘𝐴)))
238		f1oeq2 5452	. . . . . 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 147	. . . 4 ⊢ (𝜑 → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
241		isummolem2a.g	. . . 4 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
242	1, 2, 236, 240, 21, 241, 163	summodclem3 11390	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐻)‘𝑁))
243	15	fveq2d 5521	. . 3 ⊢ (𝜑 → (seq1( + , 𝐺)‘(♯‘𝐴)) = (seq1( + , 𝐺)‘𝑁))
244	234, 242, 243	3eqtr2d 2216	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐾‘𝑁)) = (seq1( + , 𝐺)‘𝑁))
245	70, 244	breqtrd 4031	1 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 DECID wdc 834 ∧ w3a 978 = wceq 1353 ∈ wcel 2148 ∀wral 2455 ⦋csb 3059 ∖ cdif 3128 ⊆ wss 3131 ifcif 3536 class class class wbr 4005 ↦ cmpt 4066 ^◡ccnv 4627 ⟶wf 5214 –1-1-onto→wf1o 5217 ‘cfv 5218 Isom wiso 5219 (class class class)co 5877 ℂcc 7811 ℝcr 7812 0cc0 7813 1c1 7814 + caddc 7816 ℝ^*cxr 7993 < clt 7994 ≤ cle 7995 ℕcn 8921 ℕ₀cn0 9178 ℤcz 9255 ℤ_≥cuz 9530 ...cfz 10010 seqcseq 10447 ♯chash 10757 ⇝ cli 11288

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7904 ax-resscn 7905 ax-1cn 7906 ax-1re 7907 ax-icn 7908 ax-addcl 7909 ax-addrcl 7910 ax-mulcl 7911 ax-mulrcl 7912 ax-addcom 7913 ax-mulcom 7914 ax-addass 7915 ax-mulass 7916 ax-distr 7917 ax-i2m1 7918 ax-0lt1 7919 ax-1rid 7920 ax-0id 7921 ax-rnegex 7922 ax-precex 7923 ax-cnre 7924 ax-pre-ltirr 7925 ax-pre-ltwlin 7926 ax-pre-lttrn 7927 ax-pre-apti 7928 ax-pre-ltadd 7929 ax-pre-mulgt0 7930 ax-pre-mulext 7931

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-isom 5227 df-riota 5833 df-ov 5880 df-oprab 5881 df-mpo 5882 df-1st 6143 df-2nd 6144 df-recs 6308 df-frec 6394 df-1o 6419 df-er 6537 df-en 6743 df-dom 6744 df-fin 6745 df-pnf 7996 df-mnf 7997 df-xr 7998 df-ltxr 7999 df-le 8000 df-sub 8132 df-neg 8133 df-reap 8534 df-ap 8541 df-div 8632 df-inn 8922 df-2 8980 df-n0 9179 df-z 9256 df-uz 9531 df-rp 9656 df-fz 10011 df-fzo 10145 df-seqfrec 10448 df-exp 10522 df-ihash 10758 df-cj 10853 df-rsqrt 11009 df-abs 11010 df-clim 11289

This theorem is referenced by: summodclem2 11392 zsumdc 11394

W3C validator