Proof of Theorem telgsums
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | telgsums.b | . . 3
⊢ 𝐵 = (Base‘𝐺) | 
| 2 |  | telgsums.0 | . . 3
⊢  0 =
(0g‘𝐺) | 
| 3 |  | telgsums.g | . . . 4
⊢ (𝜑 → 𝐺 ∈ Abel) | 
| 4 |  | ablcmn 19805 | . . . 4
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 6 |  | ablgrp 19803 | . . . . . . 7
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | 
| 7 | 3, 6 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐺 ∈ Grp) | 
| 9 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) | 
| 10 |  | telgsums.f | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) | 
| 11 | 10 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) | 
| 12 |  | rspcsbela 4438 | . . . . . 6
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) →
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵) | 
| 13 | 9, 11, 12 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵) | 
| 14 |  | peano2nn0 12566 | . . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) | 
| 15 |  | rspcsbela 4438 | . . . . . 6
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) →
⦋(𝑖 + 1) /
𝑘⦌𝐶 ∈ 𝐵) | 
| 16 | 14, 10, 15 | syl2anr 597 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
⦋(𝑖 + 1) /
𝑘⦌𝐶 ∈ 𝐵) | 
| 17 |  | telgsums.m | . . . . . 6
⊢  − =
(-g‘𝐺) | 
| 18 | 1, 17 | grpsubcl 19038 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵 ∧ ⦋(𝑖 + 1) / 𝑘⦌𝐶 ∈ 𝐵) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) | 
| 19 | 8, 13, 16, 18 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) | 
| 20 | 19 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ0
(⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) | 
| 21 |  | telgsums.s | . . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) | 
| 22 |  | telgsums.u | . . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 )) | 
| 23 |  | rspsbca 3880 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) | 
| 24 |  | sbcimg 3837 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([𝑖 / 𝑘]𝑆 < 𝑘 → [𝑖 / 𝑘]𝐶 = 0 ))) | 
| 25 |  | sbcbr2g 5201 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋𝑖 / 𝑘⦌𝑘)) | 
| 26 |  | csbvarg 4434 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ V →
⦋𝑖 / 𝑘⦌𝑘 = 𝑖) | 
| 27 | 26 | breq2d 5155 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ V → (𝑆 < ⦋𝑖 / 𝑘⦌𝑘 ↔ 𝑆 < 𝑖)) | 
| 28 | 25, 27 | bitrd 279 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < 𝑖)) | 
| 29 |  | sbceq1g 4417 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝐶 = 0 ↔
⦋𝑖 / 𝑘⦌𝐶 = 0 )) | 
| 30 | 28, 29 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ V → (([𝑖 / 𝑘]𝑆 < 𝑘 → [𝑖 / 𝑘]𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) | 
| 31 | 24, 30 | bitrd 279 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) | 
| 32 | 31 | elv 3485 | . . . . . . . . . . 11
⊢
([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 )) | 
| 33 | 23, 32 | sylib 218 | . . . . . . . . . 10
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 )) | 
| 34 | 33 | expcom 413 | . . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 ) → (𝑖 ∈ ℕ0
→ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) | 
| 35 | 22, 34 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ ℕ0 → (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) | 
| 36 | 35 | imp31 417 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ⦋𝑖 / 𝑘⦌𝐶 = 0 ) | 
| 37 | 21 | nn0red 12588 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈
ℝ) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 ∈ ℝ) | 
| 40 |  | nn0re 12535 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) | 
| 41 | 40 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑖 ∈ ℝ) | 
| 42 | 14 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (𝑖 + 1) ∈
ℕ0) | 
| 43 | 42 | nn0red 12588 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (𝑖 + 1) ∈ ℝ) | 
| 44 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 < 𝑖) | 
| 45 | 41 | ltp1d 12198 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑖 < (𝑖 + 1)) | 
| 46 | 39, 41, 43, 44, 45 | lttrd 11422 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 < (𝑖 + 1)) | 
| 47 | 46 | ex 412 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → 𝑆 < (𝑖 + 1))) | 
| 48 |  | rspsbca 3880 | . . . . . . . . . . 11
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) | 
| 49 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ (𝑖 + 1) ∈ V | 
| 50 |  | sbcimg 3837 | . . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑖 + 1) / 𝑘]𝐶 = 0 ))) | 
| 51 |  | sbcbr2g 5201 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋(𝑖 + 1) / 𝑘⦌𝑘)) | 
| 52 |  | csbvarg 4434 | . . . . . . . . . . . . . . . 16
⊢ ((𝑖 + 1) ∈ V →
⦋(𝑖 + 1) /
𝑘⦌𝑘 = (𝑖 + 1)) | 
| 53 | 52 | breq2d 5155 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈ V → (𝑆 < ⦋(𝑖 + 1) / 𝑘⦌𝑘 ↔ 𝑆 < (𝑖 + 1))) | 
| 54 | 51, 53 | bitrd 279 | . . . . . . . . . . . . . 14
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < (𝑖 + 1))) | 
| 55 |  | sbceq1g 4417 | . . . . . . . . . . . . . 14
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝐶 = 0 ↔
⦋(𝑖 + 1) /
𝑘⦌𝐶 = 0 )) | 
| 56 | 54, 55 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ V →
(([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑖 + 1) / 𝑘]𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ))) | 
| 57 | 50, 56 | bitrd 279 | . . . . . . . . . . . 12
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ))) | 
| 58 | 49, 57 | ax-mp 5 | . . . . . . . . . . 11
⊢
([(𝑖 + 1) /
𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 59 | 48, 58 | sylib 218 | . . . . . . . . . 10
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 60 | 14, 22, 59 | syl2anr 597 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 61 | 47, 60 | syld 47 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 62 | 61 | imp 406 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ) | 
| 63 | 36, 62 | oveq12d 7449 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = ( 0 − 0 )) | 
| 64 | 8 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝐺 ∈ Grp) | 
| 65 | 1, 2 | grpidcl 18983 | . . . . . . 7
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) | 
| 66 | 1, 2, 17 | grpsubid 19042 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 0 ∈ 𝐵) → ( 0 − 0 ) = 0 ) | 
| 67 | 64, 65, 66 | syl2anc2 585 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ( 0 − 0 ) = 0 ) | 
| 68 | 63, 67 | eqtrd 2777 | . . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 ) | 
| 69 | 68 | ex 412 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 )) | 
| 70 | 69 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ0 (𝑆 < 𝑖 → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 )) | 
| 71 | 1, 2, 5, 20, 21, 70 | gsummptnn0fz 20004 | . 2
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0
↦ (⦋𝑖 /
𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶)))) | 
| 72 |  | fzssuz 13605 | . . . . . 6
⊢
(0...(𝑆 + 1))
⊆ (ℤ≥‘0) | 
| 73 | 72 | a1i 11 | . . . . 5
⊢ (𝜑 → (0...(𝑆 + 1)) ⊆
(ℤ≥‘0)) | 
| 74 |  | nn0uz 12920 | . . . . 5
⊢
ℕ0 = (ℤ≥‘0) | 
| 75 | 73, 74 | sseqtrrdi 4025 | . . . 4
⊢ (𝜑 → (0...(𝑆 + 1)) ⊆
ℕ0) | 
| 76 |  | ssralv 4052 | . . . 4
⊢
((0...(𝑆 + 1))
⊆ ℕ0 → (∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵)) | 
| 77 | 75, 10, 76 | sylc 65 | . . 3
⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵) | 
| 78 | 1, 3, 17, 21, 77 | telgsumfz0s 20009 | . 2
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶)) | 
| 79 |  | peano2nn0 12566 | . . . . . 6
⊢ (𝑆 ∈ ℕ0
→ (𝑆 + 1) ∈
ℕ0) | 
| 80 | 21, 79 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑆 + 1) ∈
ℕ0) | 
| 81 | 37 | ltp1d 12198 | . . . . 5
⊢ (𝜑 → 𝑆 < (𝑆 + 1)) | 
| 82 |  | rspsbca 3880 | . . . . . . 7
⊢ (((𝑆 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) | 
| 83 |  | ovex 7464 | . . . . . . . 8
⊢ (𝑆 + 1) ∈ V | 
| 84 |  | sbcimg 3837 | . . . . . . . . 9
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑆 + 1) / 𝑘]𝐶 = 0 ))) | 
| 85 |  | sbcbr2g 5201 | . . . . . . . . . . 11
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋(𝑆 + 1) / 𝑘⦌𝑘)) | 
| 86 |  | csbvarg 4434 | . . . . . . . . . . . 12
⊢ ((𝑆 + 1) ∈ V →
⦋(𝑆 + 1) /
𝑘⦌𝑘 = (𝑆 + 1)) | 
| 87 | 86 | breq2d 5155 | . . . . . . . . . . 11
⊢ ((𝑆 + 1) ∈ V → (𝑆 < ⦋(𝑆 + 1) / 𝑘⦌𝑘 ↔ 𝑆 < (𝑆 + 1))) | 
| 88 | 85, 87 | bitrd 279 | . . . . . . . . . 10
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < (𝑆 + 1))) | 
| 89 |  | sbceq1g 4417 | . . . . . . . . . 10
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝐶 = 0 ↔
⦋(𝑆 + 1) /
𝑘⦌𝐶 = 0 )) | 
| 90 | 88, 89 | imbi12d 344 | . . . . . . . . 9
⊢ ((𝑆 + 1) ∈ V →
(([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑆 + 1) / 𝑘]𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) | 
| 91 | 84, 90 | bitrd 279 | . . . . . . . 8
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) | 
| 92 | 83, 91 | ax-mp 5 | . . . . . . 7
⊢
([(𝑆 + 1) /
𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 93 | 82, 92 | sylib 218 | . . . . . 6
⊢ (((𝑆 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 )) | 
| 94 | 93 | ex 412 | . . . . 5
⊢ ((𝑆 + 1) ∈ ℕ0
→ (∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 ) → (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) | 
| 95 | 80, 22, 81, 94 | syl3c 66 | . . . 4
⊢ (𝜑 → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ) | 
| 96 | 95 | oveq2d 7447 | . . 3
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶) = (⦋0 / 𝑘⦌𝐶 − 0 )) | 
| 97 |  | 0nn0 12541 | . . . . . 6
⊢ 0 ∈
ℕ0 | 
| 98 | 97 | a1i 11 | . . . . 5
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 99 |  | rspcsbela 4438 | . . . . 5
⊢ ((0
∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) → ⦋0 / 𝑘⦌𝐶 ∈ 𝐵) | 
| 100 | 98, 10, 99 | syl2anc 584 | . . . 4
⊢ (𝜑 → ⦋0 / 𝑘⦌𝐶 ∈ 𝐵) | 
| 101 | 1, 2, 17 | grpsubid1 19043 | . . . 4
⊢ ((𝐺 ∈ Grp ∧
⦋0 / 𝑘⦌𝐶 ∈ 𝐵) → (⦋0 / 𝑘⦌𝐶 − 0 ) = ⦋0 /
𝑘⦌𝐶) | 
| 102 | 7, 100, 101 | syl2anc 584 | . . 3
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 − 0 ) = ⦋0 /
𝑘⦌𝐶) | 
| 103 | 96, 102 | eqtrd 2777 | . 2
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶) = ⦋0 / 𝑘⦌𝐶) | 
| 104 | 71, 78, 103 | 3eqtrd 2781 | 1
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0
↦ (⦋𝑖 /
𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = ⦋0 / 𝑘⦌𝐶) |