fprodseq - Intuitionistic Logic Explorer

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

Theorem fprodseq 12167

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)

**Hypotheses**
Ref	Expression
fprod.1	⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
fprod.2	⊢ (𝜑 → 𝑀 ∈ ℕ)
fprod.3	⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
fprod.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
fprod.5	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)

**Assertion**
Ref	Expression
fprodseq	⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))

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

Proof of Theorem fprodseq Dummy variables 𝑓 𝑖 𝑗 𝑚 𝑥 𝑝 𝑞 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-proddc 12135	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
2		nnuz 9797	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9511	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		eqid 2230	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))
5		breq1 4092	. . . . . . . 8 ⊢ (𝑛 = 𝑝 → (𝑛 ≤ 𝑀 ↔ 𝑝 ≤ 𝑀))
6		fveq2 5642	. . . . . . . 8 ⊢ (𝑛 = 𝑝 → (𝐺‘𝑛) = (𝐺‘𝑝))
7	5, 6	ifbieq1d 3629	. . . . . . 7 ⊢ (𝑛 = 𝑝 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1) = if(𝑝 ≤ 𝑀, (𝐺‘𝑝), 1))
8		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → 𝑝 ∈ ℕ)
9		simpll 527	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ 𝑀) → 𝜑)
10	8	anim1i 340	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ 𝑀) → (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑀))
11		fprod.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 9606	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13		fznn 10329	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℤ → (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑀)))
14	12, 13	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑀)))
15	14	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ 𝑀) → (𝑝 ∈ (1...𝑀) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑀)))
16	10, 15	mpbird 167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ 𝑀) → 𝑝 ∈ (1...𝑀))
17	6	eleq1d 2299	. . . . . . . . . 10 ⊢ (𝑛 = 𝑝 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑝) ∈ ℂ))
18		fprod.1	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
19		fprod.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
20		fprod.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
21		fprod.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)
22	18, 11, 19, 20, 21	fsumgcl 11970	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
23	22	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
24		simpr 110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → 𝑝 ∈ (1...𝑀))
25	17, 23, 24	rspcdva 2914	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → (𝐺‘𝑝) ∈ ℂ)
26	9, 16, 25	syl2anc 411	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ 𝑀) → (𝐺‘𝑝) ∈ ℂ)
27		1cnd 8200	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑀) → 1 ∈ ℂ)
28	8	nnzd 9606	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → 𝑝 ∈ ℤ)
29	12	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → 𝑀 ∈ ℤ)
30		zdcle 9561	. . . . . . . . 9 ⊢ ((𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑝 ≤ 𝑀)
31	28, 29, 30	syl2anc 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → DECID 𝑝 ≤ 𝑀)
32	26, 27, 31	ifcldadc 3636	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → if(𝑝 ≤ 𝑀, (𝐺‘𝑝), 1) ∈ ℂ)
33	4, 7, 8, 32	fvmptd3 5743	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑝) = if(𝑝 ≤ 𝑀, (𝐺‘𝑝), 1))
34	33, 32	eqeltrd 2307	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑝) ∈ ℂ)
35	2, 3, 34	prodf 12122	. . . 4 ⊢ (𝜑 → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))):ℕ⟶ℂ)
36	35, 11	ffvelcdmd 5786	. . 3 ⊢ (𝜑 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) ∈ ℂ)
37		eleq1w 2291	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
38	37	dcbid 845	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (DECID 𝑖 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
39	38	cbvralv 2766	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
40	39	anbi2i 457	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴))
41	40	anbi1i 458	. . . . . . . . 9 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
42	41	rexbii 2538	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
43		nnnn0 9414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
44		hashfz1 11051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
45	43, 44	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℕ → (♯‘(1...𝑚)) = 𝑚)
46	45	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
47		1zzd 9511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
48		nnz 9503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
49	48	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
50	47, 49	fzfigd 10699	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
51		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
52	50, 51	fihasheqf1od 11057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
53	46, 52	eqtr3d 2265	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 = (♯‘𝐴))
54	53	breq2d 4101	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ (♯‘𝐴)))
55	54	ifbid 3628	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))
56	55	mpteq2dv 4181	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))
57	56	seqeq3d 10723	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))))
58	57	fveq1d 5644	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
59	58	eqeq2d 2242	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
60	59	pm5.32da 452	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
61	60	exbidv 1872	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
62	61	rexbiia 2546	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
63	62	bicomi 132	. . . . . . . 8 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
64	42, 63	orbi12i 771	. . . . . . 7 ⊢ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
65		f1of 5586	. . . . . . . . . . . . 13 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
66	19, 65	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
67	3, 12	fzfigd 10699	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
68		fex 5888	. . . . . . . . . . . 12 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
69	66, 67, 68	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ V)
70	11, 2	eleqtrdi 2323	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
71		fveq2 5642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑢 → (𝐹‘𝑛) = (𝐹‘𝑢))
72	71	csbeq1d 3133	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑢 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑢) / 𝑘⦌𝐵)
73		fveq2 5642	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑢 → (𝐺‘𝑛) = (𝐺‘𝑢))
74	72, 73	eqeq12d 2245	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑢 → (⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = (𝐺‘𝑛) ↔ ⦋(𝐹‘𝑢) / 𝑘⦌𝐵 = (𝐺‘𝑢)))
75	66	ffvelcdmda 5785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
76	18	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
77	75, 76	csbied 3173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
78	77, 21	eqtr4d 2266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = (𝐺‘𝑛))
79	78	ralrimiva 2604	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = (𝐺‘𝑛))
80	79	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = (𝐺‘𝑛))
81		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ (1...𝑀))
82	74, 80, 81	rspcdva 2914	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ⦋(𝐹‘𝑢) / 𝑘⦌𝐵 = (𝐺‘𝑢))
83		eqid 2230	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))
84		breq1 4092	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑢 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑢 ≤ (♯‘𝐴)))
85	84, 72	ifbieq1d 3629	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑢 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑢 ≤ (♯‘𝐴), ⦋(𝐹‘𝑢) / 𝑘⦌𝐵, 1))
86		elfznn 10294	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ∈ ℕ)
87	86	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ∈ ℕ)
88		elfzle2 10268	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (1...𝑀) → 𝑢 ≤ 𝑀)
89	88	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ≤ 𝑀)
90	11	nnnn0d 9460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
91		hashfz1 11051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
93	67, 19	fihasheqf1od 11057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (♯‘(1...𝑀)) = (♯‘𝐴))
94	92, 93	eqtr3d 2265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 = (♯‘𝐴))
95	94	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑀 = (♯‘𝐴))
96	89, 95	breqtrd 4115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → 𝑢 ≤ (♯‘𝐴))
97	96	iftrued 3613	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → if(𝑢 ≤ (♯‘𝐴), ⦋(𝐹‘𝑢) / 𝑘⦌𝐵, 1) = ⦋(𝐹‘𝑢) / 𝑘⦌𝐵)
98	97, 82	eqtrd 2263	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → if(𝑢 ≤ (♯‘𝐴), ⦋(𝐹‘𝑢) / 𝑘⦌𝐵, 1) = (𝐺‘𝑢))
99	73	eleq1d 2299	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑢 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑢) ∈ ℂ))
100	22	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
101	99, 100, 81	rspcdva 2914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → (𝐺‘𝑢) ∈ ℂ)
102	98, 101	eqeltrd 2307	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → if(𝑢 ≤ (♯‘𝐴), ⦋(𝐹‘𝑢) / 𝑘⦌𝐵, 1) ∈ ℂ)
103	83, 85, 87, 102	fvmptd3 5743	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑢) = if(𝑢 ≤ (♯‘𝐴), ⦋(𝐹‘𝑢) / 𝑘⦌𝐵, 1))
104	103, 97	eqtrd 2263	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑢) = ⦋(𝐹‘𝑢) / 𝑘⦌𝐵)
105		breq1 4092	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑢 → (𝑛 ≤ 𝑀 ↔ 𝑢 ≤ 𝑀))
106	105, 73	ifbieq1d 3629	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑢 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1) = if(𝑢 ≤ 𝑀, (𝐺‘𝑢), 1))
107	89	iftrued 3613	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → if(𝑢 ≤ 𝑀, (𝐺‘𝑢), 1) = (𝐺‘𝑢))
108	107, 101	eqeltrd 2307	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → if(𝑢 ≤ 𝑀, (𝐺‘𝑢), 1) ∈ ℂ)
109	4, 106, 87, 108	fvmptd3 5743	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑢) = if(𝑢 ≤ 𝑀, (𝐺‘𝑢), 1))
110	109, 107	eqtrd 2263	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑢) = (𝐺‘𝑢))
111	82, 104, 110	3eqtr4rd 2274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑢) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑢))
112		elnnuz 9798	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℕ ↔ 𝑝 ∈ (ℤ_≥‘1))
113	112, 34	sylan2br 288	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1))‘𝑝) ∈ ℂ)
114		breq1 4092	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑝 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑝 ≤ (♯‘𝐴)))
115		fveq2 5642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑝 → (𝐹‘𝑛) = (𝐹‘𝑝))
116	115	csbeq1d 3133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑝 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑝) / 𝑘⦌𝐵)
117	114, 116	ifbieq1d 3629	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑝 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑝 ≤ (♯‘𝐴), ⦋(𝐹‘𝑝) / 𝑘⦌𝐵, 1))
118		simpll 527	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝜑)
119		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ≤ (♯‘𝐴))
120	94	breq2d 4101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑝 ≤ 𝑀 ↔ 𝑝 ≤ (♯‘𝐴)))
121	120	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → (𝑝 ≤ 𝑀 ↔ 𝑝 ≤ (♯‘𝐴)))
122	119, 121	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ≤ 𝑀)
123	122, 16	syldan 282	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → 𝑝 ∈ (1...𝑀))
124	66	ffvelcdmda 5785	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → (𝐹‘𝑝) ∈ 𝐴)
125	20	ralrimiva 2604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
126	125	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
127		nfcsb1v 3159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘⦋(𝐹‘𝑝) / 𝑘⦌𝐵
128	127	nfel1 2384	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘⦋(𝐹‘𝑝) / 𝑘⦌𝐵 ∈ ℂ
129		csbeq1a 3135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (𝐹‘𝑝) → 𝐵 = ⦋(𝐹‘𝑝) / 𝑘⦌𝐵)
130	129	eleq1d 2299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (𝐹‘𝑝) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑝) / 𝑘⦌𝐵 ∈ ℂ))
131	128, 130	rspc 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑝) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑝) / 𝑘⦌𝐵 ∈ ℂ))
132	124, 126, 131	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (1...𝑀)) → ⦋(𝐹‘𝑝) / 𝑘⦌𝐵 ∈ ℂ)
133	118, 123, 132	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ 𝑝 ≤ (♯‘𝐴)) → ⦋(𝐹‘𝑝) / 𝑘⦌𝐵 ∈ ℂ)
134		1cnd 8200	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑝 ∈ ℕ) ∧ ¬ 𝑝 ≤ (♯‘𝐴)) → 1 ∈ ℂ)
135	94, 12	eqeltrrd 2308	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
136	135	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → (♯‘𝐴) ∈ ℤ)
137		zdcle 9561	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑝 ≤ (♯‘𝐴))
138	28, 136, 137	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → DECID 𝑝 ≤ (♯‘𝐴))
139	133, 134, 138	ifcldadc 3636	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → if(𝑝 ≤ (♯‘𝐴), ⦋(𝐹‘𝑝) / 𝑘⦌𝐵, 1) ∈ ℂ)
140	83, 117, 8, 139	fvmptd3 5743	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑝) = if(𝑝 ≤ (♯‘𝐴), ⦋(𝐹‘𝑝) / 𝑘⦌𝐵, 1))
141	140, 139	eqeltrd 2307	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑝) ∈ ℂ)
142	112, 141	sylan2br 288	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))‘𝑝) ∈ ℂ)
143		mulcl 8164	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
144	143	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
145	70, 111, 113, 142, 144	seq3fveq 10747	. . . . . . . . . . . 12 ⊢ (𝜑 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))
146	19, 145	jca 306	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀)))
147		f1oeq1 5574	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
148		fveq1 5641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
149	148	csbeq1d 3133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
150	149	ifeq1d 3624	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))
151	150	mpteq2dv 4181	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))
152	151	seqeq3d 10723	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1))))
153	152	fveq1d 5644	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))
154	153	eqeq2d 2242	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀)))
155	147, 154	anbi12d 473	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝐹‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))))
156	69, 146, 155	spcedv 2894	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀)))
157		oveq2 6031	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
158	157	f1oeq2d 5582	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
159		fveq2 5642	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))
160	159	eqeq2d 2242	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀)))
161	158, 160	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))))
162	161	exbidv 1872	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))))
163	162	rspcev 2909	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
164	11, 156, 163	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
165	164	olcd 741	. . . . . . . 8 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
166		nfcv 2373	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗if(𝑘 ∈ 𝐴, 𝐵, 1)
167		nfv 1576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 𝑗 ∈ 𝐴
168		nfcsb1v 3159	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
169		nfcv 2373	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘1
170	167, 168, 169	nfif 3635	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1)
171		eleq1w 2291	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
172		csbeq1a 3135	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
173	171, 172	ifbieq1d 3629	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1))
174	166, 170, 173	cbvmpt 4185	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1))
175	168	nfel1 2384	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
176	172	eleq1d 2299	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
177	175, 176	rspc 2903	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
178	125, 177	mpan9 281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
179		breq1 4092	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
180		fveq2 5642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
181	180	csbeq1d 3133	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
182		csbcow 3137	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
183	181, 182	eqtr4di 2281	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
184	179, 183	ifbieq1d 3629	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 1))
185	184	cbvmptv 4186	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 1))
186	174, 178, 185	prodmodc 12162	. . . . . . . . . . . 12 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
187	36, 186	jca 306	. . . . . . . . . . 11 ⊢ (𝜑 → ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) ∈ ℂ ∧ ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
188		breq2 4093	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
189	188	anbi2d 464	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → ((∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))))
190	189	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))))
191	190	rexbidv 2532	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))))
192		eqeq1 2237	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
193	192	anbi2d 464	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
194	193	exbidv 1872	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
195	194	rexbidv 2532	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
196	191, 195	orbi12d 800	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
197	196	moi2 2986	. . . . . . . . . . 11 ⊢ ((((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) ∈ ℂ ∧ ∃*𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) ∧ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
198	187, 197	sylan 283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
199	198	ancom2s 568	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
200	199	expr 375	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
201	165, 200	mpdan 421	. . . . . . 7 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
202	64, 201	biimtrrid 153	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) → 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
203	64, 196	bitr3id 194	. . . . . . 7 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑖 ∈ (ℤ_≥‘𝑚)DECID 𝑖 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
204	165, 203	syl5ibrcom 157	. . . . . 6 ⊢ (𝜑 → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
205	202, 204	impbid 129	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
206	205	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) ∈ ℂ) → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀)))
207	206	iota5 5310	. . 3 ⊢ ((𝜑 ∧ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀) ∈ ℂ) → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
208	36, 207	mpdan 421	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))
209	1, 208	eqtrid 2275	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 1)))‘𝑀))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 715 DECID wdc 841 = wceq 1397 ∃wex 1540 ∃*wmo 2079 ∈ wcel 2201 ∀wral 2509 ∃wrex 2510 Vcvv 2801 ⦋csb 3126 ⊆ wss 3199 ifcif 3604 class class class wbr 4089 ↦ cmpt 4151 ℩cio 5286 ⟶wf 5324 –1-1-onto→wf1o 5327 ‘cfv 5328 (class class class)co 6023 Fincfn 6914 ℂcc 8035 0cc0 8037 1c1 8038 · cmul 8042 ≤ cle 8220 # cap 8766 ℕcn 9148 ℕ₀cn0 9407 ℤcz 9484 ℤ_≥cuz 9760 ...cfz 10248 seqcseq 10715 ♯chash 11043 ⇝ cli 11861 ∏cprod 12134

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2203 ax-14 2204 ax-ext 2212 ax-coll 4205 ax-sep 4208 ax-nul 4216 ax-pow 4266 ax-pr 4301 ax-un 4532 ax-setind 4637 ax-iinf 4688 ax-cnex 8128 ax-resscn 8129 ax-1cn 8130 ax-1re 8131 ax-icn 8132 ax-addcl 8133 ax-addrcl 8134 ax-mulcl 8135 ax-mulrcl 8136 ax-addcom 8137 ax-mulcom 8138 ax-addass 8139 ax-mulass 8140 ax-distr 8141 ax-i2m1 8142 ax-0lt1 8143 ax-1rid 8144 ax-0id 8145 ax-rnegex 8146 ax-precex 8147 ax-cnre 8148 ax-pre-ltirr 8149 ax-pre-ltwlin 8150 ax-pre-lttrn 8151 ax-pre-apti 8152 ax-pre-ltadd 8153 ax-pre-mulgt0 8154 ax-pre-mulext 8155 ax-arch 8156 ax-caucvg 8157

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-nel 2497 df-ral 2514 df-rex 2515 df-reu 2516 df-rmo 2517 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-if 3605 df-pw 3655 df-sn 3676 df-pr 3677 df-op 3679 df-uni 3895 df-int 3930 df-iun 3973 df-br 4090 df-opab 4152 df-mpt 4153 df-tr 4189 df-id 4392 df-po 4395 df-iso 4396 df-iord 4465 df-on 4467 df-ilim 4468 df-suc 4470 df-iom 4691 df-xp 4733 df-rel 4734 df-cnv 4735 df-co 4736 df-dm 4737 df-rn 4738 df-res 4739 df-ima 4740 df-iota 5288 df-fun 5330 df-fn 5331 df-f 5332 df-f1 5333 df-fo 5334 df-f1o 5335 df-fv 5336 df-isom 5337 df-riota 5976 df-ov 6026 df-oprab 6027 df-mpo 6028 df-1st 6308 df-2nd 6309 df-recs 6476 df-irdg 6541 df-frec 6562 df-1o 6587 df-oadd 6591 df-er 6707 df-en 6915 df-dom 6916 df-fin 6917 df-pnf 8221 df-mnf 8222 df-xr 8223 df-ltxr 8224 df-le 8225 df-sub 8357 df-neg 8358 df-reap 8760 df-ap 8767 df-div 8858 df-inn 9149 df-2 9207 df-3 9208 df-4 9209 df-n0 9408 df-z 9485 df-uz 9761 df-q 9859 df-rp 9894 df-fz 10249 df-fzo 10383 df-seqfrec 10716 df-exp 10807 df-ihash 11044 df-cj 11425 df-re 11426 df-im 11427 df-rsqrt 11581 df-abs 11582 df-clim 11862 df-proddc 12135

This theorem is referenced by: prod1dc 12170 fprodf1o 12172 fprodmul 12175 prodsnf 12176

W3C validator