Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
2 | | eqid 2193 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | eqid 2193 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | gsumfzsubmcl.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
5 | | gsumfzsubmcl.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | gsumfzsubmcl.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | | gsumfzsubmcl.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝑆) |
8 | | gsumsubmcl.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) |
9 | 1 | submss 13038 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
10 | 8, 9 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐺)) |
11 | 7, 10 | fssd 5408 |
. . . . . 6
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶(Base‘𝐺)) |
12 | 1, 2, 3, 4, 5, 6, 11 | gsumfzval 12964 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
13 | 12 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
14 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
15 | 14 | iftrued 3564 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = (0g‘𝐺)) |
16 | 13, 15 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (0g‘𝐺)) |
17 | 2 | subm0cl 13040 |
. . . . 5
⊢ (𝑆 ∈ (SubMnd‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
18 | 8, 17 | syl 14 |
. . . 4
⊢ (𝜑 → (0g‘𝐺) ∈ 𝑆) |
19 | 18 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (0g‘𝐺) ∈ 𝑆) |
20 | 16, 19 | eqeltrd 2270 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) ∈ 𝑆) |
21 | 12 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
22 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ¬ 𝑁 < 𝑀) |
23 | 22 | iffalsed 3567 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, (0g‘𝐺), (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
24 | 21, 23 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
25 | 5 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℤ) |
26 | 6 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℤ) |
27 | 25 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
28 | 26 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
29 | 27, 28, 22 | nltled 8130 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ≤ 𝑁) |
30 | | eluz2 9588 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
31 | 25, 26, 29, 30 | syl3anbrc 1183 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
32 | 7 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹:(𝑀...𝑁)⟶𝑆) |
33 | 32 | ffvelcdmda 5685 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) |
34 | 8 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑆 ∈ (SubMnd‘𝐺)) |
35 | | simprl 529 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
36 | | simprr 531 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
37 | 3 | submcl 13041 |
. . . . 5
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) |
38 | 34, 35, 36, 37 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) |
39 | 5, 6 | fzfigd 10492 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
40 | 39 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝑀...𝑁) ∈ Fin) |
41 | 32, 40 | fexd 5780 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹 ∈ V) |
42 | | plusgslid 12720 |
. . . . . . 7
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
43 | 42 | slotex 12635 |
. . . . . 6
⊢ (𝐺 ∈ Mnd →
(+g‘𝐺)
∈ V) |
44 | 4, 43 | syl 14 |
. . . . 5
⊢ (𝜑 → (+g‘𝐺) ∈ V) |
45 | 44 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (+g‘𝐺) ∈ V) |
46 | 31, 33, 38, 41, 45 | seqclg 10533 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (seq𝑀((+g‘𝐺), 𝐹)‘𝑁) ∈ 𝑆) |
47 | 24, 46 | eqeltrd 2270 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) ∈ 𝑆) |
48 | | zdclt 9384 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
49 | 6, 5, 48 | syl2anc 411 |
. . 3
⊢ (𝜑 → DECID 𝑁 < 𝑀) |
50 | | exmiddc 837 |
. . 3
⊢
(DECID 𝑁 < 𝑀 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
51 | 49, 50 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
52 | 20, 47, 51 | mpjaodan 799 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆) |