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 15888

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 1148	. . . . . . . 8 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
2		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
3		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
4		nfcsb1v 3918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
5		nfcv 2902	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
6	3, 4, 5	nfif 4558	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
7		eleq1w 2815	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
8		csbeq1a 3907	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
9	7, 8	ifbieq1d 4552	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
10	2, 6, 9	cbvmpt 5259	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
11		simpll 764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝜑)
12		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13	12	ralrimiva 3145	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
14	4	nfel1 2918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
15	8	eleq1d 2817	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
16	14, 15	rspc 3600	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
17	13, 16	syl5 34	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (𝜑 → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	11, 17	mpan9 506	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
19		simplr 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
20		zprod.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
21	20	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
22		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
23		zprod.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
24		zprod.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
25	23, 24	sseqtrdi 4032	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
26	25	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
27	10, 18, 19, 21, 22, 26	prodrb 15883	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
28	27	biimpd 228	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
29	28	expimpd 453	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
30	1, 29	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
31	30	rexlimdva 3154	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
32		uzssz 12850	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
33		zssre 12572	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℝ
34	32, 33	sstri 3991	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
35	24, 34	eqsstri 4016	. . . . . . . . . . . . . . 15 ⊢ 𝑍 ⊆ ℝ
36	23, 35	sstrdi 3994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
37	36	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℝ)
38		ltso 11301	. . . . . . . . . . . . 13 ⊢ < Or ℝ
39		soss 5608	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴))
40	37, 38, 39	mpisyl 21	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → < Or 𝐴)
41		fzfi 13944	. . . . . . . . . . . . 13 ⊢ (1...𝑚) ∈ Fin
42		ovex 7445	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ∈ V
43	42	f1oen 8975	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 → (1...𝑚) ≈ 𝐴)
44	43	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
45	44	ensymd 9007	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
46		enfii 9195	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
47	41, 45, 46	sylancr 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
48		fz1iso 14430	. . . . . . . . . . . 12 ⊢ (( < Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
49	40, 47, 48	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
50		simpll 764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
51	50, 17	mpan9 506	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
52		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
53	52	csbeq1d 3897	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
54		csbcow 3908	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
55	53, 54	eqtr4di 2789	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
56	55	cbvmptv 5261	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
57		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
58		simplr 766	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
59	20	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
60	25	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
61		simprl 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
62		simprr 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
63	10, 51, 56, 57, 58, 59, 60, 61, 62	prodmolem2a 15885	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
64	63	expr 456	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
65	64	exlimdv 1935	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
66	49, 65	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
67		breq2 5152	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
68	66, 67	syl5ibrcom 246	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
69	68	expimpd 453	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
70	69	exlimdv 1935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
71	70	rexlimdva 3154	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
72	31, 71	jaod 856	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
73	20	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
74	23	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ 𝑍)
75		zprod.3	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
76	24	eleq2i 2824	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ_≥‘𝑀))
77		eluzelz 12839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
78	77	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑛 ∈ ℤ)
79		uztrn 12847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (ℤ_≥‘𝑛) ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑧 ∈ (ℤ_≥‘𝑀))
80	79	ancoms 458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → 𝑧 ∈ (ℤ_≥‘𝑀))
81	24	eleq2i 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ_≥‘𝑀))
82		zprod.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
83	24, 32	eqsstri 4016	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑍 ⊆ ℤ
84	83	sseli 3978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ)
85		iftrue 4534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
86	85	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
87	86, 12	eqeltrd 2832	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
88	87	ex 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ))
89		iffalse 4537	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1)
90		ax-1cn 11174	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
91	89, 90	eqeltrdi 2840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
92	88, 91	pm2.61d1 180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
93		eqid 2731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
94	93	fvmpt2 7009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
95	84, 92, 94	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
96	82, 95	eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
97	81, 96	sylan2br 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
98	97	ralrimiva 3145	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
99		nffvmpt1 6902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
100	99	nfeq2 2919	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
101		fveq2 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → (𝐹‘𝑘) = (𝐹‘𝑧))
102		fveq2 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
103	101, 102	eqeq12d 2747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑧 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) ↔ (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
104	100, 103	rspc 3600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
105	98, 104	mpan9 506	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
106	80, 105	sylan2 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
107	106	anassrs 467	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
108	78, 107	seqfeq 14000	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
109	108	breq1d 5158	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
110	109	anbi2d 628	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
111	110	exbidv 1923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
112	76, 111	sylan2b 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
113	112	rexbidva 3175	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
114	75, 113	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
115	114	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
116		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
117		fveq2 6891	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
118	117, 24	eqtr4di 2789	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = 𝑍)
119	118	sseq2d 4014	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ 𝑍))
120	118	rexeqdv 3325	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
121		seqeq1 13976	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
122	121	breq1d 5158	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
123	119, 120, 122	3anbi123d 1435	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
124	123	rspcev 3612	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
125	73, 74, 115, 116, 124	syl13anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
126	125	orcd 870	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
127	126	ex 412	. . . . 5 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
128	72, 127	impbid 211	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
129	95, 82	eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
130	81, 129	sylan2br 594	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
131	130	ralrimiva 3145	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
132	99	nfeq1 2917	. . . . . . . 8 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)
133	102, 101	eqeq12d 2747	. . . . . . . 8 ⊢ (𝑘 = 𝑧 → (((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) ↔ ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
134	132, 133	rspc 3600	. . . . . . 7 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
135	131, 134	mpan9 506	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧))
136	20, 135	seqfeq 14000	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
137	136	breq1d 5158	. . . 4 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
138	128, 137	bitrd 279	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
139	138	iotabidv 6527	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
140		df-prod 15857	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
141		df-fv 6551	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
142	139, 140, 141	3eqtr4g 2796	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1086 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 ⦋csb 3893 ⊆ wss 3948 ifcif 4528 class class class wbr 5148 ↦ cmpt 5231 Or wor 5587 ℩cio 6493 –1-1-onto→wf1o 6542 ‘cfv 6543 Isom wiso 6544 (class class class)co 7412 ≈ cen 8942 Fincfn 8945 ℂcc 11114 ℝcr 11115 0cc0 11116 1c1 11117 · cmul 11121 < clt 11255 ℕcn 12219 ℤcz 12565 ℤ_≥cuz 12829 ...cfz 13491 seqcseq 13973 ♯chash 14297 ⇝ cli 15435 ∏cprod 15856

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-er 8709 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-oi 9511 df-card 9940 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-n0 12480 df-z 12566 df-uz 12830 df-rp 12982 df-fz 13492 df-fzo 13635 df-seq 13974 df-exp 14035 df-hash 14298 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15439 df-prod 15857

This theorem is referenced by: iprod 15889 zprodn0 15890 prodss 15898

W3C validator