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 16016

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 1167	. . . . . . . 8 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
2		nfcv 2927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
3		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
4		nfcsb1v 3878	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
5		nfcv 2927	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
6	3, 4, 5	nfif 4520	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
7		eleq1w 2848	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
8		csbeq1a 3868	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
9	7, 8	ifbieq1d 4514	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
10	2, 6, 9	cbvmpt 5215	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
11		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝜑)
12		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13	12	ralrimiva 3159	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
14	4	nfel1 2943	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
15	8	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
16	14, 15	rspc 3571	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
17	13, 16	syl5 35	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (𝜑 → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	11, 17	mpan9 516	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
19		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
20		zprod.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
21	20	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
22		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
23		zprod.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
24		zprod.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
25	23, 24	sseqtrdi 3978	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
26	25	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
27	10, 18, 19, 21, 22, 26	prodrb 16011	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
28	27	biimpd 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
29	28	expimpd 459	. . . . . . . 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 3168	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
32		uzssz 12901	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
33		zssre 12615	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ⊆ ℝ
34	32, 33	sstri 3947	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑀) ⊆ ℝ
35	24, 34	eqsstri 3984	. . . . . . . . . . . . . . 15 ⊢ 𝑍 ⊆ ℝ
36	23, 35	sstrdi 3950	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
37	36	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℝ)
38		ltso 11307	. . . . . . . . . . . . 13 ⊢ < Or ℝ
39		soss 5591	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ ℝ → ( < Or ℝ → < Or 𝐴))
40	37, 38, 39	mpisyl 22	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → < Or 𝐴)
41		fzfi 14028	. . . . . . . . . . . . 13 ⊢ (1...𝑚) ∈ Fin
42		ovex 7452	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑚) ∈ V
43	42	f1oen 8975	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 → (1...𝑚) ≈ 𝐴)
44	43	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
45	44	ensymd 9008	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
46		enfii 9177	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
47	41, 45, 46	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
48		fz1iso 14519	. . . . . . . . . . . 12 ⊢ (( < Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
49	40, 47, 48	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
50		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
51	50, 17	mpan9 516	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
52		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
53	52	csbeq1d 3858	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
54		csbcow 3869	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
55	53, 54	eqtr4di 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
56	55	cbvmptv 5217	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
57		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
58		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
59	20	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
60	25	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
61		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
62		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
63	10, 51, 56, 57, 58, 59, 60, 61, 62	prodmolem2a 16013	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
64	63	expr 462	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
65	64	exlimdv 1966	. . . . . . . . . . 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 5115	. . . . . . . . . 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 459	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
70	69	exlimdv 1966	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
71	70	rexlimdva 3168	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
72	31, 71	jaod 873	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
73	20	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
74	23	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ 𝑍)
75		zprod.3	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
76	24	eleq2i 2857	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ_≥‘𝑀))
77		eluzelz 12890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
78	77	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑛 ∈ ℤ)
79		uztrn 12898	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (ℤ_≥‘𝑛) ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑧 ∈ (ℤ_≥‘𝑀))
80	79	ancoms 464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → 𝑧 ∈ (ℤ_≥‘𝑀))
81	24	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ_≥‘𝑀))
82		zprod.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
83	24, 32	eqsstri 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑍 ⊆ ℤ
84	83	sseli 3934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ)
85		iftrue 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
86	85	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) = 𝐵)
87	86, 12	eqeltrd 2865	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
88	87	ex 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ))
89		iffalse 4498	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) = 1)
90		ax-1cn 11175	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
91	89, 90	eqeltrdi 2873	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
92	88, 91	pm2.61d1 182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ)
93		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
94	93	fvmpt2 7005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℤ ∧ if(𝑘 ∈ 𝐴, 𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
95	84, 92, 94	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
96	82, 95	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
97	81, 96	sylan2br 607	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
98	97	ralrimiva 3159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘))
99		nffvmpt1 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
100	99	nfeq2 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)
101		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → (𝐹‘𝑘) = (𝐹‘𝑧))
102		fveq2 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑧 → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
103	101, 102	eqeq12d 2781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑧 → ((𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) ↔ (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
104	100, 103	rspc 3571	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)(𝐹‘𝑘) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧)))
105	98, 104	mpan9 516	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
106	80, 105	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ_≥‘𝑀) ∧ 𝑧 ∈ (ℤ_≥‘𝑛))) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
107	106	anassrs 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑧 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑧) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧))
108	78, 107	seqfeq 14083	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
109	108	breq1d 5121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
110	109	anbi2d 642	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
111	110	exbidv 1954	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
112	76, 111	sylan2b 606	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
113	112	rexbidva 3189	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
114	75, 113	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
115	114	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
116		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
117		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
118	117, 24	eqtr4di 2818	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = 𝑍)
119	118	sseq2d 3970	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ 𝑍))
120	118	rexeqdv 3326	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
121		seqeq1 14060	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
122	121	breq1d 5121	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
123	119, 120, 122	3anbi123d 1464	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
124	123	rspcev 3583	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 ⊆ 𝑍 ∧ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
125	73, 74, 115, 116, 124	syl13anc 1399	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
126	125	orcd 887	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
127	126	ex 418	. . . . 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 2803	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
130	81, 129	sylan2br 607	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
131	130	ralrimiva 3159	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘))
132	99	nfeq1 2942	. . . . . . . 8 ⊢ Ⅎ𝑘((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)
133	102, 101	eqeq12d 2781	. . . . . . . 8 ⊢ (𝑘 = 𝑧 → (((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) ↔ ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
134	132, 133	rspc 3571	. . . . . . 7 ⊢ (𝑧 ∈ (ℤ_≥‘𝑀) → (∀𝑘 ∈ (ℤ_≥‘𝑀)((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑘) = (𝐹‘𝑘) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧)))
135	131, 134	mpan9 516	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑧) = (𝐹‘𝑧))
136	20, 135	seqfeq 14083	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
137	136	breq1d 5121	. . . 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 6524	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
140		df-prod 15983	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
141		df-fv 6548	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
142	139, 140, 141	3eqtr4g 2825	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 ⦋csb 3854 ⊆ wss 3906 ifcif 4489 class class class wbr 5111 ↦ cmpt 5194 Or wor 5570 ℩cio 6494 –1-1-onto→wf1o 6539 ‘cfv 6540 Isom wiso 6541 (class class class)co 7419 ≈ cen 8946 Fincfn 8949 ℂcc 11115 ℝcr 11116 0cc0 11117 1c1 11118 · cmul 11122 < clt 11260 ℕcn 12250 ℤcz 12608 ℤ_≥cuz 12880 ...cfz 13553 seqcseq 14057 ♯chash 14386 ⇝ cli 15561 ∏cprod 15982

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-oi 9479 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-n0 12522 df-z 12609 df-uz 12881 df-rp 13035 df-fz 13554 df-fzo 13702 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-prod 15983

This theorem is used by: iprod 16017 zprodn0 16018 prodss 16026

W3C validator