Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )