Theorem zproddc 11601

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 2329	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
5		nfv 1538	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
6		nfcsb1v 3102	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
7		nfcv 2329	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
8	5, 6, 7	nfif 3574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
9		eleq1w 2248	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
10		csbeq1a 3078	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
11	9, 10	ifbieq1d 3568	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
12	4, 8, 11	cbvmpt 4110	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
13		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝜑)
14		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
15	14	ralrimiva 2560	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
16	6	nfel1 2340	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
17	10	eleq1d 2256	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	16, 17	rspc 2847	. . . . . . . . . . . . 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 3215	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))
28	27	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) → 𝐴 ⊆ (ℤ≥‘𝑀))
29		zproddc.dc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
30	26	raleqi 2687	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
31	29, 30	sylib 122	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)
32		eleq1w 2248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
33	32	dcbid 839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑖 ∈ 𝐴))
34	33	cbvralv 2715	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑖 ∈ (ℤ≥‘𝑀)DECID 𝑖 ∈ 𝐴)
35	31, 34	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ (ℤ≥‘𝑀)DECID 𝑖 ∈ 𝐴)
36	35	r19.21bi 2575	. . . . . . . . . . . . . . 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 3169	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ 𝑖 ∈ (ℤ≥‘𝑀) → ¬ 𝑖 ∈ 𝐴))
43	40, 41, 42	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → ¬ 𝑖 ∈ 𝐴)
44	43	olcd 735	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
45		df-dc 836	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ 𝐴 ↔ (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
46	44, 45	sylibr 134	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
47		eluzelz 9551	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ≥‘𝑚) → 𝑖 ∈ ℤ)
48		eluzdc 9624	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ≥‘𝑀))
49	23, 47, 48	syl2an 289	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → DECID 𝑖 ∈ (ℤ≥‘𝑀))
50		exmiddc 837	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ (ℤ≥‘𝑀) → (𝑖 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ≥‘𝑀)))
51	49, 50	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → (𝑖 ∈ (ℤ≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ≥‘𝑀)))
52	39, 46, 51	mpjaodan 799	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ≥‘𝑚)) ∧ 𝑖 ∈ (ℤ≥‘𝑚)) → DECID 𝑖 ∈ 𝐴)
53	12, 20, 21, 23, 24, 28, 52, 38	prodrbdc 11596	. . . . . . . . . 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 2604	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
58		uzssz 9561	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
59	27, 58	sstrdi 3179	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
60	59	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℤ)
61		1zzd 9294	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
62		nnz 9286	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
63	62	adantl 277	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
64	63	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
65	61, 64	fzfigd 10445	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
66		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
67		f1oeng 6771	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
68	65, 66, 67	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
69	68	ensymd 6797	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
70		enfii 6888	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
71	65, 69, 70	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
72		zfz1iso 10835	. . . . . . . . . . . 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 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
77		fveq2 5527	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
78	77	csbeq1d 3076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
79	76, 78	ifbieq1d 3568	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
80		csbcow 3080	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
81		ifeq1 3549	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)
83	79, 82	eqtr4di 2238	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
84	83	cbvmptv 4111	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
85		eqid 2187	. . . . . . . . . . . . . . 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 11598	. . . . . . . . . . . . . 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 10783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
95	87	nnnn0d 9243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ0)
96		hashfz1 10777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ0 → (♯‘(1...𝑚)) = 𝑚)
97	95, 96	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
98	94, 97	eqtr3d 2222	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
99	98	breq2d 4027	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
100	99	ifbid 3567	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))
101	100	mpteq2dv 4106	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))
102	101	seqeq3d 10467	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))))
103	102	fveq1d 5529	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
104	92, 103	breqtrd 4041	. . . . . . . . . . . . 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 1829	. . . . . . . . . . 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 4019	. . . . . . . . . 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 1829	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
112	111	rexlimdva 2604	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
113	57, 112	jaod 718	. . . . 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 2254	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑀))
120		eluzelz 9551	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → 𝑛 ∈ ℤ)
121	120	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ ℤ)
122		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ (ℤ≥‘𝑛))
123		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ (ℤ≥‘𝑀))
124		uztrn 9558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ (ℤ≥‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑝 ∈ (ℤ≥‘𝑀))
125	122, 123, 124	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ (ℤ≥‘𝑀))
126	125, 26	eleqtrrdi 2281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → 𝑝 ∈ 𝑍)
127		zprod.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
128	127	ralrimiva 2560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
129	128	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
130		nfv 1538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑝 ∈ 𝐴
131		nfcsb1v 3102	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵
132	130, 131, 7	nfif 3574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
133	132	nfeq2 2341	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
134		fveq2 5527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐹‘𝑘) = (𝐹‘𝑝))
135		eleq1w 2248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → (𝑘 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
136		csbeq1a 3078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → 𝐵 = ⦋𝑝 / 𝑘⦌𝐵)
137	135, 136	ifbieq1d 3568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
138	134, 137	eqeq12d 2202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑝 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)))
139	133, 138	rspc 2847	. . . . . . . . . . . . . . . . . . 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 2340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ
144	136	eleq1d 2256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐵 ∈ ℂ ↔ ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
145	143, 144	rspc 2847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
146	141, 142, 145	sylc 62	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
147		1cnd 7987	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
148		eleq1w 2248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑝 → (𝑗 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
149	148	dcbid 839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑝 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑝 ∈ 𝐴))
150	29	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
151	149, 150, 126	rspcdva 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → DECID 𝑝 ∈ 𝐴)
152	146, 147, 151	ifcldadc 3575	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
153	140, 152	eqeltrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑝) ∈ ℂ)
154		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ (ℤ≥‘𝑛))
155		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ (ℤ≥‘𝑀))
156		uztrn 9558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑟 ∈ (ℤ≥‘𝑛) ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑟 ∈ (ℤ≥‘𝑀))
157	154, 155, 156	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ (ℤ≥‘𝑀))
158	157, 26	eleqtrrdi 2281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ 𝑍)
159	128	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
160		nfv 1538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑟 ∈ 𝐴
161		nfcsb1v 3102	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵
162	160, 161, 7	nfif 3574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
163	162	nfeq2 2341	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
164		fveq2 5527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → (𝐹‘𝑘) = (𝐹‘𝑟))
165		eleq1w 2248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝑘 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
166		csbeq1a 3078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → 𝐵 = ⦋𝑟 / 𝑘⦌𝐵)
167	165, 166	ifbieq1d 3568	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
168	164, 167	eqeq12d 2202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑟 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
169	163, 168	rspc 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
170	158, 159, 169	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
171	58, 157	sselid 3165	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℤ)
172		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
173	15	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
174	161	nfel1 2340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ
175	166	eleq1d 2256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝐵 ∈ ℂ ↔ ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
176	174, 175	rspc 2847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
177	172, 173, 176	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
178		1cnd 7987	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
179		eleq1w 2248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑟 → (𝑗 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
180	179	dcbid 839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑟 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑟 ∈ 𝐴))
181	29	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
182	180, 181, 158	rspcdva 2858	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → DECID 𝑟 ∈ 𝐴)
183	177, 178, 182	ifcldadc 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ)
184		nfcv 2329	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘𝑟
185		eqid 2187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
186	184, 162, 167, 185	fvmptf 5621	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ ℤ ∧ if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
187	171, 183, 186	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
188	170, 187	eqtr4d 2223	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑟) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟))
189		mulcl 7952	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
190	189	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
191	121, 153, 188, 190	seq3feq 10486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
192	191	breq1d 4025	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
193	192	anbi2d 464	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
194	193	exbidv 1835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
195	119, 194	sylan2b 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
196	195	rexbidva 2484	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
197	118, 196	mpbid 147	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
198	26	rexeqi 2688	. . . . . . . . . 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 5527	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ≥‘𝑚) = (ℤ≥‘𝑀))
202	201	sseq2d 3197	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑀)))
203	201	raleqdv 2689	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴))
204	202, 203	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ↔ (𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴)))
205	201	rexeqdv 2690	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
206		seqeq1 10462	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
207	206	breq1d 4025	. . . . . . . . . . 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 2853	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐴 ⊆ (ℤ≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
211	114, 117, 200, 210	syl12anc 1246	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
212	211	orcd 734	. . . . . 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 9551	. . . . . . . 8 ⊢ (𝑝 ∈ (ℤ≥‘𝑀) → 𝑝 ∈ ℤ)
216		simpr 110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
217	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
218	216, 217, 145	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
219		1cnd 7987	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
220	29	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
221	26	eleq2i 2254	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑍 ↔ 𝑝 ∈ (ℤ≥‘𝑀))
222	221	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (ℤ≥‘𝑀) → 𝑝 ∈ 𝑍)
223	222	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → 𝑝 ∈ 𝑍)
224	149, 220, 223	rspcdva 2858	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → DECID 𝑝 ∈ 𝐴)
225	218, 219, 224	ifcldadc 3575	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
226		nfcv 2329	. . . . . . . . 9 ⊢ Ⅎ𝑘𝑝
227	226, 132, 137, 185	fvmptf 5621	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
228	215, 225, 227	syl2an2 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
229	228, 225	eqeltrd 2264	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) ∈ ℂ)
230		eluzelz 9551	. . . . . . . 8 ⊢ (𝑟 ∈ (ℤ≥‘𝑀) → 𝑟 ∈ ℤ)
231		simpr 110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
232	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
233	231, 232, 176	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
234		1cnd 7987	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
235	29	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
236	26	eleq2i 2254	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ 𝑍 ↔ 𝑟 ∈ (ℤ≥‘𝑀))
237	236	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (ℤ≥‘𝑀) → 𝑟 ∈ 𝑍)
238	237	adantl 277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → 𝑟 ∈ 𝑍)
239	180, 235, 238	rspcdva 2858	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → DECID 𝑟 ∈ 𝐴)
240	233, 234, 239	ifcldadc 3575	. . . . . . . 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 2223	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = (𝐹‘𝑟))
245	189	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
246	22, 229, 244, 245	seq3feq 10486	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
247	246	breq1d 4025	. . . 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 5211	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
250		df-proddc 11573	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
251		df-fv 5236	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
252	249, 250, 251	3eqtr4g 2245	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1363  ∃wex 1502   ∈ wcel 2158  ∀wral 2465  ∃wrex 2466  ⦋csb 3069   ⊆ wss 3141  ifcif 3546   class class class wbr 4015   ↦ cmpt 4076  ℩cio 5188  –1-1-onto→wf1o 5227  ‘cfv 5228   Isom wiso 5229  (class class class)co 5888   ≈ cen 6752  Fincfn 6754  ℂcc 7823  0cc0 7825  1c1 7826   · cmul 7830   < clt 8006   ≤ cle 8007   # cap 8552  ℕcn 8933  ℕ₀cn0 9190  ℤcz 9267  ℤ_≥cuz 9542  ...cfz 10022  seqcseq 10459  ♯chash 10769   ⇝ cli 11300  ∏cprod 11572

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-irdg 6385  df-frec 6406  df-1o 6431  df-oadd 6435  df-er 6549  df-en 6755  df-dom 6756  df-fin 6757  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-seqfrec 10460  df-exp 10534  df-ihash 10770  df-cj 10865  df-rsqrt 11021  df-abs 11022  df-clim 11301  df-proddc 11573

This theorem is referenced by:  iprodap  11602  zprodap0  11603  prodssdc  11611