Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | | gsumz.z |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
3 | | eqid 2193 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | simp1 999 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐺 ∈ Mnd) |
5 | | simp2 1000 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℤ) |
6 | | simp3 1001 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
7 | 1, 2 | mndidcl 13001 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 0 ∈
(Base‘𝐺)) |
8 | 4, 7 | syl 14 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈
(Base‘𝐺)) |
9 | 8 | adantr 276 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 0 ∈ (Base‘𝐺)) |
10 | 9 | fmpttd 5705 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↦ 0 ):(𝑀...𝑁)⟶(Base‘𝐺)) |
11 | 1, 2, 3, 4, 5, 6, 10 | gsumfzval 12964 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐺 Σg
(𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁))) |
12 | 11 | adantr 276 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁))) |
13 | | simpr 110 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
14 | 13 | iftrued 3564 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁)) = 0 ) |
15 | 12, 14 | eqtrd 2226 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 ) |
16 | 11 | adantr 276 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁))) |
17 | | simpr 110 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → ¬ 𝑁 < 𝑀) |
18 | 17 | iffalsed 3567 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁)) = (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁)) |
19 | 5 | adantr 276 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝑀 ∈ ℤ) |
20 | 6 | adantr 276 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝑁 ∈ ℤ) |
21 | 5 | zred 9429 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
22 | 6 | zred 9429 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
23 | 21, 22 | lenltd 8127 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀)) |
24 | 23 | biimpar 297 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝑀 ≤ 𝑁) |
25 | | eluz2 9588 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
26 | 19, 20, 24, 25 | syl3anbrc 1183 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
27 | | eluzfz2 10088 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
28 | 26, 27 | syl 14 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
29 | 4 | adantr 276 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → 𝐺 ∈ Mnd) |
30 | | fveqeq2 5555 |
. . . . . 6
⊢ (𝑤 = 𝑀 → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ↔ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑀) = 0 )) |
31 | 30 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 𝑀 → ((𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ) ↔ (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑀) = 0 ))) |
32 | | fveqeq2 5555 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ↔ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 )) |
33 | 32 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ) ↔ (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ))) |
34 | | fveqeq2 5555 |
. . . . . 6
⊢ (𝑤 = (𝑦 + 1) → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ↔ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = 0 )) |
35 | 34 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = (𝑦 + 1) → ((𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ) ↔ (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = 0 ))) |
36 | | fveqeq2 5555 |
. . . . . 6
⊢ (𝑤 = 𝑁 → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ↔ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁) = 0 )) |
37 | 36 | imbi2d 230 |
. . . . 5
⊢ (𝑤 = 𝑁 → ((𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑤) = 0 ) ↔ (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁) = 0 ))) |
38 | | eluzel2 9587 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
39 | 38 | adantr 276 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → 𝑀 ∈ ℤ) |
40 | 39 | adantr 276 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℤ) |
41 | | eluzelz 9591 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
42 | 41 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → 𝑁 ∈ ℤ) |
43 | 40, 42 | fzfigd 10492 |
. . . . . . . . . 10
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) ∈ Fin) |
44 | 43 | mptexd 5777 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → (𝑘 ∈ (𝑀...𝑁) ↦ 0 ) ∈
V) |
45 | | vex 2763 |
. . . . . . . . 9
⊢ 𝑢 ∈ V |
46 | | fvexg 5565 |
. . . . . . . . 9
⊢ (((𝑘 ∈ (𝑀...𝑁) ↦ 0 ) ∈ V ∧ 𝑢 ∈ V) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘𝑢) ∈ V) |
47 | 44, 45, 46 | sylancl 413 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘𝑢) ∈ V) |
48 | | plusgslid 12720 |
. . . . . . . . . . 11
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
49 | 48 | slotex 12635 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Mnd →
(+g‘𝐺)
∈ V) |
50 | 49 | ad2antlr 489 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (+g‘𝐺) ∈ V) |
51 | | simprr 531 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → 𝑣 ∈ V) |
52 | | ovexg 5944 |
. . . . . . . . 9
⊢ ((𝑢 ∈ V ∧
(+g‘𝐺)
∈ V ∧ 𝑣 ∈ V)
→ (𝑢(+g‘𝐺)𝑣) ∈ V) |
53 | 45, 50, 51, 52 | mp3an2i 1353 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (𝑢(+g‘𝐺)𝑣) ∈ V) |
54 | 39, 47, 53 | seq3-1 10523 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑀) = ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘𝑀)) |
55 | | eqid 2193 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 0 ) = (𝑘 ∈ (𝑀...𝑁) ↦ 0 ) |
56 | | eqidd 2194 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → 0 = 0 ) |
57 | | eluzfz1 10087 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
58 | 57 | adantr 276 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → 𝑀 ∈ (𝑀...𝑁)) |
59 | 7 | adantl 277 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → 0 ∈ (Base‘𝐺)) |
60 | 55, 56, 58, 59 | fvmptd3 5643 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘𝑀) = 0 ) |
61 | 54, 60 | eqtrd 2226 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝐺 ∈ Mnd) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑀) = 0 ) |
62 | 61 | ex 115 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑀) = 0 )) |
63 | | elfzouz 10207 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑀..^𝑁) → 𝑦 ∈ (ℤ≥‘𝑀)) |
64 | 63 | adantr 276 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) → 𝑦 ∈ (ℤ≥‘𝑀)) |
65 | | elfzouz2 10218 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑦)) |
66 | | uztrn 9599 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘𝑦) ∧ 𝑦 ∈ (ℤ≥‘𝑀)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
67 | 65, 63, 66 | syl2anc 411 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
68 | 67, 47 | sylanl1 402 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ 𝑢 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘𝑢) ∈ V) |
69 | 67, 53 | sylanl1 402 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (𝑢(+g‘𝐺)𝑣) ∈ V) |
70 | 64, 68, 69 | seq3p1 10526 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦)(+g‘𝐺)((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘(𝑦 + 1)))) |
71 | 70 | adantr 276 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦)(+g‘𝐺)((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘(𝑦 + 1)))) |
72 | | simpr 110 |
. . . . . . . . 9
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) |
73 | | eqidd 2194 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑦 + 1) → 0 = 0 ) |
74 | | fzofzp1 10284 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑀..^𝑁) → (𝑦 + 1) ∈ (𝑀...𝑁)) |
75 | 74 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) → (𝑦 + 1) ∈ (𝑀...𝑁)) |
76 | 7 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) → 0 ∈ (Base‘𝐺)) |
77 | 55, 73, 75, 76 | fvmptd3 5643 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘(𝑦 + 1)) = 0 ) |
78 | 77 | adantr 276 |
. . . . . . . . 9
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘(𝑦 + 1)) = 0 ) |
79 | 72, 78 | oveq12d 5928 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦)(+g‘𝐺)((𝑘 ∈ (𝑀...𝑁) ↦ 0 )‘(𝑦 + 1))) = ( 0 (+g‘𝐺) 0 )) |
80 | 1, 3, 2 | mndlid 13006 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ 0 ∈
(Base‘𝐺)) → (
0
(+g‘𝐺)
0 ) =
0
) |
81 | 7, 80 | mpdan 421 |
. . . . . . . . 9
⊢ (𝐺 ∈ Mnd → ( 0
(+g‘𝐺)
0 ) =
0
) |
82 | 81 | ad2antlr 489 |
. . . . . . . 8
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → ( 0
(+g‘𝐺)
0 ) =
0
) |
83 | 71, 79, 82 | 3eqtrd 2230 |
. . . . . . 7
⊢ (((𝑦 ∈ (𝑀..^𝑁) ∧ 𝐺 ∈ Mnd) ∧ (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = 0 ) |
84 | 83 | exp31 364 |
. . . . . 6
⊢ (𝑦 ∈ (𝑀..^𝑁) → (𝐺 ∈ Mnd → ((seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = 0 ))) |
85 | 84 | a2d 26 |
. . . . 5
⊢ (𝑦 ∈ (𝑀..^𝑁) → ((𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑦) = 0 ) → (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘(𝑦 + 1)) = 0 ))) |
86 | 31, 33, 35, 37, 62, 85 | fzind2 10296 |
. . . 4
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝐺 ∈ Mnd → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁) = 0 )) |
87 | 28, 29, 86 | sylc 62 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → (seq𝑀((+g‘𝐺), (𝑘 ∈ (𝑀...𝑁) ↦ 0 ))‘𝑁) = 0 ) |
88 | 16, 18, 87 | 3eqtrd 2230 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝑁 < 𝑀) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 ) |
89 | | zdclt 9384 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
90 | 6, 5, 89 | syl2anc 411 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
91 | | exmiddc 837 |
. . 3
⊢
(DECID 𝑁 < 𝑀 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
92 | 90, 91 | syl 14 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
93 | 15, 88, 92 | mpjaodan 799 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐺 Σg
(𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 ) |