Theorem prodss 15295

Description: Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.)

Hypotheses

Ref	Expression
prodss.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
prodss.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
prodss.3	⊢ (𝜑 → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))
prodss.4	⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1)
prodss.5	⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))

Assertion

Ref	Expression
prodss	⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)

Distinct variable groups:   𝐴,𝑘,𝑛,𝑦   𝐵,𝑘,𝑛,𝑦   𝐶,𝑛,𝑦   𝑘,𝑛,𝜑,𝑦   𝑛,𝑀,𝑦   𝜑,𝑛,𝑦   𝑘,𝑀

Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem prodss

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2821	. . . . 5 ⊢ (ℤ≥‘𝑀) = (ℤ≥‘𝑀)
2		simpr 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ)
3		prodss.3	. . . . . 6 ⊢ (𝜑 → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))
4	3	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∃𝑛 ∈ (ℤ≥‘𝑀)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))
5		prodss.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
6		prodss.5	. . . . . . 7 ⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀))
7	5, 6	sstrd 3976	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀))
8	7	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑀))
9		simpr 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ (ℤ≥‘𝑀))
10		iftrue 4472	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝐵 → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) = ⦋𝑚 / 𝑘⦌𝐶)
11	10	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) = ⦋𝑚 / 𝑘⦌𝐶)
12		prodss.2	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
13	12	ex 415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
14	13	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
15		eldif 3945	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴))
16		prodss.4	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 1)
17		ax-1cn 10589	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
18	16, 17	eqeltrdi 2921	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ)
19	15, 18	sylan2br 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ)
20	19	expr 459	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
21	14, 20	pm2.61d 181	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
22	21	ralrimiva 3182	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
23		nfcsb1v 3906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐶
24	23	nfel1 2994	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ
25		csbeq1a 3896	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → 𝐶 = ⦋𝑚 / 𝑘⦌𝐶)
26	25	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → (𝐶 ∈ ℂ ↔ ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ))
27	24, 26	rspc 3610	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ))
28	22, 27	mpan9 509	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ)
29	11, 28	eqeltrd 2913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
30		iffalse 4475	. . . . . . . . . . . 12 ⊢ (¬ 𝑚 ∈ 𝐵 → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) = 1)
31	30, 17	eqeltrdi 2921	. . . . . . . . . . 11 ⊢ (¬ 𝑚 ∈ 𝐵 → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
32	31	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
33	29, 32	pm2.61dan 811	. . . . . . . . 9 ⊢ (𝜑 → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
34	33	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
35	34	adantr 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ)
36		nfcv 2977	. . . . . . . 8 ⊢ Ⅎ𝑘𝑚
37		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝑚 ∈ 𝐵
38		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑘1
39	37, 23, 38	nfif 4495	. . . . . . . 8 ⊢ Ⅎ𝑘if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1)
40		eleq1w 2895	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐵 ↔ 𝑚 ∈ 𝐵))
41	40, 25	ifbieq1d 4489	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐵, 𝐶, 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
42		eqid 2821	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1)) = (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))
43	36, 39, 41, 42	fvmptf 6783	. . . . . . 7 ⊢ ((𝑚 ∈ (ℤ≥‘𝑀) ∧ if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
44	9, 35, 43	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
45		iftrue 4472	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝐴 → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))
46	45	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))
47		simpr 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐴)
48	5	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ 𝐵)
49	48	sselda 3966	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐵)
50	28	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ)
51	49, 50	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ)
52		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶)
53	52	fvmpts 6765	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ 𝐴 ∧ ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ⦋𝑚 / 𝑘⦌𝐶)
54	47, 51, 53	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ⦋𝑚 / 𝑘⦌𝐶)
55	46, 54	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶)
56	55	ex 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑚 ∈ 𝐴 → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶))
57	56	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → (𝑚 ∈ 𝐴 → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶))
58		iffalse 4475	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑚 ∈ 𝐴 → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = 1)
59	58	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ 𝐵 ∧ ¬ 𝑚 ∈ 𝐴) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = 1)
60	59	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ (𝑚 ∈ 𝐵 ∧ ¬ 𝑚 ∈ 𝐴)) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = 1)
61		eldif 3945	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (𝐵 ∖ 𝐴) ↔ (𝑚 ∈ 𝐵 ∧ ¬ 𝑚 ∈ 𝐴))
62	16	ralrimiva 3182	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑘 ∈ (𝐵 ∖ 𝐴)𝐶 = 1)
63	62	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∀𝑘 ∈ (𝐵 ∖ 𝐴)𝐶 = 1)
64	23	nfeq1 2993	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐶 = 1
65	25	eqeq1d 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → (𝐶 = 1 ↔ ⦋𝑚 / 𝑘⦌𝐶 = 1))
66	64, 65	rspc 3610	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐵 ∖ 𝐴) → (∀𝑘 ∈ (𝐵 ∖ 𝐴)𝐶 = 1 → ⦋𝑚 / 𝑘⦌𝐶 = 1))
67	63, 66	mpan9 509	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (𝐵 ∖ 𝐴)) → ⦋𝑚 / 𝑘⦌𝐶 = 1)
68	61, 67	sylan2br 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ (𝑚 ∈ 𝐵 ∧ ¬ 𝑚 ∈ 𝐴)) → ⦋𝑚 / 𝑘⦌𝐶 = 1)
69	60, 68	eqtr4d 2859	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ (𝑚 ∈ 𝐵 ∧ ¬ 𝑚 ∈ 𝐴)) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶)
70	69	expr 459	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → (¬ 𝑚 ∈ 𝐴 → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶))
71	57, 70	pm2.61d 181	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = ⦋𝑚 / 𝑘⦌𝐶)
72	10	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) = ⦋𝑚 / 𝑘⦌𝐶)
73	71, 72	eqtr4d 2859	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
74	48	ssneld 3968	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (¬ 𝑚 ∈ 𝐵 → ¬ 𝑚 ∈ 𝐴))
75	74	imp 409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑚 ∈ 𝐵) → ¬ 𝑚 ∈ 𝐴)
76	75, 58	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = 1)
77	30	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) = 1)
78	76, 77	eqtr4d 2859	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
79	73, 78	pm2.61dan 811	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
80	79	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
81	44, 80	eqtr4d 2859	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 1))
82	12	fmpttd 6873	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
83	82	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
84	83	ffvelrnda 6845	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ)
85	1, 2, 4, 8, 81, 84	zprod 15285	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ( ⇝ ‘seq𝑀( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1)))))
86	6	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝐵 ⊆ (ℤ≥‘𝑀))
87	43	ancoms 461	. . . . . . 7 ⊢ ((if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1) ∈ ℂ ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
88	34, 87	sylan 582	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
89		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → 𝑚 ∈ 𝐵)
90		eqid 2821	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
91	90	fvmpts 6765	. . . . . . . . . 10 ⊢ ((𝑚 ∈ 𝐵 ∧ ⦋𝑚 / 𝑘⦌𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ⦋𝑚 / 𝑘⦌𝐶)
92	89, 50, 91	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ⦋𝑚 / 𝑘⦌𝐶)
93	92	ifeq1d 4484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
94	93	adantlr 713	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
95		iffalse 4475	. . . . . . . . 9 ⊢ (¬ 𝑚 ∈ 𝐵 → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = 1)
96	95, 30	eqtr4d 2859	. . . . . . . 8 ⊢ (¬ 𝑚 ∈ 𝐵 → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
97	96	adantl 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑚 ∈ 𝐵) → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
98	94, 97	pm2.61dan 811	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1) = if(𝑚 ∈ 𝐵, ⦋𝑚 / 𝑘⦌𝐶, 1))
99	88, 98	eqtr4d 2859	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 1))
100	21	fmpttd 6873	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
101	100	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
102	101	ffvelrnda 6845	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ)
103	1, 2, 4, 86, 99, 102	zprod 15285	. . . 4 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ( ⇝ ‘seq𝑀( · , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐵, 𝐶, 1)))))
104	85, 103	eqtr4d 2859	. . 3 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
105		prodfc 15293	. . 3 ⊢ ∏𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐴 𝐶
106		prodfc 15293	. . 3 ⊢ ∏𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ∏𝑘 ∈ 𝐵 𝐶
107	104, 105, 106	3eqtr3g 2879	. 2 ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
108	5	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ 𝐵)
109	6	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐵 ⊆ (ℤ≥‘𝑀))
110		uzf 12240	. . . . . . . . . . 11 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
111	110	fdmi 6518	. . . . . . . . . 10 ⊢ dom ℤ≥ = ℤ
112	111	eleq2i 2904	. . . . . . . . 9 ⊢ (𝑀 ∈ dom ℤ≥ ↔ 𝑀 ∈ ℤ)
113		ndmfv 6694	. . . . . . . . 9 ⊢ (¬ 𝑀 ∈ dom ℤ≥ → (ℤ≥‘𝑀) = ∅)
114	112, 113	sylnbir 333	. . . . . . . 8 ⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅)
115	114	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → (ℤ≥‘𝑀) = ∅)
116	109, 115	sseqtrd 4006	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐵 ⊆ ∅)
117	108, 116	sstrd 3976	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ ∅)
118		ss0 4351	. . . . 5 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)
119	117, 118	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 = ∅)
120		ss0 4351	. . . . 5 ⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅)
121	116, 120	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐵 = ∅)
122	119, 121	eqtr4d 2859	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 = 𝐵)
123	122	prodeq1d 15269	. 2 ⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)
124	107, 123	pm2.61dan 811	1 ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1533  ∃wex 1776   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  ⦋csb 3882   ∖ cdif 3932   ⊆ wss 3935  ∅c0 4290  ifcif 4466  𝒫 cpw 4538   class class class wbr 5058   ↦ cmpt 5138  dom cdm 5549  ⟶wf 6345  ‘cfv 6349  ℂcc 10529  0cc0 10531  1c1 10532   · cmul 10536  ℤcz 11975  ℤ_≥cuz 12237  seqcseq 13363   ⇝ cli 14835  ∏cprod 15253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12384  df-fz 12887  df-fzo 13028  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-prod 15254

This theorem is referenced by:  fprodss  15296