zproddc - Intuitionistic Logic Explorer

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

Theorem zproddc 11453

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 519	. . . . . . . . 9 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
2		simprr 522	. . . . . . . . 9 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
3	1, 2	jca 304	. . . . . . . 8 ⊢ (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
4		nfcv 2296	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖if(𝑘 ∈ 𝐴, 𝐵, 1)
5		nfv 1505	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘 𝑖 ∈ 𝐴
6		nfcsb1v 3060	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
7		nfcv 2296	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘1
8	5, 6, 7	nfif 3529	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1)
9		eleq1w 2215	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
10		csbeq1a 3036	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
11	9, 10	ifbieq1d 3523	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
12	4, 8, 11	cbvmpt 4055	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 1))
13		simpll 519	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝜑)
14		zprod.6	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
15	14	ralrimiva 2527	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
16	6	nfel1 2307	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
17	10	eleq1d 2223	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
18	16, 17	rspc 2807	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
19	15, 18	syl5 32	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (𝜑 → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
20	13, 19	mpan9 279	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
21		simplr 520	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
22		zprod.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23	22	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
24		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
25		zprod.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
26		zprod.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
27	25, 26	sseqtrdi 3172	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
28	27	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
29		zproddc.dc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
30	26	raleqi 2653	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
31	29, 30	sylib 121	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
32		eleq1w 2215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
33	32	dcbid 824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑖 ∈ 𝐴))
34	33	cbvralv 2677	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
35	31, 34	sylib 121	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
36	35	r19.21bi 2542	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
37	36	adantlr 469	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
38	37	adantlr 469	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
39	38	adantlr 469	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
40		simp-4l 531	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝜑)
41		simpr 109	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ (ℤ_≥‘𝑀))
42	27	ssneld 3126	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ 𝑖 ∈ (ℤ_≥‘𝑀) → ¬ 𝑖 ∈ 𝐴))
43	40, 41, 42	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ 𝐴)
44	43	olcd 724	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
45		df-dc 821	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ 𝐴 ↔ (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
46	44, 45	sylibr 133	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
47		eluzelz 9427	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘𝑚) → 𝑖 ∈ ℤ)
48		eluzdc 9499	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
49	23, 47, 48	syl2an 287	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
50		exmiddc 822	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ (ℤ_≥‘𝑀) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
51	49, 50	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
52	39, 46, 51	mpjaodan 788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ 𝐴)
53	12, 20, 21, 23, 24, 28, 52, 38	prodrbdc 11448	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
54	53	biimpd 143	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
55	54	expimpd 361	. . . . . . . 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 2571	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
58		uzssz 9437	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
59	27, 58	sstrdi 3136	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
60	59	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℤ)
61		1zzd 9173	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
62		nnz 9165	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
63	62	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
64	63	adantr 274	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
65	61, 64	fzfigd 10308	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
66		simpr 109	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
67		f1oeng 6691	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
68	65, 66, 67	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
69	68	ensymd 6717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
70		enfii 6808	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
71	65, 69, 70	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
72		zfz1iso 10689	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
73	60, 71, 72	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
74		simpll 519	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝜑)
75	74, 19	mpan9 279	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
76		breq1 3964	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
77		fveq2 5461	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
78	77	csbeq1d 3034	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
79	76, 78	ifbieq1d 3523	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
80		csbcow 3038	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
81		ifeq1 3504	. . . . . . . . . . . . . . . . . 18 ⊢ (⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 → if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1))
82	80, 81	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑘⦌𝐵, 1)
83	79, 82	eqtr4di 2205	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
84	83	cbvmptv 4056	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
85		eqid 2154	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 1))
86	36	ad4ant14 506	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
87		simplr 520	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
88	22	ad2antrr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
89	27	ad2antrr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
90		simprl 521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
91		simprr 522	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
92	12, 75, 84, 85, 86, 87, 88, 89, 90, 91	prodmodclem2a 11450	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
93	65	adantrr 471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
94	93, 90	fihasheqf1od 10641	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
95	87	nnnn0d 9122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ₀)
96		hashfz1 10634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
97	95, 96	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
98	94, 97	eqtr3d 2189	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
99	98	breq2d 3973	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
100	99	ifbid 3522	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))
101	100	mpteq2dv 4051	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))
102	101	seqeq3d 10330	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))))
103	102	fveq1d 5463	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
104	92, 103	breqtrd 3986	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
105	104	expr 373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
106	105	exlimdv 1796	. . . . . . . . . . 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 3965	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
109	107, 108	syl5ibrcom 156	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
110	109	expimpd 361	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
111	110	exlimdv 1796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
112	111	rexlimdva 2571	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
113	57, 112	jaod 707	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
114	22	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
115	27	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → 𝐴 ⊆ (ℤ_≥‘𝑀))
116	31	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
117	115, 116	jca 304	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴))
118		zproddc.3	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦))
119	26	eleq2i 2221	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ_≥‘𝑀))
120		eluzelz 9427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (ℤ_≥‘𝑀) → 𝑛 ∈ ℤ)
121	120	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑛 ∈ ℤ)
122		simpr 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → 𝑝 ∈ (ℤ_≥‘𝑛))
123		simplr 520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → 𝑛 ∈ (ℤ_≥‘𝑀))
124		uztrn 9434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ (ℤ_≥‘𝑛) ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑝 ∈ (ℤ_≥‘𝑀))
125	122, 123, 124	syl2anc 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → 𝑝 ∈ (ℤ_≥‘𝑀))
126	125, 26	eleqtrrdi 2248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → 𝑝 ∈ 𝑍)
127		zprod.5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
128	127	ralrimiva 2527	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
129	128	ad2antrr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
130		nfv 1505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑝 ∈ 𝐴
131		nfcsb1v 3060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵
132	130, 131, 7	nfif 3529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
133	132	nfeq2 2308	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)
134		fveq2 5461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐹‘𝑘) = (𝐹‘𝑝))
135		eleq1w 2215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → (𝑘 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
136		csbeq1a 3036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑝 → 𝐵 = ⦋𝑝 / 𝑘⦌𝐵)
137	135, 136	ifbieq1d 3523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
138	134, 137	eqeq12d 2169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑝 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)))
139	133, 138	rspc 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) → (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1)))
140	126, 129, 139	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
141		simpr 109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
142	15	ad3antrrr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
143	131	nfel1 2307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ
144	136	eleq1d 2223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑝 → (𝐵 ∈ ℂ ↔ ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
145	143, 144	rspc 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ))
146	141, 142, 145	sylc 62	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
147		1cnd 7873	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
148		eleq1w 2215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑝 → (𝑗 ∈ 𝐴 ↔ 𝑝 ∈ 𝐴))
149	148	dcbid 824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑝 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑝 ∈ 𝐴))
150	29	ad2antrr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
151	149, 150, 126	rspcdva 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → DECID 𝑝 ∈ 𝐴)
152	146, 147, 151	ifcldadc 3530	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
153	140, 152	eqeltrd 2231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑝) ∈ ℂ)
154		simpr 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ (ℤ_≥‘𝑛))
155		simplr 520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → 𝑛 ∈ (ℤ_≥‘𝑀))
156		uztrn 9434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑟 ∈ (ℤ_≥‘𝑛) ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → 𝑟 ∈ (ℤ_≥‘𝑀))
157	154, 155, 156	syl2anc 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ (ℤ_≥‘𝑀))
158	157, 26	eleqtrrdi 2248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ 𝑍)
159	128	ad2antrr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
160		nfv 1505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘 𝑟 ∈ 𝐴
161		nfcsb1v 3060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵
162	160, 161, 7	nfif 3529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
163	162	nfeq2 2308	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)
164		fveq2 5461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → (𝐹‘𝑘) = (𝐹‘𝑟))
165		eleq1w 2215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝑘 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
166		csbeq1a 3036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → 𝐵 = ⦋𝑟 / 𝑘⦌𝐵)
167	165, 166	ifbieq1d 3523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑟 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
168	164, 167	eqeq12d 2169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑟 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) ↔ (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
169	163, 168	rspc 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1)))
170	158, 159, 169	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
171	58, 157	sseldi 3122	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → 𝑟 ∈ ℤ)
172		simpr 109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
173	15	ad3antrrr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
174	161	nfel1 2307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑘⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ
175	166	eleq1d 2223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑟 → (𝐵 ∈ ℂ ↔ ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
176	174, 175	rspc 2807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ))
177	172, 173, 176	sylc 62	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
178		1cnd 7873	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
179		eleq1w 2215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑟 → (𝑗 ∈ 𝐴 ↔ 𝑟 ∈ 𝐴))
180	179	dcbid 824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑟 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑟 ∈ 𝐴))
181	29	ad2antrr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
182	180, 181, 158	rspcdva 2818	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → DECID 𝑟 ∈ 𝐴)
183	177, 178, 182	ifcldadc 3530	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ)
184		nfcv 2296	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘𝑟
185		eqid 2154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
186	184, 162, 167, 185	fvmptf 5553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑟 ∈ ℤ ∧ if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
187	171, 183, 186	syl2anc 409	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
188	170, 187	eqtr4d 2190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑟) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟))
189		mulcl 7838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝 · 𝑞) ∈ ℂ)
190	189	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
191	121, 153, 188, 190	seq3feq 10349	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → seq𝑛( · , 𝐹) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
192	191	breq1d 3971	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (seq𝑛( · , 𝐹) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
193	192	anbi2d 460	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → ((𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
194	193	exbidv 1802	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝑀)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
195	119, 194	sylan2b 285	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
196	195	rexbidva 2451	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
197	118, 196	mpbid 146	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
198	26	rexeqi 2654	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
199	197, 198	sylib 121	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦))
200	199	anim1i 338	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
201		fveq2 5461	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
202	201	sseq2d 3154	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑀)))
203	201	raleqdv 2655	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴))
204	202, 203	anbi12d 465	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ↔ (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)))
205	201	rexeqdv 2656	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)))
206		seqeq1 10325	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))))
207	206	breq1d 3971	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
208	205, 207	anbi12d 465	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → ((∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
209	204, 208	anbi12d 465	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → (((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))))
210	209	rspcev 2813	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ ((𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑀)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
211	114, 117, 200, 210	syl12anc 1215	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)))
212	211	orcd 723	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
213	212	ex 114	. . . . 5 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))))
214	113, 213	impbid 128	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
215		eluzelz 9427	. . . . . . . 8 ⊢ (𝑝 ∈ (ℤ_≥‘𝑀) → 𝑝 ∈ ℤ)
216		simpr 109	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐴)
217	15	ad2antrr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
218	216, 217, 145	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) ∧ 𝑝 ∈ 𝐴) → ⦋𝑝 / 𝑘⦌𝐵 ∈ ℂ)
219		1cnd 7873	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑝 ∈ 𝐴) → 1 ∈ ℂ)
220	29	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
221	26	eleq2i 2221	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ 𝑍 ↔ 𝑝 ∈ (ℤ_≥‘𝑀))
222	221	biimpri 132	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (ℤ_≥‘𝑀) → 𝑝 ∈ 𝑍)
223	222	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → 𝑝 ∈ 𝑍)
224	149, 220, 223	rspcdva 2818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → DECID 𝑝 ∈ 𝐴)
225	218, 219, 224	ifcldadc 3530	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ)
226		nfcv 2296	. . . . . . . . 9 ⊢ Ⅎ𝑘𝑝
227	226, 132, 137, 185	fvmptf 5553	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1) ∈ ℂ) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
228	215, 225, 227	syl2an2 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) = if(𝑝 ∈ 𝐴, ⦋𝑝 / 𝑘⦌𝐵, 1))
229	228, 225	eqeltrd 2231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑝) ∈ ℂ)
230		eluzelz 9427	. . . . . . . 8 ⊢ (𝑟 ∈ (ℤ_≥‘𝑀) → 𝑟 ∈ ℤ)
231		simpr 109	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
232	15	ad2antrr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
233	231, 232, 176	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) ∧ 𝑟 ∈ 𝐴) → ⦋𝑟 / 𝑘⦌𝐵 ∈ ℂ)
234		1cnd 7873	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑟 ∈ 𝐴) → 1 ∈ ℂ)
235	29	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → ∀𝑗 ∈ 𝑍 DECID 𝑗 ∈ 𝐴)
236	26	eleq2i 2221	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ 𝑍 ↔ 𝑟 ∈ (ℤ_≥‘𝑀))
237	236	biimpri 132	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (ℤ_≥‘𝑀) → 𝑟 ∈ 𝑍)
238	237	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → 𝑟 ∈ 𝑍)
239	180, 235, 238	rspcdva 2818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → DECID 𝑟 ∈ 𝐴)
240	233, 234, 239	ifcldadc 3530	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1) ∈ ℂ)
241	230, 240, 186	syl2an2 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
242	128	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 1))
243	238, 242, 169	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑟) = if(𝑟 ∈ 𝐴, ⦋𝑟 / 𝑘⦌𝐵, 1))
244	241, 243	eqtr4d 2190	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (ℤ_≥‘𝑀)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑟) = (𝐹‘𝑟))
245	189	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ (𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ)) → (𝑝 · 𝑞) ∈ ℂ)
246	22, 229, 244, 245	seq3feq 10349	. . . . 5 ⊢ (𝜑 → seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑀( · , 𝐹))
247	246	breq1d 3971	. . . 4 ⊢ (𝜑 → (seq𝑀( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
248	214, 247	bitrd 187	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))) ↔ seq𝑀( · , 𝐹) ⇝ 𝑥))
249	248	iotabidv 5149	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥))
250		df-proddc 11425	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ_≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
251		df-fv 5171	. 2 ⊢ ( ⇝ ‘seq𝑀( · , 𝐹)) = (℩𝑥seq𝑀( · , 𝐹) ⇝ 𝑥)
252	249, 250, 251	3eqtr4g 2212	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( · , 𝐹)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 DECID wdc 820 = wceq 1332 ∃wex 1469 ∈ wcel 2125 ∀wral 2432 ∃wrex 2433 ⦋csb 3027 ⊆ wss 3098 ifcif 3501 class class class wbr 3961 ↦ cmpt 4021 ℩cio 5126 –1-1-onto→wf1o 5162 ‘cfv 5163 Isom wiso 5164 (class class class)co 5814 ≈ cen 6672 Fincfn 6674 ℂcc 7709 0cc0 7711 1c1 7712 · cmul 7716 < clt 7891 ≤ cle 7892 # cap 8435 ℕcn 8812 ℕ₀cn0 9069 ℤcz 9146 ℤ_≥cuz 9418 ...cfz 9890 seqcseq 10322 ♯chash 10626 ⇝ cli 11152 ∏cprod 11424

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-coll 4075 ax-sep 4078 ax-nul 4086 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-setind 4490 ax-iinf 4541 ax-cnex 7802 ax-resscn 7803 ax-1cn 7804 ax-1re 7805 ax-icn 7806 ax-addcl 7807 ax-addrcl 7808 ax-mulcl 7809 ax-mulrcl 7810 ax-addcom 7811 ax-mulcom 7812 ax-addass 7813 ax-mulass 7814 ax-distr 7815 ax-i2m1 7816 ax-0lt1 7817 ax-1rid 7818 ax-0id 7819 ax-rnegex 7820 ax-precex 7821 ax-cnre 7822 ax-pre-ltirr 7823 ax-pre-ltwlin 7824 ax-pre-lttrn 7825 ax-pre-apti 7826 ax-pre-ltadd 7827 ax-pre-mulgt0 7828 ax-pre-mulext 7829

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ne 2325 df-nel 2420 df-ral 2437 df-rex 2438 df-reu 2439 df-rmo 2440 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-if 3502 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-br 3962 df-opab 4022 df-mpt 4023 df-tr 4059 df-id 4248 df-po 4251 df-iso 4252 df-iord 4321 df-on 4323 df-ilim 4324 df-suc 4326 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-f1 5168 df-fo 5169 df-f1o 5170 df-fv 5171 df-isom 5172 df-riota 5770 df-ov 5817 df-oprab 5818 df-mpo 5819 df-1st 6078 df-2nd 6079 df-recs 6242 df-irdg 6307 df-frec 6328 df-1o 6353 df-oadd 6357 df-er 6469 df-en 6675 df-dom 6676 df-fin 6677 df-pnf 7893 df-mnf 7894 df-xr 7895 df-ltxr 7896 df-le 7897 df-sub 8027 df-neg 8028 df-reap 8429 df-ap 8436 df-div 8525 df-inn 8813 df-2 8871 df-n0 9070 df-z 9147 df-uz 9419 df-q 9507 df-rp 9539 df-fz 9891 df-fzo 10020 df-seqfrec 10323 df-exp 10397 df-ihash 10627 df-cj 10719 df-rsqrt 10875 df-abs 10876 df-clim 11153 df-proddc 11425

This theorem is referenced by: iprodap 11454 zprodap0 11455 prodssdc 11463

W3C validator