# Metamath Proof Explorer

## Theorem fprod

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017)

Ref Expression
Hypotheses fprod.1 ( 𝑘 = ( 𝐹𝑛 ) → 𝐵 = 𝐶 )
fprod.2 ( 𝜑𝑀 ∈ ℕ )
fprod.3 ( 𝜑𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
fprod.4 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
fprod.5 ( ( 𝜑𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑛 ) = 𝐶 )
Assertion fprod ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )

### Proof

Step Hyp Ref Expression
1 fprod.1 ( 𝑘 = ( 𝐹𝑛 ) → 𝐵 = 𝐶 )
2 fprod.2 ( 𝜑𝑀 ∈ ℕ )
3 fprod.3 ( 𝜑𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴 )
4 fprod.4 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
5 fprod.5 ( ( 𝜑𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑛 ) = 𝐶 )
6 df-prod 𝑘𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
7 fvex ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V
8 nfcv 𝑗 if ( 𝑘𝐴 , 𝐵 , 1 )
9 nfv 𝑘 𝑗𝐴
10 nfcsb1v 𝑘 𝑗 / 𝑘 𝐵
11 nfcv 𝑘 1
12 9 10 11 nfif 𝑘 if ( 𝑗𝐴 , 𝑗 / 𝑘 𝐵 , 1 )
13 eleq1w ( 𝑘 = 𝑗 → ( 𝑘𝐴𝑗𝐴 ) )
14 csbeq1a ( 𝑘 = 𝑗𝐵 = 𝑗 / 𝑘 𝐵 )
15 13 14 ifbieq1d ( 𝑘 = 𝑗 → if ( 𝑘𝐴 , 𝐵 , 1 ) = if ( 𝑗𝐴 , 𝑗 / 𝑘 𝐵 , 1 ) )
16 8 12 15 cbvmpt ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) = ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝑗 / 𝑘 𝐵 , 1 ) )
17 4 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝐵 ∈ ℂ )
18 10 nfel1 𝑘 𝑗 / 𝑘 𝐵 ∈ ℂ
19 14 eleq1d ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ 𝑗 / 𝑘 𝐵 ∈ ℂ ) )
20 18 19 rspc ( 𝑗𝐴 → ( ∀ 𝑘𝐴 𝐵 ∈ ℂ → 𝑗 / 𝑘 𝐵 ∈ ℂ ) )
21 17 20 mpan9 ( ( 𝜑𝑗𝐴 ) → 𝑗 / 𝑘 𝐵 ∈ ℂ )
22 fveq2 ( 𝑛 = 𝑖 → ( 𝑓𝑛 ) = ( 𝑓𝑖 ) )
23 22 csbeq1d ( 𝑛 = 𝑖 ( 𝑓𝑛 ) / 𝑘 𝐵 = ( 𝑓𝑖 ) / 𝑘 𝐵 )
24 csbcow ( 𝑓𝑖 ) / 𝑗 𝑗 / 𝑘 𝐵 = ( 𝑓𝑖 ) / 𝑘 𝐵
25 23 24 eqtr4di ( 𝑛 = 𝑖 ( 𝑓𝑛 ) / 𝑘 𝐵 = ( 𝑓𝑖 ) / 𝑗 𝑗 / 𝑘 𝐵 )
26 25 cbvmptv ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) = ( 𝑖 ∈ ℕ ↦ ( 𝑓𝑖 ) / 𝑗 𝑗 / 𝑘 𝐵 )
27 16 21 26 prodmo ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
28 f1of ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
29 3 28 syl ( 𝜑𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
30 ovex ( 1 ... 𝑀 ) ∈ V
31 fex ( ( 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐹 ∈ V )
32 29 30 31 sylancl ( 𝜑𝐹 ∈ V )
33 nnuz ℕ = ( ℤ ‘ 1 )
34 2 33 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 1 ) )
35 elfznn ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ∈ ℕ )
36 fvex ( 𝐺𝑛 ) ∈ V
37 5 36 eqeltrrdi ( ( 𝜑𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝐶 ∈ V )
38 eqid ( 𝑛 ∈ ℕ ↦ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ 𝐶 )
39 38 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ 𝐶 ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
40 35 37 39 syl2an2 ( ( 𝜑𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
41 5 40 eqtr4d ( ( 𝜑𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) )
42 41 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... 𝑀 ) ( 𝐺𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) )
43 nffvmpt1 𝑛 ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 )
44 43 nfeq2 𝑛 ( 𝐺𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 )
45 fveq2 ( 𝑛 = 𝑘 → ( 𝐺𝑛 ) = ( 𝐺𝑘 ) )
46 fveq2 ( 𝑛 = 𝑘 → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) )
47 45 46 eqeq12d ( 𝑛 = 𝑘 → ( ( 𝐺𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) ↔ ( 𝐺𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) ) )
48 44 47 rspc ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑀 ) ( 𝐺𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) → ( 𝐺𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) ) )
49 42 48 mpan9 ( ( 𝜑𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) )
50 34 49 seqfveq ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) )
51 3 50 jca ( 𝜑 → ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) )
52 f1oeq1 ( 𝑓 = 𝐹 → ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ) )
53 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑛 ) = ( 𝐹𝑛 ) )
54 53 csbeq1d ( 𝑓 = 𝐹 ( 𝑓𝑛 ) / 𝑘 𝐵 = ( 𝐹𝑛 ) / 𝑘 𝐵 )
55 fvex ( 𝐹𝑛 ) ∈ V
56 55 1 csbie ( 𝐹𝑛 ) / 𝑘 𝐵 = 𝐶
57 54 56 eqtrdi ( 𝑓 = 𝐹 ( 𝑓𝑛 ) / 𝑘 𝐵 = 𝐶 )
58 57 mpteq2dv ( 𝑓 = 𝐹 → ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) = ( 𝑛 ∈ ℕ ↦ 𝐶 ) )
59 58 seqeq3d ( 𝑓 = 𝐹 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) )
60 59 fveq1d ( 𝑓 = 𝐹 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) )
61 60 eqeq2d ( 𝑓 = 𝐹 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) )
62 52 61 anbi12d ( 𝑓 = 𝐹 → ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) ↔ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) ) )
63 32 51 62 spcedv ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) )
64 oveq2 ( 𝑚 = 𝑀 → ( 1 ... 𝑚 ) = ( 1 ... 𝑀 ) )
65 64 f1oeq2d ( 𝑚 = 𝑀 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ) )
66 fveq2 ( 𝑚 = 𝑀 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) )
67 66 eqeq2d ( 𝑚 = 𝑀 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) )
68 65 67 anbi12d ( 𝑚 = 𝑀 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) ) )
69 68 exbidv ( 𝑚 = 𝑀 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) ) )
70 69 rspcev ( ( 𝑀 ∈ ℕ ∧ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑀 ) ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) )
71 2 63 70 syl2anc ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) )
72 71 olcd ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
73 breq2 ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
74 73 3anbi3d ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ) )
75 74 rexbidv ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ) )
76 eqeq1 ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) )
77 76 anbi2d ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
78 77 exbidv ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
79 78 rexbidv ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
80 75 79 orbi12d ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) )
81 80 moi2 ( ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ∧ ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
82 7 81 mpanl1 ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
83 82 ancom2s ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
84 83 expr ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
85 27 72 84 syl2anc ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
86 72 80 syl5ibrcom ( 𝜑 → ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) )
87 85 86 impbid ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
88 87 adantr ( ( 𝜑 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
89 88 iota5 ( ( 𝜑 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
90 7 89 mpan2 ( 𝜑 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
91 6 90 syl5eq ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )