Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → 𝑁 < 𝑀) |
2 | 1 | iftrued 3564 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = 0 ) |
3 | | gsumreidx.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
4 | | gsumreidx.z |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
5 | | eqid 2193 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
6 | | gsumreidx.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ CMnd) |
7 | | gsumfzreidx.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
8 | | gsumfzreidx.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | | gsumreidx.f |
. . . . 5
⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) |
10 | 3, 4, 5, 6, 7, 8, 9 | gsumfzval 12964 |
. . . 4
⊢ (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
11 | 10 | adantr 276 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
12 | | gsumreidx.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
13 | | f1of 5492 |
. . . . . . . 8
⊢ (𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
14 | 12, 13 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
15 | | fco 5411 |
. . . . . . 7
⊢ ((𝐹:(𝑀...𝑁)⟶𝐵 ∧ 𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) → (𝐹 ∘ 𝐻):(𝑀...𝑁)⟶𝐵) |
16 | 9, 14, 15 | syl2anc 411 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘ 𝐻):(𝑀...𝑁)⟶𝐵) |
17 | 3, 4, 5, 6, 7, 8, 16 | gsumfzval 12964 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘ 𝐻)) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁))) |
18 | 17 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝐹 ∘ 𝐻)) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁))) |
19 | 1 | iftrued 3564 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁)) = 0 ) |
20 | 18, 19 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg (𝐹 ∘ 𝐻)) = 0 ) |
21 | 2, 11, 20 | 3eqtr4d 2236 |
. 2
⊢ ((𝜑 ∧ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |
22 | 6 | cmnmndd 13367 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Mnd) |
23 | 22 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
24 | | simprl 529 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
25 | | simprr 531 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
26 | 3, 5 | mndcl 12994 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) |
27 | 23, 24, 25, 26 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) |
28 | 6 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ CMnd) |
29 | 3, 5 | cmncom 13361 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
30 | 28, 24, 25, 29 | syl3anc 1249 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)) |
31 | 22 | ad2antrr 488 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐺 ∈ Mnd) |
32 | 3, 5 | mndass 12995 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
33 | 31, 32 | sylancom 420 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
34 | 7 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℤ) |
35 | 8 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℤ) |
36 | 34 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ∈ ℝ) |
37 | 35 | zred 9429 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ ℝ) |
38 | | simpr 110 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ¬ 𝑁 < 𝑀) |
39 | 36, 37, 38 | nltled 8130 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑀 ≤ 𝑁) |
40 | | eluz2 9588 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
41 | 34, 35, 39, 40 | syl3anbrc 1183 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) |
42 | | ssidd 3200 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐵 ⊆ 𝐵) |
43 | | plusgslid 12720 |
. . . . . . 7
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
44 | 43 | slotex 12635 |
. . . . . 6
⊢ (𝐺 ∈ CMnd →
(+g‘𝐺)
∈ V) |
45 | 6, 44 | syl 14 |
. . . . 5
⊢ (𝜑 → (+g‘𝐺) ∈ V) |
46 | 45 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (+g‘𝐺) ∈ V) |
47 | 12 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
48 | | f1ocnv 5505 |
. . . . 5
⊢ (𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
49 | 47, 48 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ◡𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
50 | 16 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐹 ∘ 𝐻):(𝑀...𝑁)⟶𝐵) |
51 | 50 | ffvelcdmda 5685 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹 ∘ 𝐻)‘𝑥) ∈ 𝐵) |
52 | 14 | ad2antrr 488 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
53 | 12, 48 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) |
54 | | f1of 5492 |
. . . . . . . . 9
⊢ (◡𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → ◡𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
55 | 53, 54 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
56 | 55 | adantr 276 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → ◡𝐻:(𝑀...𝑁)⟶(𝑀...𝑁)) |
57 | 56 | ffvelcdmda 5685 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (◡𝐻‘𝑘) ∈ (𝑀...𝑁)) |
58 | | fvco3 5620 |
. . . . . 6
⊢ ((𝐻:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ (◡𝐻‘𝑘) ∈ (𝑀...𝑁)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑘)) = (𝐹‘(𝐻‘(◡𝐻‘𝑘)))) |
59 | 52, 57, 58 | syl2anc 411 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑘)) = (𝐹‘(𝐻‘(◡𝐻‘𝑘)))) |
60 | | f1ocnvfv2 5813 |
. . . . . . 7
⊢ ((𝐻:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘(◡𝐻‘𝑘)) = 𝑘) |
61 | 47, 60 | sylan 283 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘(◡𝐻‘𝑘)) = 𝑘) |
62 | 61 | fveq2d 5550 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘(𝐻‘(◡𝐻‘𝑘))) = (𝐹‘𝑘)) |
63 | 59, 62 | eqtr2d 2227 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑁 < 𝑀) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = ((𝐹 ∘ 𝐻)‘(◡𝐻‘𝑘))) |
64 | 7, 8 | fzfigd 10492 |
. . . . . . 7
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
65 | 9, 64 | fexd 5780 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) |
66 | 14, 64 | fexd 5780 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ V) |
67 | | coexg 5202 |
. . . . . 6
⊢ ((𝐹 ∈ V ∧ 𝐻 ∈ V) → (𝐹 ∘ 𝐻) ∈ V) |
68 | 65, 66, 67 | syl2anc 411 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘ 𝐻) ∈ V) |
69 | 68 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐹 ∘ 𝐻) ∈ V) |
70 | 9 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹:(𝑀...𝑁)⟶𝐵) |
71 | 64 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝑀...𝑁) ∈ Fin) |
72 | 70, 71 | fexd 5780 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → 𝐹 ∈ V) |
73 | 27, 30, 33, 41, 42, 46, 49, 51, 63, 69, 72 | seqf1og 10582 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (seq𝑀((+g‘𝐺), 𝐹)‘𝑁) = (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁)) |
74 | 10 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁))) |
75 | 38 | iffalsed 3567 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
76 | 74, 75 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (seq𝑀((+g‘𝐺), 𝐹)‘𝑁)) |
77 | 17 | adantr 276 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg (𝐹 ∘ 𝐻)) = if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁))) |
78 | 38 | iffalsed 3567 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → if(𝑁 < 𝑀, 0 , (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁)) = (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁)) |
79 | 77, 78 | eqtrd 2226 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg (𝐹 ∘ 𝐻)) = (seq𝑀((+g‘𝐺), (𝐹 ∘ 𝐻))‘𝑁)) |
80 | 73, 76, 79 | 3eqtr4d 2236 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑁 < 𝑀) → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |
81 | | zdclt 9384 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝑁 <
𝑀) |
82 | 8, 7, 81 | syl2anc 411 |
. . 3
⊢ (𝜑 → DECID 𝑁 < 𝑀) |
83 | | exmiddc 837 |
. . 3
⊢
(DECID 𝑁 < 𝑀 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
84 | 82, 83 | syl 14 |
. 2
⊢ (𝜑 → (𝑁 < 𝑀 ∨ ¬ 𝑁 < 𝑀)) |
85 | 21, 80, 84 | mpjaodan 799 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) |