Metamath Proof Explorer

Theorem fsum

Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014) (Revised by Mario Carneiro, 13-Jun-2019)

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

Proof

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