zprod - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > zprod		Structured version Visualization version GIF version

Theorem zprod 15998

Description: Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)

**Hypotheses**
Ref	Expression
zprod.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
zprod.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
zprod.3	⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
zprod.4	⊢ (𝜑 → 𝐴 ⊆ 𝑍)
zprod.5	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
zprod.6	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)

**Assertion**
Ref	Expression
zprod	⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Distinct variable groups: 𝐴,𝑘,𝑛 𝜑,𝑘,𝑛 𝑛,𝑍 𝐵,𝑛,𝑦 𝑘,𝐹 𝜑,𝑦 𝑦,𝐴 𝑘,𝑀,𝑦 Allowed substitution hints: 𝐵(𝑘) 𝐹(𝑦, 𝑛) 𝑀(𝑛) 𝑍(𝑦, 𝑘)

Proof of Theorem zprod Dummy variables 𝑓 𝑔 𝑖 𝑗 𝑚 𝑧 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		3simpb 1166	. . . . . . . 8 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
2		nfcv 2924	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
3		nfv 1943	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
4		nfcsb1v 3876	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
5		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
6	3, 4, 5	nfif 4517	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
7		eleq1w 2845	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
8		csbeq1a 3866	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
9	7, 8	ifbieq1d 4511	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
10	2, 6, 9	cbvmpt 5212	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
11		simpll 778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝜑)
12		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13	12	ralrimiva 3156	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
14	4	nfel1 2940	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
15	8	eleq1d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
16	14, 15	rspc 3568	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
17	13, 16	syl5 35	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (𝜑 → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	11, 17	mpan9 515	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
19		simplr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
20		zprod.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
21	20	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
22		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
23		zprod.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
24		zprod.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
25	23, 24	sseqtrdi 3976	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
26	25	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
27	10, 18, 19, 21, 22, 26	prodrb 15993	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
28	27	biimpd 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
29	28	expimpd 458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
30	1, 29	syl5 35	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
31	30	rexlimdva 3165	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
32		uzssz 12889	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
33		zssre 12604	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℝ
34	32, 33	sstri 3945	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
35	24, 34	eqsstri 3982	. . . . . . . . . . . . . . 15 ⊢ 𝑍 ⊆ ℝ
36	23, 35	sstrdi 3948	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
37	36	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℝ)
38		ltso 11296	. . . . . . . . . . . . 13 ⊢ < Or ℝ
39		soss 5588	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴))
40	37, 38, 39	mpisyl 22	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → < Or 𝐴)
41		fzfi 14015	. . . . . . . . . . . . 13 ⊢ (1...𝑚) ∈ Fin
42		ovex 7445	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ∈ V
43	42	f1oen 8967	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 → (1...𝑚) ≈ 𝐴)
44	43	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
45	44	ensymd 9000	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
46		enfii 9168	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
47	41, 45, 46	sylancr 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
48		fz1iso 14506	. . . . . . . . . . . 12 ⊢ (( < Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
49	40, 47, 48	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
50		simpll 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
51	50, 17	mpan9 515	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
52		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
53	52	csbeq1d 3856	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
54		csbcow 3867	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
55	53, 54	eqtr4di 2815	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
56	55	cbvmptv 5214	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
57		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
58		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
59	20	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
60	25	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
61		simprl 782	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
62		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
63	10, 51, 56, 57, 58, 59, 60, 61, 62	prodmolem2a 15995	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
64	63	expr 461	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
65	64	exlimdv 1962	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
66	49, 65	mpd 16	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
67		breq2 5112	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
68	66, 67	syl5ibrcom 250	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
69	68	expimpd 458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
70	69	exlimdv 1962	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
71	70	rexlimdva 3165	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
72	31, 71	jaod 872	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
73	20	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
74	23	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ 𝑍)
75		zprod.3	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
76	24	eleq2i 2854	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ_≥‘𝑀))
77		eluzelz 12878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
78	77	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑛 ∈ ℤ)
79		uztrn 12886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (ℤ_≥‘𝑛) ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑧 ∈ (ℤ_≥‘𝑀))
80	79	ancoms 463	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → 𝑧 ∈ (ℤ_≥‘𝑀))
81	24	eleq2i 2854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ_≥‘𝑀))
82		zprod.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
83	24, 32	eqsstri 3982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑍 ⊆ ℤ
84	83	sseli 3932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ)
85		iftrue 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
86	85	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
87	86, 12	eqeltrd 2862	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
88	87	ex 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ))
89		iffalse 4495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1)
90		ax-1cn 11164	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
91	89, 90	eqeltrdi 2870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
92	88, 91	pm2.61d1 182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
93		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
94	93	fvmpt2 7001	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
95	84, 92, 94	syl2anr 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
96	82, 95	eqtr4d 2800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
97	81, 96	sylan2br 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
98	97	ralrimiva 3156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
99		nffvmpt1 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
100	99	nfeq2 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
101		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → (𝐹‘𝑘) = (𝐹‘𝑧))
102		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
103	101, 102	eqeq12d 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑧 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) ↔ (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
104	100, 103	rspc 3568	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
105	98, 104	mpan9 515	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
106	80, 105	sylan2 604	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
107	106	anassrs 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
108	78, 107	seqfeq 14070	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
109	108	breq1d 5118	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
110	109	anbi2d 641	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
111	110	exbidv 1950	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
112	76, 111	sylan2b 605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
113	112	rexbidva 3186	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
114	75, 113	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
115	114	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
116		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
117		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
118	117, 24	eqtr4di 2815	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = 𝑍)
119	118	sseq2d 3968	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ 𝑍))
120	118	rexeqdv 3323	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
121		seqeq1 14047	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
122	121	breq1d 5118	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
123	119, 120, 122	3anbi123d 1463	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
124	123	rspcev 3580	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
125	73, 74, 115, 116, 124	syl13anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
126	125	orcd 886	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
127	126	ex 417	. . . . 5 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
128	72, 127	impbid 215	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
129	95, 82	eqtr4d 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
130	81, 129	sylan2br 606	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
131	130	ralrimiva 3156	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
132	99	nfeq1 2939	. . . . . . . 8 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)
133	102, 101	eqeq12d 2778	. . . . . . . 8 ⊢ (𝑘 = 𝑧 → (((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) ↔ ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
134	132, 133	rspc 3568	. . . . . . 7 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
135	131, 134	mpan9 515	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧))
136	20, 135	seqfeq 14070	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
137	136	breq1d 5118	. . . 4 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
138	128, 137	bitrd 282	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
139	138	iotabidv 6520	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
140		df-prod 15965	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
141		df-fv 6544	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
142	139, 140, 141	3eqtr4g 2822	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1102 = wceq 1569 ∃wex 1808 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ⦋csb 3852 ⊆ wss 3904 ifcif 4486 class class class wbr 5108 ↦ cmpt 5191 Or wor 5567 ℩cio 6490 –1-1-onto→wf1o 6535 ‘cfv 6536 Isom wiso 6537 (class class class)co 7412 ≈ cen 8938 Fincfn 8941 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 · cmul 11111 < clt 11249 ℕcn 12239 ℤcz 12597 ℤ_≥cuz 12868 ...cfz 13541 seqcseq 14044 ♯chash 14373 ⇝ cli 15542 ∏cprod 15964

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-n0 12511 df-z 12598 df-uz 12869 df-rp 13023 df-fz 13542 df-fzo 13690 df-seq 14045 df-exp 14105 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-clim 15546 df-prod 15965

This theorem is used by: iprod 15999 zprodn0 16000 prodss 16008

W3C validator