Step | Hyp | Ref
| Expression |
1 | | gsumcl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsumcl.z |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
3 | | eqid 2193 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | gsumfzcl.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
5 | | gsumfzcl.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | gsumfzcl.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | | gsumfzcl.f |
. . . . . 6
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
8 | 1, 2, 3, 4, 5, 6, 7 | gsumfzval 12964 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
9 | 8 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
10 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
11 | 10 | iftrued 3564 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = 0 ) |
12 | 9, 11 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = 0 ) |
13 | 1, 2 | mndidcl 13001 |
. . . . 5
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
14 | 4, 13 | syl 14 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐵) |
15 | 14 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → 0 ∈ 𝐵) |
16 | 12, 15 | eqeltrd 2270 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) ∈ 𝐵) |
17 | 8 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
18 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ¬ 𝑁 < 𝑀) |
19 | 18 | iffalsed 3567 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
20 | 17, 19 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
21 | 5 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℤ) |
22 | 6 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℤ) |
23 | 21 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
24 | 22 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
25 | 23, 24, 18 | nltled 8130 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ≤ 𝑁) |
26 | | eluz2 9588 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
27 | 21, 22, 25, 26 | syl3anbrc 1183 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
28 | 5, 6 | fzfigd 10492 |
. . . . . . 7
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
29 | 7, 28 | fexd 5780 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) |
30 | 29 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → 𝐹 ∈ V) |
31 | | vex 2763 |
. . . . 5
⊢ 𝑥 ∈ V |
32 | | fvexg 5565 |
. . . . 5
⊢ ((𝐹 ∈ V ∧ 𝑥 ∈ V) → (𝐹‘𝑥) ∈ V) |
33 | 30, 31, 32 | sylancl 413 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ V) |
34 | 7 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...𝑁)⟶𝐵) |
35 | | simpr 110 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...𝑁)) |
36 | 34, 35 | ffvelcdmd 5686 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝐵) |
37 | 4 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
38 | | simprl 529 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
39 | | simprr 531 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
40 | 1, 3 | mndcl 12994 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) |
41 | 37, 38, 39, 40 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) |
42 | | ssv 3201 |
. . . . 5
⊢ 𝐵 ⊆ V |
43 | 42 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐵 ⊆ V) |
44 | | simprl 529 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑥 ∈ V) |
45 | | plusgslid 12720 |
. . . . . . . 8
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
46 | 45 | slotex 12635 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd →
(+g‘𝐺)
∈ V) |
47 | 4, 46 | syl 14 |
. . . . . 6
⊢ (𝜑 → (+g‘𝐺) ∈ V) |
48 | 47 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (+g‘𝐺) ∈ V) |
49 | | simprr 531 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑦 ∈ V) |
50 | | ovexg 5944 |
. . . . 5
⊢ ((𝑥 ∈ V ∧
(+g‘𝐺)
∈ V ∧ 𝑦 ∈ V)
→ (𝑥(+g‘𝐺)𝑦) ∈ V) |
51 | 44, 48, 49, 50 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝐺)𝑦) ∈ V) |
52 | 27, 33, 36, 41, 43, 51 | seq3clss 10532 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (seq𝑀((+g‘𝐺), 𝐹)‘𝑁) ∈ 𝐵) |
53 | 20, 52 | eqeltrd 2270 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) ∈ 𝐵) |
54 | | zdclt 9384 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
55 | 6, 5, 54 | syl2anc 411 |
. . 3
⊢ (𝜑 → DECID 𝑁 < 𝑀) |
56 | | exmiddc 837 |
. . 3
⊢
(DECID 𝑁 < 𝑀 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
57 | 55, 56 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
58 | 16, 53, 57 | mpjaodan 799 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) |