Theorem zproddc 11586

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	⊢ (𝜑 → 𝑀 ∈ ℤ)
zproddc.3	⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
zprod.4	⊢ (𝜑 → 𝐴 ⊆ 𝑍)
zproddc.dc	⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
zprod.5	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
zprod.6	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)

Assertion

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

Distinct variable groups:   𝐴,𝑗,𝑘,𝑛,𝑦   𝐵,𝑗,𝑛,𝑦   𝑘,𝐹   𝑗,𝑀,𝑘,𝑛,𝑦   𝑗,𝑍,𝑘,𝑛   𝜑,𝑗,𝑘,𝑛,𝑦

Allowed substitution hints:   𝐵(𝑘)   𝐹(𝑦,𝑗,𝑛)   𝑍(𝑦)

Proof of Theorem zproddc

Dummy variables 𝑓 𝑔 𝑖 𝑚 𝑝 𝑟 𝑞 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 527	. . . . . . . . 9 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ≥‘𝑚))
2		simprr 531	. . . . . . . . 9 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
3	1, 2	jca 306	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
4		nfcv 2319	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
5		nfv 1528	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
6		nfcsb1v 3090	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
7		nfcv 2319	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
8	5, 6, 7	nfif 3562	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
9		eleq1w 2238	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
10		csbeq1a 3066	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
11	9, 10	ifbieq1d 3556	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
12	4, 8, 11	cbvmpt 4098	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
13		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝜑)
14		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
15	14	ralrimiva 2550	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
16	6	nfel1 2330	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
17	10	eleq1d 2246	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	16, 17	rspc 2835	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
19	15, 18	syl5 32	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (𝜑 → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
20	13, 19	mpan9 281	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
21		simplr 528	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝑚 ∈ ℤ)
22		zprod.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23	22	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝑀 ∈ ℤ)
24		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝐴 ⊆ (ℤ≥‘𝑚))
25		zprod.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
26		zprod.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ≥‘𝑀)
27	25, 26	sseqtrdi 3203	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))
28	27	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝐴 ⊆ (ℤ≥‘𝑀))
29		zproddc.dc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
30	26	raleqi 2676	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
31	29, 30	sylib 122	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
32		eleq1w 2238	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
33	32	dcbid 838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑖 ∈ 𝐴))
34	33	cbvralv 2703	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑖 ∈ (ℤ≥‘𝑀)DECID 𝑖 ∈ 𝐴)
35	31, 34	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ (ℤ≥‘𝑀)DECID 𝑖 ∈ 𝐴)
36	35	r19.21bi 2565	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
37	36	adantlr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
38	37	adantlr 477	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
39	38	adantlr 477	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
40		simp-4l 541	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → 𝜑)
41		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → ¬ 𝑖 ∈ (ℤ≥‘𝑀))
42	27	ssneld 3157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ 𝑖 ∈ (ℤ≥‘𝑀) → ¬ 𝑖 ∈ 𝐴))
43	40, 41, 42	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → ¬ 𝑖 ∈ 𝐴)
44	43	olcd 734	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
45		df-dc 835	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ 𝐴 ↔ (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
46	44, 45	sylibr 134	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
47		eluzelz 9536	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑚) → 𝑖 ∈ ℤ)
48		eluzdc 9609	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ≥‘𝑀))
49	23, 47, 48	syl2an 289	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → DECID 𝑖 ∈ (ℤ≥‘𝑀))
50		exmiddc 836	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ (ℤ≥‘𝑀) → (𝑖 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ≥‘𝑀)))
51	49, 50	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → (𝑖 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ≥‘𝑀)))
52	39, 46, 51	mpjaodan 798	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → DECID 𝑖 ∈ 𝐴)
53	12, 20, 21, 23, 24, 28, 52, 38	prodrbdc 11581	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
54	53	biimpd 144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
55	54	expimpd 363	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
56	3, 55	syl5 32	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
57	56	rexlimdva 2594	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
58		uzssz 9546	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
59	27, 58	sstrdi 3167	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
60	59	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℤ)
61		1zzd 9279	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
62		nnz 9271	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
63	62	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
64	63	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
65	61, 64	fzfigd 10430	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
66		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
67		f1oeng 6756	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
68	65, 66, 67	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
69	68	ensymd 6782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
70		enfii 6873	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
71	65, 69, 70	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
72		zfz1iso 10820	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
73	60, 71, 72	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
74		simpll 527	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
75	74, 19	mpan9 281	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
76		breq1 4006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
77		fveq2 5515	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
78	77	csbeq1d 3064	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
79	76, 78	ifbieq1d 3556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
80		csbcow 3068	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
81		ifeq1 3537	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)
83	79, 82	eqtr4di 2228	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
84	83	cbvmptv 4099	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
85		eqid 2177	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
86	36	ad4ant14 514	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
87		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
88	22	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
89	27	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑀))
90		simprl 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
91		simprr 531	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
92	12, 75, 84, 85, 86, 87, 88, 89, 90, 91	prodmodclem2a 11583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
93	65	adantrr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
94	93, 90	fihasheqf1od 10768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
95	87	nnnn0d 9228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ0)
96		hashfz1 10762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
97	95, 96	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
98	94, 97	eqtr3d 2212	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
99	98	breq2d 4015	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
100	99	ifbid 3555	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))
101	100	mpteq2dv 4094	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))
102	101	seqeq3d 10452	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))))
103	102	fveq1d 5517	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
104	92, 103	breqtrd 4029	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
105	104	expr 375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
106	105	exlimdv 1819	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
107	73, 106	mpd 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
108		breq2 4007	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
109	107, 108	syl5ibrcom 157	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
110	109	expimpd 363	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
111	110	exlimdv 1819	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
112	111	rexlimdva 2594	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
113	57, 112	jaod 717	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
114	22	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
115	27	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ (ℤ≥‘𝑀))
116	31	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
117	115, 116	jca 306	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴))
118		zproddc.3	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
119	26	eleq2i 2244	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀))
120		eluzelz 9536	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
121	120	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ ℤ)
122		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ (ℤ≥‘𝑛))
123		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ (ℤ≥‘𝑀))
124		uztrn 9543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ (ℤ≥‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑝 ∈ (ℤ≥‘𝑀))
125	122, 123, 124	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ (ℤ≥‘𝑀))
126	125, 26	eleqtrrdi 2271	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ 𝑍)
127		zprod.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
128	127	ralrimiva 2550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
129	128	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
130		nfv 1528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑝 ∈ 𝐴
131		nfcsb1v 3090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵
132	130, 131, 7	nfif 3562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
133	132	nfeq2 2331	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
134		fveq2 5515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐹‘𝑘) = (𝐹‘𝑝))
135		eleq1w 2238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → (𝑘 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
136		csbeq1a 3066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → 𝐵 = ⦋𝑝 / 𝑘⦌𝐵)
137	135, 136	ifbieq1d 3556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
138	134, 137	eqeq12d 2192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑝 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)))
139	133, 138	rspc 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) → (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)))
140	126, 129, 139	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
141		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
142	15	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
143	131	nfel1 2330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ
144	136	eleq1d 2246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐵 ∈ ℂ ↔ ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
145	143, 144	rspc 2835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
146	141, 142, 145	sylc 62	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
147		1cnd 7972	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
148		eleq1w 2238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑝 → (𝑗 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
149	148	dcbid 838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑝 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑝 ∈ 𝐴))
150	29	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
151	149, 150, 126	rspcdva 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → DECID 𝑝 ∈ 𝐴)
152	146, 147, 151	ifcldadc 3563	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
153	140, 152	eqeltrd 2254	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑝) ∈ ℂ)
154		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ (ℤ≥‘𝑛))
155		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ (ℤ≥‘𝑀))
156		uztrn 9543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑟 ∈ (ℤ≥‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑟 ∈ (ℤ≥‘𝑀))
157	154, 155, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ (ℤ≥‘𝑀))
158	157, 26	eleqtrrdi 2271	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ 𝑍)
159	128	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
160		nfv 1528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑟 ∈ 𝐴
161		nfcsb1v 3090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵
162	160, 161, 7	nfif 3562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
163	162	nfeq2 2331	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
164		fveq2 5515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → (𝐹‘𝑘) = (𝐹‘𝑟))
165		eleq1w 2238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝑘 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
166		csbeq1a 3066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → 𝐵 = ⦋𝑟 / 𝑘⦌𝐵)
167	165, 166	ifbieq1d 3556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
168	164, 167	eqeq12d 2192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑟 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
169	163, 168	rspc 2835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
170	158, 159, 169	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
171	58, 157	sselid 3153	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℤ)
172		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
173	15	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
174	161	nfel1 2330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ
175	166	eleq1d 2246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝐵 ∈ ℂ ↔ ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
176	174, 175	rspc 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
177	172, 173, 176	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
178		1cnd 7972	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
179		eleq1w 2238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑟 → (𝑗 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
180	179	dcbid 838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑟 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑟 ∈ 𝐴))
181	29	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
182	180, 181, 158	rspcdva 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → DECID 𝑟 ∈ 𝐴)
183	177, 178, 182	ifcldadc 3563	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ)
184		nfcv 2319	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘𝑟
185		eqid 2177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
186	184, 162, 167, 185	fvmptf 5608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ ℤ ∧ if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
187	171, 183, 186	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
188	170, 187	eqtr4d 2213	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑟) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟))
189		mulcl 7937	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
190	189	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
191	121, 153, 188, 190	seq3feq 10471	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
192	191	breq1d 4013	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
193	192	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
194	193	exbidv 1825	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
195	119, 194	sylan2b 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
196	195	rexbidva 2474	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
197	118, 196	mpbid 147	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
198	26	rexeqi 2677	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
199	197, 198	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
200	199	anim1i 340	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
201		fveq2 5515	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ≥‘𝑚) = (ℤ≥‘𝑀))
202	201	sseq2d 3185	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑀)))
203	201	raleqdv 2678	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴))
204	202, 203	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ↔ (𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)))
205	201	rexeqdv 2679	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
206		seqeq1 10447	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
207	206	breq1d 4013	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
208	205, 207	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → ((∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
209	204, 208	anbi12d 473	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))))
210	209	rspcev 2841	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
211	114, 117, 200, 210	syl12anc 1236	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
212	211	orcd 733	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
213	212	ex 115	. . . . 5 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
214	113, 213	impbid 129	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
215		eluzelz 9536	. . . . . . . 8 ⊢ (𝑝 ∈ (ℤ≥‘𝑀) → 𝑝 ∈ ℤ)
216		simpr 110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
217	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
218	216, 217, 145	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
219		1cnd 7972	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
220	29	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
221	26	eleq2i 2244	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑍 ↔ 𝑝 ∈ (ℤ≥‘𝑀))
222	221	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (ℤ≥‘𝑀) → 𝑝 ∈ 𝑍)
223	222	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → 𝑝 ∈ 𝑍)
224	149, 220, 223	rspcdva 2846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → DECID 𝑝 ∈ 𝐴)
225	218, 219, 224	ifcldadc 3563	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
226		nfcv 2319	. . . . . . . . 9 ⊢ Ⅎ𝑘𝑝
227	226, 132, 137, 185	fvmptf 5608	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
228	215, 225, 227	syl2an2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
229	228, 225	eqeltrd 2254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) ∈ ℂ)
230		eluzelz 9536	. . . . . . . 8 ⊢ (𝑟 ∈ (ℤ≥‘𝑀) → 𝑟 ∈ ℤ)
231		simpr 110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
232	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
233	231, 232, 176	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
234		1cnd 7972	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
235	29	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
236	26	eleq2i 2244	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ 𝑍 ↔ 𝑟 ∈ (ℤ≥‘𝑀))
237	236	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (ℤ≥‘𝑀) → 𝑟 ∈ 𝑍)
238	237	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → 𝑟 ∈ 𝑍)
239	180, 235, 238	rspcdva 2846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → DECID 𝑟 ∈ 𝐴)
240	233, 234, 239	ifcldadc 3563	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ)
241	230, 240, 186	syl2an2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
242	128	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
243	238, 242, 169	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
244	241, 243	eqtr4d 2213	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = (𝐹‘𝑟))
245	189	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
246	22, 229, 244, 245	seq3feq 10471	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
247	246	breq1d 4013	. . . 4 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
248	214, 247	bitrd 188	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
249	248	iotabidv 5199	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
250		df-proddc 11558	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
251		df-fv 5224	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
252	249, 250, 251	3eqtr4g 2235	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834   = wceq 1353  ∃wex 1492   ∈ wcel 2148  ∀wral 2455  ∃wrex 2456  ⦋csb 3057   ⊆ wss 3129  ifcif 3534   class class class wbr 4003   ↦ cmpt 4064  ℩cio 5176  –1-1-onto→wf1o 5215  ‘cfv 5216   Isom wiso 5217  (class class class)co 5874   ≈ cen 6737  Fincfn 6739  ℂcc 7808  0cc0 7810  1c1 7811   · cmul 7815   < clt 7991   ≤ cle 7992   # cap 8537  ℕcn 8918  ℕ₀cn0 9175  ℤcz 9252  ℤ_≥cuz 9527  ...cfz 10007  seqcseq 10444  ♯chash 10754   ⇝ cli 11285  ∏cprod 11557

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

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-seqfrec 10445  df-exp 10519  df-ihash 10755  df-cj 10850  df-rsqrt 11006  df-abs 11007  df-clim 11286  df-proddc 11558

This theorem is referenced by:  iprodap  11587  zprodap0  11588  prodssdc  11596