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 18199 |
. . . 4
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
6 | | ablgrp 18198 |
. . . . . . 7
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
7 | 3, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Grp) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐺 ∈ Grp) |
9 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
10 | | telgsums.f |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) |
12 | | rspcsbela 4006 |
. . . . . 6
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) →
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵) |
13 | 9, 11, 12 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵) |
14 | | peano2nn0 11333 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
15 | | rspcsbela 4006 |
. . . . . 6
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) →
⦋(𝑖 + 1) /
𝑘⦌𝐶 ∈ 𝐵) |
16 | 14, 10, 15 | syl2anr 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
⦋(𝑖 + 1) /
𝑘⦌𝐶 ∈ 𝐵) |
17 | | telgsums.m |
. . . . . 6
⊢ − =
(-g‘𝐺) |
18 | 1, 17 | grpsubcl 17495 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
⦋𝑖 / 𝑘⦌𝐶 ∈ 𝐵 ∧ ⦋(𝑖 + 1) / 𝑘⦌𝐶 ∈ 𝐵) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) |
19 | 8, 13, 16, 18 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) |
20 | 19 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ0
(⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) ∈ 𝐵) |
21 | | telgsums.s |
. . 3
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
22 | | telgsums.u |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 )) |
23 | | rspsbca 3519 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) |
24 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑖 ∈ V |
25 | | sbcimg 3477 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([𝑖 / 𝑘]𝑆 < 𝑘 → [𝑖 / 𝑘]𝐶 = 0 ))) |
26 | | sbcbr2g 4710 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋𝑖 / 𝑘⦌𝑘)) |
27 | | csbvarg 4003 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ V →
⦋𝑖 / 𝑘⦌𝑘 = 𝑖) |
28 | 27 | breq2d 4665 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ V → (𝑆 < ⦋𝑖 / 𝑘⦌𝑘 ↔ 𝑆 < 𝑖)) |
29 | 26, 28 | bitrd 268 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < 𝑖)) |
30 | | sbceq1g 3988 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘]𝐶 = 0 ↔
⦋𝑖 / 𝑘⦌𝐶 = 0 )) |
31 | 29, 30 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ V → (([𝑖 / 𝑘]𝑆 < 𝑘 → [𝑖 / 𝑘]𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) |
32 | 25, 31 | bitrd 268 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ V → ([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) |
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . . 11
⊢
([𝑖 / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 )) |
34 | 23, 33 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 )) |
35 | 34 | expcom 451 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 ) → (𝑖 ∈ ℕ0
→ (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) |
36 | 22, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ ℕ0 → (𝑆 < 𝑖 → ⦋𝑖 / 𝑘⦌𝐶 = 0 ))) |
37 | 36 | imp31 448 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ⦋𝑖 / 𝑘⦌𝐶 = 0 ) |
38 | 21 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ ℝ) |
39 | 38 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈
ℝ) |
40 | 39 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 ∈ ℝ) |
41 | | nn0re 11301 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
42 | 41 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑖 ∈ ℝ) |
43 | 14 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (𝑖 + 1) ∈
ℕ0) |
44 | 43 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (𝑖 + 1) ∈ ℝ) |
45 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 < 𝑖) |
46 | 42 | ltp1d 10954 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑖 < (𝑖 + 1)) |
47 | 40, 42, 44, 45, 46 | lttrd 10198 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝑆 < (𝑖 + 1)) |
48 | 47 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → 𝑆 < (𝑖 + 1))) |
49 | | rspsbca 3519 |
. . . . . . . . . . 11
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) |
50 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑖 + 1) ∈ V |
51 | | sbcimg 3477 |
. . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑖 + 1) / 𝑘]𝐶 = 0 ))) |
52 | | sbcbr2g 4710 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋(𝑖 + 1) / 𝑘⦌𝑘)) |
53 | | csbvarg 4003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 + 1) ∈ V →
⦋(𝑖 + 1) /
𝑘⦌𝑘 = (𝑖 + 1)) |
54 | 53 | breq2d 4665 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈ V → (𝑆 < ⦋(𝑖 + 1) / 𝑘⦌𝑘 ↔ 𝑆 < (𝑖 + 1))) |
55 | 52, 54 | bitrd 268 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < (𝑖 + 1))) |
56 | | sbceq1g 3988 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘]𝐶 = 0 ↔
⦋(𝑖 + 1) /
𝑘⦌𝐶 = 0 )) |
57 | 55, 56 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ V →
(([(𝑖 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑖 + 1) / 𝑘]𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ))) |
58 | 51, 57 | bitrd 268 |
. . . . . . . . . . . 12
⊢ ((𝑖 + 1) ∈ V →
([(𝑖 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ))) |
59 | 50, 58 | ax-mp 5 |
. . . . . . . . . . 11
⊢
([(𝑖 + 1) /
𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) |
60 | 49, 59 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝑖 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) |
61 | 14, 22, 60 | syl2anr 495 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < (𝑖 + 1) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) |
62 | 48, 61 | syld 47 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 )) |
63 | 62 | imp 445 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ⦋(𝑖 + 1) / 𝑘⦌𝐶 = 0 ) |
64 | 37, 63 | oveq12d 6668 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = ( 0 − 0 )) |
65 | 8 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → 𝐺 ∈ Grp) |
66 | 1, 2 | grpidcl 17450 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
67 | 65, 66 | jccir 562 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (𝐺 ∈ Grp ∧ 0 ∈ 𝐵)) |
68 | 1, 2, 17 | grpsubid 17499 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 0 ∈ 𝐵) → ( 0 − 0 ) = 0 ) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → ( 0 − 0 ) = 0 ) |
70 | 64, 69 | eqtrd 2656 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑆 < 𝑖) → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 ) |
71 | 70 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑆 < 𝑖 → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 )) |
72 | 71 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ0 (𝑆 < 𝑖 → (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶) = 0 )) |
73 | 1, 2, 5, 20, 21, 72 | gsummptnn0fzv 18383 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0
↦ (⦋𝑖 /
𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶)))) |
74 | | fzssuz 12382 |
. . . . . 6
⊢
(0...(𝑆 + 1))
⊆ (ℤ≥‘0) |
75 | 74 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0...(𝑆 + 1)) ⊆
(ℤ≥‘0)) |
76 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
77 | 75, 76 | syl6sseqr 3652 |
. . . 4
⊢ (𝜑 → (0...(𝑆 + 1)) ⊆
ℕ0) |
78 | | ssralv 3666 |
. . . 4
⊢
((0...(𝑆 + 1))
⊆ ℕ0 → (∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵)) |
79 | 77, 10, 78 | sylc 65 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵) |
80 | 1, 3, 17, 21, 79 | telgsumfz0s 18388 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶)) |
81 | | peano2nn0 11333 |
. . . . . 6
⊢ (𝑆 ∈ ℕ0
→ (𝑆 + 1) ∈
ℕ0) |
82 | 21, 81 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆 + 1) ∈
ℕ0) |
83 | 38 | ltp1d 10954 |
. . . . 5
⊢ (𝜑 → 𝑆 < (𝑆 + 1)) |
84 | | rspsbca 3519 |
. . . . . . 7
⊢ (((𝑆 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → [(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 )) |
85 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑆 + 1) ∈ V |
86 | | sbcimg 3477 |
. . . . . . . . 9
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ ([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑆 + 1) / 𝑘]𝐶 = 0 ))) |
87 | | sbcbr2g 4710 |
. . . . . . . . . . 11
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < ⦋(𝑆 + 1) / 𝑘⦌𝑘)) |
88 | | csbvarg 4003 |
. . . . . . . . . . . 12
⊢ ((𝑆 + 1) ∈ V →
⦋(𝑆 + 1) /
𝑘⦌𝑘 = (𝑆 + 1)) |
89 | 88 | breq2d 4665 |
. . . . . . . . . . 11
⊢ ((𝑆 + 1) ∈ V → (𝑆 < ⦋(𝑆 + 1) / 𝑘⦌𝑘 ↔ 𝑆 < (𝑆 + 1))) |
90 | 87, 89 | bitrd 268 |
. . . . . . . . . 10
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 ↔ 𝑆 < (𝑆 + 1))) |
91 | | sbceq1g 3988 |
. . . . . . . . . 10
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘]𝐶 = 0 ↔
⦋(𝑆 + 1) /
𝑘⦌𝐶 = 0 )) |
92 | 90, 91 | imbi12d 334 |
. . . . . . . . 9
⊢ ((𝑆 + 1) ∈ V →
(([(𝑆 + 1) / 𝑘]𝑆 < 𝑘 → [(𝑆 + 1) / 𝑘]𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) |
93 | 86, 92 | bitrd 268 |
. . . . . . . 8
⊢ ((𝑆 + 1) ∈ V →
([(𝑆 + 1) / 𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) |
94 | 85, 93 | ax-mp 5 |
. . . . . . 7
⊢
([(𝑆 + 1) /
𝑘](𝑆 < 𝑘 → 𝐶 = 0 ) ↔ (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 )) |
95 | 84, 94 | sylib 208 |
. . . . . 6
⊢ (((𝑆 + 1) ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 )) → (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 )) |
96 | 95 | ex 450 |
. . . . 5
⊢ ((𝑆 + 1) ∈ ℕ0
→ (∀𝑘 ∈
ℕ0 (𝑆 <
𝑘 → 𝐶 = 0 ) → (𝑆 < (𝑆 + 1) → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ))) |
97 | 82, 22, 83, 96 | syl3c 66 |
. . . 4
⊢ (𝜑 → ⦋(𝑆 + 1) / 𝑘⦌𝐶 = 0 ) |
98 | 97 | oveq2d 6666 |
. . 3
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶) = (⦋0 / 𝑘⦌𝐶 − 0 )) |
99 | | 0nn0 11307 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
100 | 99 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℕ0) |
101 | | rspcsbela 4006 |
. . . . 5
⊢ ((0
∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) → ⦋0 / 𝑘⦌𝐶 ∈ 𝐵) |
102 | 100, 10, 101 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ⦋0 / 𝑘⦌𝐶 ∈ 𝐵) |
103 | 1, 2, 17 | grpsubid1 17500 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧
⦋0 / 𝑘⦌𝐶 ∈ 𝐵) → (⦋0 / 𝑘⦌𝐶 − 0 ) = ⦋0 /
𝑘⦌𝐶) |
104 | 7, 102, 103 | syl2anc 693 |
. . 3
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 − 0 ) = ⦋0 /
𝑘⦌𝐶) |
105 | 98, 104 | eqtrd 2656 |
. 2
⊢ (𝜑 → (⦋0 / 𝑘⦌𝐶 −
⦋(𝑆 + 1) /
𝑘⦌𝐶) = ⦋0 / 𝑘⦌𝐶) |
106 | 73, 80, 105 | 3eqtrd 2660 |
1
⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0
↦ (⦋𝑖 /
𝑘⦌𝐶 −
⦋(𝑖 + 1) /
𝑘⦌𝐶))) = ⦋0 / 𝑘⦌𝐶) |