This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zsum

Description: Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses zsum.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
zsum.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
zsum.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
zsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
zsum.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion zsum ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 zsum.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 zsum.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 zsum.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
4 zsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
5 zsum.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6 eleq1w ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
7 csbeq1 ⊢ ( 𝑛 = 𝑖 → ⦋ 𝑛 / 𝑘 ⦌ 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
8 6 7 ifbieq1d ⊢ ( 𝑛 = 𝑖 → if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) = if ( 𝑖 ∈ 𝐴 , ⦋ 𝑖 / 𝑘 ⦌ 𝐵 , 0 ) )
9 8 cbvmptv ⊢ ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = ( 𝑖 ∈ ℤ ↦ if ( 𝑖 ∈ 𝐴 , ⦋ 𝑖 / 𝑘 ⦌ 𝐵 , 0 ) )
10 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → 𝜑 )
11 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
12 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
13 12 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ
14 csbeq1a ⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
15 14 eleq1d ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
16 13 15 rspc ⊢ ( 𝑖 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
17 11 16 syl5 ⊢ ( 𝑖 ∈ 𝐴 → ( 𝜑 → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
18 10 17 mpan9 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → 𝑚 ∈ ℤ )
20 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → 𝑀 ∈ ℤ )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) )
22 3 1 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
24 9 18 19 20 21 23 sumrb ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
25 24 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ) → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
26 25 expimpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
27 26 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
28 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝐴 ⊆ 𝑍 )
29 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
30 1 29 eqsstri ⊢ 𝑍 ⊆ ℤ
31 zssre ⊢ ℤ ⊆ ℝ
32 30 31 sstri ⊢ 𝑍 ⊆ ℝ
33 ltso ⊢ < Or ℝ
34 soss ⊢ ( 𝑍 ⊆ ℝ → ( < Or ℝ → < Or 𝑍 ) )
35 32 33 34 mp2 ⊢ < Or 𝑍
36 soss ⊢ ( 𝐴 ⊆ 𝑍 → ( < Or 𝑍 → < Or 𝐴 ) )
37 28 35 36 mpisyl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → < Or 𝐴 )
38 fzfi ⊢ ( 1 ... 𝑚 ) ∈ Fin
39 ovex ⊢ ( 1 ... 𝑚 ) ∈ V
40 39 f1oen ⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 → ( 1 ... 𝑚 ) ≈ 𝐴 )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 1 ... 𝑚 ) ≈ 𝐴 )
42 41 ensymd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝐴 ≈ ( 1 ... 𝑚 ) )
43 enfii ⊢ ( ( ( 1 ... 𝑚 ) ∈ Fin ∧ 𝐴 ≈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ Fin )
44 38 42 43 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝐴 ∈ Fin )
45 fz1iso ⊢ ( ( < Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
46 37 44 45 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
47 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝜑 )
48 47 17 mpan9 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
49 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑗 ) )
50 49 csbeq1d ⊢ ( 𝑛 = 𝑗 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
51 csbcow ⊢ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵
52 50 51 eqtr4di ⊢ ( 𝑛 = 𝑗 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
53 52 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
54 eqid ⊢ ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ) = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑔 ‘ 𝑗 ) / 𝑖 ⦌ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
55 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑚 ∈ ℕ )
56 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑀 ∈ ℤ )
57 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
58 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 )
59 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
60 9 48 53 54 55 56 57 58 59 summolem2a ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
61 60 expr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
62 61 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( ∃ 𝑔 𝑔 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
63 46 62 mpd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) )
64 breq2 ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) → ( seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
65 63 64 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
66 65 expimpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
67 66 exlimdv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
68 67 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
69 27 68 jaod ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
70 2 adantr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → 𝑀 ∈ ℤ )
71 22 adantr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
72 simpr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 )
73 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑀 ) )
74 73 sseq2d ⊢ ( 𝑚 = 𝑀 → ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ↔ 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) ) )
75 seqeq1 ⊢ ( 𝑚 = 𝑀 → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) )
76 75 breq1d ⊢ ( 𝑚 = 𝑀 → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
77 74 76 anbi12d ⊢ ( 𝑚 = 𝑀 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ) )
78 77 rspcev ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ) → ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
79 70 71 72 78 syl12anc ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
80 79 orcd ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
81 80 ex ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) )
82 69 81 impbid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) )
83 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
84 29 83 sselid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ ℤ )
85 83 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑗 ∈ 𝑍 )
86 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
88 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 )
89 88 nfeq2 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 )
90 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
91 csbeq1a ⊢ ( 𝑘 = 𝑗 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
92 90 91 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ↔ ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) )
93 89 92 rspc ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) )
94 85 87 93 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
95 fvex ⊢ ( 𝐹 ‘ 𝑗 ) ∈ V
96 94 95 eqeltrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ V )
97 nfcv ⊢ Ⅎ 𝑛 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 )
98 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ 𝐴
99 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝐵
100 nfcv ⊢ Ⅎ 𝑘 0
101 98 99 100 nfif ⊢ Ⅎ 𝑘 if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 )
102 eleq1w ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴 ) )
103 csbeq1a ⊢ ( 𝑘 = 𝑛 → 𝐵 = ⦋ 𝑛 / 𝑘 ⦌ 𝐵 )
104 102 103 ifbieq1d ⊢ ( 𝑘 = 𝑛 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
105 97 101 104 cbvmpt ⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) )
106 105 eqcomi ⊢ ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
107 106 fvmpts ⊢ ( ( 𝑗 ∈ ℤ ∧ ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ V ) → ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
108 84 96 107 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
109 108 94 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
110 2 109 seqfeq ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) = seq 𝑀 ( + , 𝐹 ) )
111 110 breq1d ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝑥 ) )
112 82 111 bitrd ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝑥 ) )
113 112 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 seq 𝑀 ( + , 𝐹 ) ⇝ 𝑥 ) )
114 df-sum ⊢ Σ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛 ∈ 𝐴 , ⦋ 𝑛 / 𝑘 ⦌ 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
115 df-fv ⊢ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = ( ℩ 𝑥 seq 𝑀 ( + , 𝐹 ) ⇝ 𝑥 )
116 113 114 115 3eqtr4g ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )