Step | Hyp | Ref
| Expression |
1 | | gsumval2.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | eqid 2193 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | gsumval2.p |
. . 3
⊢ + =
(+g‘𝐺) |
4 | | gsumval2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
5 | | gsumval2.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
6 | | eluzel2 9597 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
7 | 5, 6 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
8 | | eluzelz 9601 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
9 | 5, 8 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
10 | 7, 9 | fzfigd 10502 |
. . 3
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
11 | | gsumval2.f |
. . 3
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
12 | 1, 2, 3, 4, 10, 11 | igsumval 12973 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥(((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
13 | | simprr 531 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) |
14 | | simprl 529 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑀...𝑁) = (𝑚...𝑛)) |
15 | | eqcom 2195 |
. . . . . . . . . . . . . 14
⊢ ((𝑚...𝑛) = (𝑀...𝑁) ↔ (𝑀...𝑁) = (𝑚...𝑛)) |
16 | | fzopth 10127 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → ((𝑚...𝑛) = (𝑀...𝑁) ↔ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁))) |
17 | 15, 16 | bitr3id 194 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁))) |
18 | 17 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁))) |
19 | 14, 18 | mpbid 147 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) |
20 | 19 | simpld 112 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑚 = 𝑀) |
21 | 20 | seqeq1d 10524 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹)) |
22 | 19 | simprd 114 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑛 = 𝑁) |
23 | 21, 22 | fveq12d 5561 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
24 | 13, 23 | eqtrd 2226 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘𝑚) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
25 | 24 | rexlimiva 2606 |
. . . . . 6
⊢
(∃𝑛 ∈
(ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
26 | 25 | exlimiv 1609 |
. . . . 5
⊢
(∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
27 | 7 | elexd 2773 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ V) |
28 | 27 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → 𝑀 ∈ V) |
29 | 5 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
30 | | oveq2 5926 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (𝑀...𝑛) = (𝑀...𝑁)) |
31 | 30 | eqeq2d 2205 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → ((𝑀...𝑁) = (𝑀...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑁))) |
32 | | fveq2 5554 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
33 | 32 | eqeq2d 2205 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
34 | 31, 33 | anbi12d 473 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
35 | 34 | adantl 277 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) ∧ 𝑛 = 𝑁) → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
36 | | eqidd 2194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → (𝑀...𝑁) = (𝑀...𝑁)) |
37 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
38 | 36, 37 | jca 306 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
39 | 29, 35, 38 | rspcedvd 2870 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛))) |
40 | | fveq2 5554 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (ℤ≥‘𝑚) =
(ℤ≥‘𝑀)) |
41 | | oveq1 5925 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (𝑚...𝑛) = (𝑀...𝑛)) |
42 | 41 | eqeq2d 2205 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑛))) |
43 | | seqeq1 10521 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹)) |
44 | 43 | fveq1d 5556 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑛)) |
45 | 44 | eqeq2d 2205 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (𝑥 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛))) |
46 | 42, 45 | anbi12d 473 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)))) |
47 | 40, 46 | rexeqbidv 2707 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)))) |
48 | 28, 39, 47 | spcedv 2849 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) |
49 | 48 | ex 115 |
. . . . 5
⊢ (𝜑 → (𝑥 = (seq𝑀( + , 𝐹)‘𝑁) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
50 | 26, 49 | impbid2 143 |
. . . 4
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
51 | | eluzfz2 10098 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
52 | 5, 51 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
53 | | n0i 3452 |
. . . . . . 7
⊢ (𝑁 ∈ (𝑀...𝑁) → ¬ (𝑀...𝑁) = ∅) |
54 | 52, 53 | syl 14 |
. . . . . 6
⊢ (𝜑 → ¬ (𝑀...𝑁) = ∅) |
55 | 54 | intnanrd 933 |
. . . . 5
⊢ (𝜑 → ¬ ((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺))) |
56 | | biorf 745 |
. . . . 5
⊢ (¬
((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ (((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
57 | 55, 56 | syl 14 |
. . . 4
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ (((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
58 | 50, 57 | bitr3d 190 |
. . 3
⊢ (𝜑 → (𝑥 = (seq𝑀( + , 𝐹)‘𝑁) ↔ (((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
59 | 58 | iotabidv 5237 |
. 2
⊢ (𝜑 → (℩𝑥𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) = (℩𝑥(((𝑀...𝑁) = ∅ ∧ 𝑥 = (0g‘𝐺)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
60 | | eqid 2193 |
. . 3
⊢ (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑁) |
61 | | seqex 10520 |
. . . . 5
⊢ seq𝑀( + , 𝐹) ∈ V |
62 | | fvexg 5573 |
. . . . 5
⊢
((seq𝑀( + , 𝐹) ∈ V ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , 𝐹)‘𝑁) ∈ V) |
63 | 61, 5, 62 | sylancr 414 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ V) |
64 | | eueq 2931 |
. . . . 5
⊢
((seq𝑀( + , 𝐹)‘𝑁) ∈ V ↔ ∃!𝑥 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
65 | 63, 64 | sylib 122 |
. . . 4
⊢ (𝜑 → ∃!𝑥 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
66 | | eqeq1 2200 |
. . . . 5
⊢ (𝑥 = (seq𝑀( + , 𝐹)‘𝑁) → (𝑥 = (seq𝑀( + , 𝐹)‘𝑁) ↔ (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑁))) |
67 | 66 | iota2 5244 |
. . . 4
⊢
(((seq𝑀( + , 𝐹)‘𝑁) ∈ V ∧ ∃!𝑥 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → ((seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑁) ↔ (℩𝑥𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐹)‘𝑁))) |
68 | 63, 65, 67 | syl2anc 411 |
. . 3
⊢ (𝜑 → ((seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀( + , 𝐹)‘𝑁) ↔ (℩𝑥𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐹)‘𝑁))) |
69 | 60, 68 | mpbii 148 |
. 2
⊢ (𝜑 → (℩𝑥𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀( + , 𝐹)‘𝑁)) |
70 | 12, 59, 69 | 3eqtr2d 2232 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁)) |