Step | Hyp | Ref
| Expression |
1 | | gsumval.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsumval.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | gsumval.p |
. . 3
⊢ + =
(+g‘𝐺) |
4 | | gsumval.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
5 | | gsumfzval.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | gsumfzval.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | 5, 6 | fzfigd 10492 |
. . 3
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
8 | | gsumfzval.f |
. . 3
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
9 | 1, 2, 3, 4, 7, 8 | igsumval 12963 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥(((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
10 | | fn0g 12948 |
. . . . . 6
⊢
0g Fn V |
11 | 4 | elexd 2773 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
12 | | funfvex 5563 |
. . . . . . 7
⊢ ((Fun
0g ∧ 𝐺
∈ dom 0g) → (0g‘𝐺) ∈ V) |
13 | 12 | funfni 5346 |
. . . . . 6
⊢
((0g Fn V ∧ 𝐺 ∈ V) → (0g‘𝐺) ∈ V) |
14 | 10, 11, 13 | sylancr 414 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
15 | 2, 14 | eqeltrid 2280 |
. . . 4
⊢ (𝜑 → 0 ∈ V) |
16 | | seqex 10510 |
. . . . 5
⊢ seq𝑀( + , 𝐹) ∈ V |
17 | | fvexg 5565 |
. . . . 5
⊢
((seq𝑀( + , 𝐹) ∈ V ∧ 𝑁 ∈ ℤ) →
(seq𝑀( + , 𝐹)‘𝑁) ∈ V) |
18 | 16, 6, 17 | sylancr 414 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ∈ V) |
19 | 15, 18 | ifexd 4513 |
. . 3
⊢ (𝜑 → if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)) ∈ V) |
20 | | zdclt 9384 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
21 | 6, 5, 20 | syl2anc 411 |
. . . . . . 7
⊢ (𝜑 → DECID 𝑁 < 𝑀) |
22 | | eqifdc 3592 |
. . . . . . 7
⊢
(DECID 𝑁 < 𝑀 → (𝑥 = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((𝑁 < 𝑀 ∧ 𝑥 = 0 ) ∨ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))))) |
23 | 21, 22 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝑥 = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((𝑁 < 𝑀 ∧ 𝑥 = 0 ) ∨ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))))) |
24 | | fzn 10098 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) |
25 | 5, 6, 24 | syl2anc 411 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) |
26 | 25 | anbi1d 465 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 < 𝑀 ∧ 𝑥 = 0 ) ↔ ((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ))) |
27 | 5 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑀 ∈ ℤ) |
28 | 27 | zred 9429 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑀 ∈ ℝ) |
29 | 6 | adantr 276 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑁 ∈ ℤ) |
30 | 29 | zred 9429 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑁 ∈ ℝ) |
31 | | simprl 529 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → ¬ 𝑁 < 𝑀) |
32 | 28, 30, 31 | nltled 8130 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑀 ≤ 𝑁) |
33 | | eluz 9595 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
34 | 27, 29, 33 | syl2anc 411 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
35 | 32, 34 | mpbird 167 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑁 ∈ (ℤ≥‘𝑀)) |
36 | | oveq2 5918 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → (𝑀...𝑛) = (𝑀...𝑁)) |
37 | 36 | eqeq2d 2205 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → ((𝑀...𝑁) = (𝑀...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑁))) |
38 | | fveq2 5546 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
39 | 38 | eqeq2d 2205 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → (𝑥 = (seq𝑀( + , 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
40 | 37, 39 | anbi12d 473 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
41 | 40 | adantl 277 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) ∧ 𝑛 = 𝑁) → (((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
42 | | eqidd 2194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → (𝑀...𝑁) = (𝑀...𝑁)) |
43 | | simprr 531 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
44 | 42, 43 | jca 306 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → ((𝑀...𝑁) = (𝑀...𝑁) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
45 | 35, 41, 44 | rspcedvd 2870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛))) |
46 | | fveq2 5546 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (ℤ≥‘𝑚) =
(ℤ≥‘𝑀)) |
47 | | oveq1 5917 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑀 → (𝑚...𝑛) = (𝑀...𝑛)) |
48 | 47 | eqeq2d 2205 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → ((𝑀...𝑁) = (𝑚...𝑛) ↔ (𝑀...𝑁) = (𝑀...𝑛))) |
49 | | seqeq1 10511 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑀 → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹)) |
50 | 49 | fveq1d 5548 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑀 → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑛)) |
51 | 50 | eqeq2d 2205 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (𝑥 = (seq𝑚( + , 𝐹)‘𝑛) ↔ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛))) |
52 | 48, 51 | anbi12d 473 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)))) |
53 | 46, 52 | rexeqbidv 2707 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) ↔ ∃𝑛 ∈ (ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)))) |
54 | 53 | spcegv 2848 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ →
(∃𝑛 ∈
(ℤ≥‘𝑀)((𝑀...𝑁) = (𝑀...𝑛) ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑛)) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
55 | 27, 45, 54 | sylc 62 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) |
56 | 55 | ex 115 |
. . . . . . . 8
⊢ (𝜑 → ((¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) → ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
57 | | eluzel2 9587 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → 𝑚 ∈ ℤ) |
58 | 57 | ad2antlr 489 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑚 ∈ ℤ) |
59 | 58 | zred 9429 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑚 ∈ ℝ) |
60 | | eluzelre 9592 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → 𝑛 ∈ ℝ) |
61 | 60 | ad2antlr 489 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑛 ∈ ℝ) |
62 | | eluzle 9594 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → 𝑚 ≤ 𝑛) |
63 | 62 | ad2antlr 489 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑚 ≤ 𝑛) |
64 | 59, 61, 63 | lensymd 8131 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → ¬ 𝑛 < 𝑚) |
65 | | simprl 529 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑀...𝑁) = (𝑚...𝑛)) |
66 | 65 | eqcomd 2199 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑚...𝑛) = (𝑀...𝑁)) |
67 | | fzopth 10117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑚) → ((𝑚...𝑛) = (𝑀...𝑁) ↔ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁))) |
68 | 67 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → ((𝑚...𝑛) = (𝑀...𝑁) ↔ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁))) |
69 | 66, 68 | mpbid 147 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) |
70 | 69 | simprd 114 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑛 = 𝑁) |
71 | 69 | simpld 112 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑚 = 𝑀) |
72 | 70, 71 | breq12d 4042 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (𝑛 < 𝑚 ↔ 𝑁 < 𝑀)) |
73 | 64, 72 | mtbid 673 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → ¬ 𝑁 < 𝑀) |
74 | | simprr 531 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) |
75 | 71 | seqeq1d 10514 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → seq𝑚( + , 𝐹) = seq𝑀( + , 𝐹)) |
76 | 75, 70 | fveq12d 5553 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (seq𝑚( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘𝑁)) |
77 | 74, 76 | eqtrd 2226 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) |
78 | 73, 77 | jca 306 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ ((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) → (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) |
79 | 78 | rexlimdva2 2614 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) → (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
80 | 79 | exlimdv 1830 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)) → (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)))) |
81 | 56, 80 | impbid 129 |
. . . . . . 7
⊢ (𝜑 → ((¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁)) ↔ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) |
82 | 26, 81 | orbi12d 794 |
. . . . . 6
⊢ (𝜑 → (((𝑁 < 𝑀 ∧ 𝑥 = 0 ) ∨ (¬ 𝑁 < 𝑀 ∧ 𝑥 = (seq𝑀( + , 𝐹)‘𝑁))) ↔ (((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))))) |
83 | 23, 82 | bitr2d 189 |
. . . . 5
⊢ (𝜑 → ((((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ↔ 𝑥 = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)))) |
84 | 83 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)) ∈ V) → ((((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))) ↔ 𝑥 = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)))) |
85 | 84 | iota5 5228 |
. . 3
⊢ ((𝜑 ∧ if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)) ∈ V) → (℩𝑥(((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁))) |
86 | 19, 85 | mpdan 421 |
. 2
⊢ (𝜑 → (℩𝑥(((𝑀...𝑁) = ∅ ∧ 𝑥 = 0 ) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)((𝑀...𝑁) = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛)))) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁))) |
87 | 9, 86 | eqtrd 2226 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁))) |