Theorem prodss

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

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

Proof

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